fact: Definition is_eq_reln (a : E) (r : E2P) := (forall x : E, inc x a -> r x x) & (forall x y : E, inc x a -> inc y a -> r x y -> r y x) & (forall x y z : E, inc x a -> inc y a -> inc z a -> r x y -> r y z -> r x z).
imports: set_theory