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

let X, Y be Element of L; :: thesis: X \+\ (X "/\" Y) = X \ Y

X \+\ (X "/\" Y) = (X "/\" ((X "/\" Y) `)) "\/" (Y "/\" (X "/\" (X `))) by LATTICES:def 7

.= (X "/\" ((X "/\" Y) `)) "\/" (Y "/\" (Bottom L)) by LATTICES:20

.= X "/\" ((X `) "\/" (Y `)) by LATTICES:23

.= (X "/\" (X `)) "\/" (X "/\" (Y `)) by LATTICES:def 11

.= (Bottom L) "\/" (X "/\" (Y `)) by LATTICES:20

.= X "/\" (Y `) ;

hence X \+\ (X "/\" Y) = X \ Y ; :: thesis: verum

let X, Y be Element of L; :: thesis: X \+\ (X "/\" Y) = X \ Y

X \+\ (X "/\" Y) = (X "/\" ((X "/\" Y) `)) "\/" (Y "/\" (X "/\" (X `))) by LATTICES:def 7

.= (X "/\" ((X "/\" Y) `)) "\/" (Y "/\" (Bottom L)) by LATTICES:20

.= X "/\" ((X `) "\/" (Y `)) by LATTICES:23

.= (X "/\" (X `)) "\/" (X "/\" (Y `)) by LATTICES:def 11

.= (Bottom L) "\/" (X "/\" (Y `)) by LATTICES:20

.= X "/\" (Y `) ;

hence X \+\ (X "/\" Y) = X \ Y ; :: thesis: verum