let L be B_Lattice; :: thesis: for X, Y being Element of L holds (X "\/" Y) \ (X \+\ Y) = X "/\" Y
let X, Y be Element of L; :: thesis: (X "\/" Y) \ (X \+\ Y) = X "/\" Y
set XY = X "\/" Y;
thus (X "\/" Y) \ (X \+\ Y) = (X "\/" Y) "/\" (((X "/\" (Y `)) `) "/\" ((Y "/\" (X `)) `)) by LATTICES:24
.= (X "\/" Y) "/\" (((X "/\" (Y `)) `) "/\" ((Y `) "\/" ((X `) `))) by LATTICES:23
.= (X "\/" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" ((X `) `))) by LATTICES:23
.= (X "\/" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" X))
.= (X "\/" Y) "/\" (((X `) "\/" Y) "/\" ((Y `) "\/" X))
.= ((X "\/" Y) "/\" ((X `) "\/" Y)) "/\" ((Y `) "\/" X) by LATTICES:def 7
.= (((X "\/" Y) "/\" (X `)) "\/" ((X "\/" Y) "/\" Y)) "/\" ((Y `) "\/" X) by LATTICES:def 11
.= (((X "\/" Y) "/\" (X `)) "\/" Y) "/\" ((Y `) "\/" X) by LATTICES:def 9
.= (((X "/\" (X `)) "\/" (Y "/\" (X `))) "\/" Y) "/\" ((Y `) "\/" X) by LATTICES:def 11
.= (((Bottom L) "\/" (Y "/\" (X `))) "\/" Y) "/\" ((Y `) "\/" X) by LATTICES:20
.= Y "/\" ((Y `) "\/" X) by LATTICES:def 8
.= (Y "/\" (Y `)) "\/" (Y "/\" X) by LATTICES:def 11
.= (Bottom L) "\/" (Y "/\" X) by LATTICES:20
.= X "/\" Y ; :: thesis: verum