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