let L be with_zero GAD_Lattice; :: thesis: for x, y being Element of L holds
( x "/\" y = bottom L iff y "/\" x = bottom L )
let x, y be Element of L; :: thesis: ( x "/\" y = bottom L iff y "/\" x = bottom L )
set b1 = bottom L;
thus ( x "/\" y = bottom L implies y "/\" x = bottom L ) :: thesis: ( y "/\" x = bottom L implies x "/\" y = bottom L )

proof

assume Z1: x "/\" y = bottom L ; :: thesis: y "/\" x = bottom L
y "/\" x = y "/\" (x "/\" x) by IMeet
.= (y "/\" x) "/\" x by LATTICES:def 7
.= (x "/\" y) "/\" x by Lem310
.= bottom L by GADL0, Z1 ;
hence y "/\" x = bottom L ; :: thesis: verum

end;

assume Z1: y "/\" x = bottom L ; :: thesis: x "/\" y = bottom L
x "/\" y = x "/\" (y "/\" y) by IMeet
.= (x "/\" y) "/\" y by LATTICES:def 7
.= (y "/\" x) "/\" y by Lem310
.= bottom L by GADL0, Z1 ;
hence x "/\" y = bottom L ; :: thesis: verum