fact: Definition property (a : E) (l : E2P) := A (forall x : E, inc x a -> l x x) (A (forall x y : E, inc x a -> inc y a -> l x y -> l y x -> x = y) (forall x y z : E, inc x a -> inc y a -> inc z a -> l x y -> l y z -> l x z)).
imports: universe