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

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