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:42
.= ((a `) "\/" b) "/\" ((b `) "\/" a) by FILTER_0:42
.= ((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:20
.= (((a `) "/\" (b `)) "\/" (Bottom B)) "\/" ((Bottom B) "\/" (b "/\" a)) by LATTICES:20
.= ((a `) "/\" (b `)) "\/" ((Bottom B) "\/" (b "/\" a))
.= (a "/\" b) "\/" ((a `) "/\" (b `)) ; :: thesis: verum