DEDUCT_ANTISYM_RULE : thm -> thm -> thm
A |- p B |- q ---------------------------------- (A - {q}) u (B - {p}) |- p <=> q
{q} |- p {p} |- q -------------------------- |- p <=> q
# let th1 = SYM(ASSUME `x:num = y`) and th2 = SYM(ASSUME `y:num = x`);; val th1 : thm = x = y |- y = x val th2 : thm = y = x |- x = y # DEDUCT_ANTISYM_RULE th1 th2;; val it : thm = |- y = x <=> x = y