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
(X \+\ Y) \+\ (X "\/" Y) = ((X \+\ Y) "/\" ((X `) "/\" (Y `))) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:24
.= (((X "/\" (Y `)) "/\" ((X `) "/\" (Y `))) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `)))) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:def 11
.= ((X "/\" ((Y `) "/\" ((Y `) "/\" (X `)))) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `)))) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:def 7
.= ((X "/\" (((Y `) "/\" (Y `)) "/\" (X `))) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `)))) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:def 7
.= (((X "/\" (X `)) "/\" (Y `)) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `)))) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:def 7
.= (((Bottom L) "/\" (Y `)) "\/" ((Y "/\" (X `)) "/\" ((X `) "/\" (Y `)))) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:20
.= (Y "/\" ((X `) "/\" ((X `) "/\" (Y `)))) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:def 7
.= (Y "/\" (((X `) "/\" (X `)) "/\" (Y `))) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:def 7
.= ((Y "/\" (Y `)) "/\" (X `)) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:def 7
.= ((Bottom L) "/\" (X `)) "\/" ((X "\/" Y) \ (X \+\ Y)) by LATTICES:20
.= Y "/\" X by Lm1 ;
hence (X \+\ Y) \+\ (X "\/" Y) = X "/\" Y ; :: thesis: verum