let L be B_Lattice; :: thesis: for X, Y being Element of L holds
( X "/\" Y = Bottom L iff X \ Y = X )
let X, Y be Element of L; :: thesis: ( X "/\" Y = Bottom L iff X \ Y = X )
thus ( X "/\" Y = Bottom L implies X \ Y = X ) :: thesis: ( X \ Y = X implies X "/\" Y = Bottom L )

proof

assume X "/\" Y = Bottom L ; :: thesis: X \ Y = X
then X [= Y ` by LATTICES:52;
then X "/\" X [= X "/\" (Y ` ) by LATTICES:27;
then A1: X [= X "/\" (Y ` ) by LATTICES:18;
X \ Y [= X by LATTICES:23;
hence X \ Y = X by A1, Def3; :: thesis: verum

end;

assume X \ Y = X ; :: thesis: X "/\" Y = Bottom L
then (X ` ) "\/" ((Y ` ) ` ) = X ` by LATTICES:50;
then X "/\" ((X ` ) "\/" Y) [= X "/\" (X ` ) by LATTICES:49;
then (X "/\" (X ` )) "\/" (X "/\" Y) [= X "/\" (X ` ) by LATTICES:def 11;
then (Bottom L) "\/" (X "/\" Y) [= X "/\" (X ` ) by LATTICES:47;
then (Bottom L) "\/" (X "/\" Y) [= Bottom L by LATTICES:47;
then A2: X "/\" Y [= Bottom L by LATTICES:39;
Bottom L [= X "/\" Y by LATTICES:41;
hence X "/\" Y = Bottom L by A2, Def3; :: thesis: verum