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