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