theorem eqscomb (A B: set): $ A == B <-> B == A $;
A == B -> B == A
B == A -> A == B
A == B <-> B == A