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 `) `)))) by LATTICES:22
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" ((X "/\" Y) "/\" (((X `) "\/" Y) "/\" ((Y `) "\/" X))) by LATTICES:22
.= (((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)) "\/" (((Bottom L) "\/" ((X "/\" Y) "/\" Y)) "/\" ((Y `) "\/" X)) by LATTICES:15
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" (((X "/\" Y) "/\" Y) "/\" ((Y `) "\/" X)) by LATTICES:14
.= (((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:2
.= (((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)) "\/" ((Bottom L) "\/" ((X "/\" Y) "/\" X)) by LATTICES:15
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" ((X "/\" Y) "/\" X) by LATTICES:14
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" (Y "/\" (X "/\" X)) by LATTICES:def 7
.= (((X \+\ Y) \ X) "\/" ((X \+\ Y) \ Y)) "\/" (Y "/\" X) by LATTICES:2
.= ((((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 `) "/\" (Bottom L)) "\/" (Y "/\" (X `))) "\/" (((X \ Y) "\/" (Y \ X)) "/\" (Y `))) "\/" (Y "/\" X) by LATTICES:2
.= (((Bottom L) "\/" (Y "/\" (X `))) "\/" (((X \ Y) "\/" (Y \ X)) "/\" (Y `))) "\/" (Y "/\" X) by LATTICES:15
.= ((Y "/\" (X `)) "\/" (((X \ Y) "\/" (Y \ X)) "/\" (Y `))) "\/" (Y "/\" X) by LATTICES:14
.= ((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:2
.= ((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 `)) "\/" (Bottom L))) "\/" (Y "/\" X) by LATTICES:15
.= ((Y "/\" (X `)) "\/" (X "/\" (Y `))) "\/" (Y "/\" X) by LATTICES:14
.= (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 by LATTICES:17
.= (Y "\/" X) "/\" ((X `) "\/" X) by LATTICES:11
.= (Y "\/" X) "/\" (Top L) by LATTICES:21
.= Y "\/" X by LATTICES:17 ;
hence (X \+\ Y) \+\ (X "/\" Y) = X "\/" Y ; :: thesis: verum