let B be B_Lattice; :: thesis: for a, b being Element of B holds
( (a => b) ` = a "/\" (b `) & (a <=> b) ` = (a "/\" (b `)) "\/" ((a `) "/\" b) & (a <=> b) ` = a <=> (b `) & (a <=> b) ` = (a `) <=> b )
let a, b be Element of B; :: thesis: ( (a => b) ` = a "/\" (b `) & (a <=> b) ` = (a "/\" (b `)) "\/" ((a `) "/\" b) & (a <=> b) ` = a <=> (b `) & (a <=> b) ` = (a `) <=> b )

A1: now

let a, b be Element of B; :: thesis: (a => b) ` = a "/\" (b `)
thus (a => b) ` = ((a `) "\/" b) ` by FILTER_0:55
.= ((a `) `) "/\" (b `) by LATTICES:51
.= a "/\" (b `) by LATTICES:49 ; :: thesis: verum

end;

hence (a => b) ` = a "/\" (b `) ; :: thesis: ( (a <=> b) ` = (a "/\" (b `)) "\/" ((a `) "/\" b) & (a <=> b) ` = a <=> (b `) & (a <=> b) ` = (a `) <=> b )
thus (a <=> b) ` = ((a => b) `) "\/" ((b => a) `) by LATTICES:50
.= (a "/\" (b `)) "\/" ((b => a) `) by A1
.= (a "/\" (b `)) "\/" ((a `) "/\" b) by A1 ; :: thesis: ( (a <=> b) ` = a <=> (b `) & (a <=> b) ` = (a `) <=> b )
hence (a <=> b) ` = (a "/\" (b `)) "\/" ((a `) "/\" ((b `) `)) by LATTICES:49
.= a <=> (b `) by Th51 ;
:: thesis: (a <=> b) ` = (a `) <=> b
hence (a <=> b) ` = (a "/\" (b `)) "\/" ((a `) "/\" ((b `) `)) by Th51
.= (((a `) `) "/\" (b `)) "\/" ((a `) "/\" ((b `) `)) by LATTICES:49
.= ((a `) "/\" b) "\/" (((a `) `) "/\" (b `)) by LATTICES:49
.= (a `) <=> b by Th51 ;
:: thesis: verum