25   \begin{center}\small

    25   \begin{center}\small

    26   @{prop[mode=Axiom] "trcl R x x"} \hspace{5mm}

    26   @{prop[mode=Axiom] "trcl R x x"} \hspace{5mm}

    27   @{prop[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}

    27   @{prop[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}

    28   \end{center}

    28   \end{center}

    29 

    29 

    31   defined predicate is the least predicate closed under a collection of

    32   defined predicate is the least predicate closed under a collection of

    32   introduction rules, the predicate @{text "trcl R x y"} can be defined so

    33   introduction rules, the predicate @{text "trcl R x y"} can be defined so

    33   that it holds if and only if @{text "P x y"} holds for every predicate

    34   that it holds if and only if @{text "P x y"} holds for every predicate

    34   @{text P} closed under the rules above. This gives rise to the definition

    35   @{text P} closed under the rules above. This gives rise to the definition

    35 *}

    36 *}