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