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:50
.= (((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:51
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" ((X "/\" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y "/\" (X `)) `))) by LATTICES:50
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" ((X "/\" Y) "/\" (((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" ((X `) `)))) by LATTICES:50
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" ((X "/\" Y) "/\" (((X `) "\/" Y) "/\" ((Y `) "\/" ((X `) `)))) by LATTICES:49
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" ((X "/\" Y) "/\" (((X `) "\/" Y) "/\" ((Y `) "\/" X))) by LATTICES:49
.= (((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:47
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" (((Bottom L) "\/" ((X "/\" Y) "/\" Y)) "/\" ((Y `) "\/" X)) by LATTICES:40
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" (((X "/\" Y) "/\" Y) "/\" ((Y `) "\/" X)) by LATTICES:39
.= (((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)) by LATTICES:18
.= (((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:47
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" ((Bottom L) "\/" ((X "/\" Y) "/\" X)) by LATTICES:40
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" ((X "/\" Y) "/\" X) by LATTICES:39
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" (Y "/\" (X "/\" X)) by LATTICES:def 7
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" (Y "/\" X) by LATTICES:18
.= ((((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:47
.= ((((Y `) "/\" (Bottom L)) "\/" (Y "/\" (X `))) "\/" (((X \ Y) "\/" (Y \ X)) "/\" (Y `))) "\/" (Y "/\" X) by LATTICES:18
.= (((Bottom L) "\/" (Y "/\" (X `))) "\/" (((X \ Y) "\/" (Y \ X)) "/\" (Y `))) "\/" (Y "/\" X) by LATTICES:40
.= ((Y "/\" (X `)) "\/" (((X \ Y) "\/" (Y \ X)) "/\" (Y `))) "\/" (Y "/\" X) by LATTICES:39
.= ((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 `)) "\/" ((Y "/\" (X `)) "/\" (Y `)))) "\/" (Y "/\" X) by LATTICES:18
.= ((Y "/\" (X `)) "\/" ((X "/\" (Y `)) "\/" ((X `) "/\" (Y "/\" (Y `))))) "\/" (Y "/\" X) by LATTICES:def 7
.= ((Y "/\" (X `)) "\/" ((X "/\" (Y `)) "\/" ((X `) "/\" (Bottom L)))) "\/" (Y "/\" X) by LATTICES:47
.= ((Y "/\" (X `)) "\/" ((X "/\" (Y `)) "\/" (Bottom L))) "\/" (Y "/\" X) by LATTICES:40
.= ((Y "/\" (X `)) "\/" (X "/\" (Y `))) "\/" (Y "/\" X) by LATTICES:39
.= (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:48
.= (Y "/\" (X `)) "\/" X by LATTICES:43
.= (Y "\/" X) "/\" ((X `) "\/" X) by LATTICES:31
.= (Y "\/" X) "/\" (Top L) by LATTICES:48
.= Y "\/" X by LATTICES:43 ;
hence (X \+\ Y) \+\ (X "/\" Y) = X "\/" Y ; :: thesis: verum