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

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