∀ x y, x = y ⇒ y = x

Theorem sym_eq : forall A, forall (x:A), forall (y:A), (eq (A) x y) -> eq (A) y x.

theorem sym_eq : \forall A. \forall (x:A). \forall (y:A). ((eq) (A) x y) -> (eq) (A) y x.

theorem sym_eq : forall (A : Type) , forall (x:A) , forall (y:A) , ((((logic.eq_) (A)) (x)) (y)) -> (((logic.eq_) (A)) (y)) (x).

sym_eq [A:TYPE+] : LEMMA (FORALL(x:A):(FORALL(y:A):(logic_sttfa.eq[A](x)(y) => logic_sttfa.eq[A](y)(x))))

Printing for OpenTheory is not working at the moment.