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