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