theorem :: XBOOLEAN:128
for p, q, r, s being boolean object st p <=> q = TRUE & r <=> s = TRUE holds
(p <=> r) <=> (q <=> s) = TRUE