:: deftheorem defines <=> XBOOLEAN:def 8 :
for p, q being boolean object holds p <=> q = (p => q) '&' (q => p);