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 )

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

( (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 `)

hence
(a => b) ` = a "/\" (b `)
; :: thesis: ( (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 `)

thus (a => b) ` = ((a `) "\/" b) ` by FILTER_0:42

.= ((a `) `) "/\" (b `) by LATTICES:24

.= a "/\" (b `) ; :: thesis: verum

end;thus (a => b) ` = ((a `) "\/" b) ` by FILTER_0:42

.= ((a `) `) "/\" (b `) by LATTICES:24

.= a "/\" (b `) ; :: thesis: verum

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