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