let B be B_Lattice; :: thesis: for a, b being Element of B holds a <=> b = (a "/\" b) "\/" ((a `) "/\" (b `))
let a, b be Element of B; :: thesis: a <=> b = (a "/\" b) "\/" ((a `) "/\" (b `))
thus a <=> b = ((a `) "\/" b) "/\" (b => a) by FILTER_0:55
.= ((a `) "\/" b) "/\" ((b `) "\/" a) by FILTER_0:55
.= ((a `) "/\" ((b `) "\/" a)) "\/" (b "/\" ((b `) "\/" a)) by LATTICES:def 11
.= (((a `) "/\" (b `)) "\/" ((a `) "/\" a)) "\/" (b "/\" ((b `) "\/" a)) by LATTICES:def 11
.= (((a `) "/\" (b `)) "\/" ((a `) "/\" a)) "\/" ((b "/\" (b `)) "\/" (b "/\" a)) by LATTICES:def 11
.= (((a `) "/\" (b `)) "\/" (Bottom B)) "\/" ((b "/\" (b `)) "\/" (b "/\" a)) by LATTICES:47
.= (((a `) "/\" (b `)) "\/" (Bottom B)) "\/" ((Bottom B) "\/" (b "/\" a)) by LATTICES:47
.= ((a `) "/\" (b `)) "\/" ((Bottom B) "\/" (b "/\" a)) by LATTICES:39
.= (a "/\" b) "\/" ((a `) "/\" (b `)) by LATTICES:39 ; :: thesis: verum