:: deftheorem defines \ BOOLEALG:def 1 :
for L being Lattice
for X, Y being Element of L holds X \ Y = X "/\" (Y `);