proposition: Lemma inf_def: forall (x y: X A B), (forall z, z <== x <-> z <== y) -> x==y.
proof: Proof. intros x y H. apply leq_antisym. apply -> H; reflexivity. apply <- H; reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph)