:: deftheorem defines <=> FILTER_0:def 10 :
for L being Lattice
for p, q being Element of L holds p <=> q = (p => q) "/\" (q => p);