theorem eqscomd (A B: set) (G: wff): $ G -> A == B $ > $ G -> B == A $;
A == B -> B == A
G -> A == B
G -> B == A