theorem Th1: :: LATTICE3:1

for X being set
for x, y being Element of (BooleLatt X) holds
( x "\/" y = x \/ y & x "/\" y = x /\ y ) ;