:: deftheorem defines = BOOLEALG:def 3 :
for L being Lattice
for X, Y being Element of L holds
( X = Y iff ( X [= Y & Y [= X ) );