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:24
.= ((X `) "\/" ((Y `) `)) "/\" ((Y "/\" (X `)) `) by LATTICES:23
.= ((X `) "\/" ((Y `) `)) "/\" ((Y `) "\/" ((X `) `)) by LATTICES:23
.= ((X `) "\/" Y) "/\" ((Y `) "\/" ((X `) `))
.= ((X `) "\/" Y) "/\" ((Y `) "\/" X)
.= ((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:20
.= ((X `) "/\" (Y `)) "\/" ((Bottom L) "\/" (Y "/\" X)) by LATTICES:20
.= (X "/\" Y) "\/" ((X `) "/\" (Y `)) ; :: thesis: verum