λR. ∀ x y z, R x y ⇒ R y z ⇒ R x z

Definition transitive : forall (A:Type), (A -> A -> Prop) -> Prop := fun (A:Type) => fun (R:(A -> A -> Prop)) => forall (x:A), forall (y:A), forall (z:A), (R x y) -> (R y z) -> R x z

definition transitive : \forall A : Type[0] . (A -> A -> Prop) -> Prop := \lambda A : Type[0]. \lambda R : A -> A -> Prop. \forall (x:A). \forall (y:A). \forall (z:A). (R x y) -> (R y z) -> R x z

def transitive : forall (A : Type) , ((A) -> (A) -> Prop) -> Prop := fun (A : Type) , fun (R : (A) -> (A) -> Prop) , forall (x:A) , forall (y:A) , forall (z:A) , (((R) (x)) (y)) -> (((R) (y)) (z)) -> ((R) (x)) (z)

transitive [A:TYPE+] : [[A -> [A -> bool]] -> bool] = (LAMBDA(R:[A -> [A -> bool]]):(FORALL(x:A):(FORALL(y:A):(FORALL(z:A):(R(x)(y) => (R(y)(z) => R(x)(z)))))))

Printing for OpenTheory is not working at the moment.