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