let L be B_Lattice; :: thesis: for X, Y being Element of L st X misses Y holds
(X "\/" Y) \ Y = X
let X, Y be Element of L; :: thesis: ( X misses Y implies (X "\/" Y) \ Y = X )
assume X "/\" Y = Bottom L ; :: according to BOOLEALG:def 4 :: thesis: (X "\/" Y) \ Y = X
then (X ` ) "\/" (X "/\" Y) = X ` by LATTICES:39;
then ((X ` ) "\/" X) "/\" ((X ` ) "\/" Y) = X ` by LATTICES:31;
then (Top L) "/\" ((X ` ) "\/" Y) = X ` by LATTICES:48;
then ((X ` ) "\/" Y) ` = (X ` ) ` by LATTICES:43;
then ((X ` ) "\/" Y) ` = X by LATTICES:49;
then A1: ((X ` ) ` ) "/\" (Y ` ) = X by LATTICES:51;
(X "\/" Y) \ Y = (X "/\" (Y ` )) "\/" (Y "/\" (Y ` )) by LATTICES:def 11
.= (X "/\" (Y ` )) "\/" (Bottom L) by LATTICES:47
.= X "/\" (Y ` ) by LATTICES:39 ;
hence (X "\/" Y) \ Y = X by A1, LATTICES:49; :: thesis: verum