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 A1: X "/\" X [= X "/\" (Y `) by LATTICES:9, LATTICES:25;
X \ Y [= X by LATTICES:6;
hence X \ Y = X by A1; :: thesis: verum
end;
assume X \ Y = X ; :: thesis: X "/\" Y = Bottom L
then (X `) "\/" ((Y `) `) = X ` by LATTICES:23;
then X "/\" ((X `) "\/" Y) [= X "/\" (X `) ;
then (X "/\" (X `)) "\/" (X "/\" Y) [= X "/\" (X `) by LATTICES:def 11;
then (Bottom L) "\/" (X "/\" Y) [= X "/\" (X `) by LATTICES:20;
then A2: X "/\" Y [= Bottom L by LATTICES:20;
Bottom L [= X "/\" Y by LATTICES:16;
hence X "/\" Y = Bottom L by A2; :: thesis: verum