∀ x y, leibniz x y ⇒ leibniz y x

Axiom sym_leibniz : forall A, forall (x:A), forall (y:A), (leibniz (A) x y) -> leibniz (A) y x

axiom sym_leibniz : \forall A. \forall (x:A). \forall (y:A). ((leibniz) (A) x y) -> (leibniz) (A) y x

axiom sym_leibniz : forall (A : Type) , forall (x:A) , forall (y:A) , ((((leibniz.leibniz) (A)) (x)) (y)) -> (((leibniz.leibniz) (A)) (y)) (x)

sym_leibniz [A:TYPE+] : AXIOM (FORALL(x:A):(FORALL(y:A):(leibniz_sttfa.leibniz[A](x)(y) => leibniz_sttfa.leibniz[A](y)(x))))

Printing for OpenTheory is not working at the moment.