:: deftheorem defines <=> PL_AXIOM:def 13 :
for p, q being Element of PL-WFF holds p <=> q = (p => q) '&' (q => p);