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 :: thesis: for a, b being Element of B holds (a => b) ` = a "/\" (b `)
let a, b be Element of B; :: thesis: (a => b) ` = a "/\" (b `)
thus (a => b) ` = ((a `) "\/" b) ` by FILTER_0:42
.= ((a `) `) "/\" (b `) by LATTICES:24
.= a "/\" (b `) ; :: 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:23
.= (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 `) `))
.= a <=> (b `) by Th50 ;
:: thesis: (a <=> b) ` = (a `) <=> b
hence (a <=> b) ` = (a "/\" (b `)) "\/" ((a `) "/\" ((b `) `)) by Th50
.= (((a `) `) "/\" (b `)) "\/" ((a `) "/\" ((b `) `))
.= ((a `) "/\" b) "\/" (((a `) `) "/\" (b `))
.= (a `) <=> b by Th50 ;
:: thesis: verum