let B be B_Lattice; for a, b being Element of B holds a <=> (a <=> b) = b
let a, b be Element of B; a <=> (a <=> b) = b
A1:
a "/\" ((a "/\" b) "\/" ((a `) "/\" (b `))) = (a "/\" (a "/\" b)) "\/" (a "/\" ((a `) "/\" (b `)))
by LATTICES:def 11;
A2:
(a `) "/\" ((a "/\" (b `)) "\/" ((a `) "/\" b)) = ((a `) "/\" (a "/\" (b `))) "\/" ((a `) "/\" ((a `) "/\" b))
by LATTICES:def 11;
A3:
a "\/" (a `) = Top B
by LATTICES:21;
A4:
(a "/\" b) "\/" ((a `) "/\" b) = (a "\/" (a `)) "/\" b
by LATTICES:def 11;
A5:
(a <=> b) ` = (a "/\" (b `)) "\/" ((a `) "/\" b)
by Th51;
A6:
(a `) "/\" (a "/\" (b `)) = ((a `) "/\" a) "/\" (b `)
by LATTICES:def 7;
A7:
a "/\" (a `) = Bottom B
by LATTICES:20;
A8:
a <=> b = (a "/\" b) "\/" ((a `) "/\" (b `))
by Th50;
A9:
a "/\" (a "/\" b) = (a "/\" a) "/\" b
by LATTICES:def 7;
A10:
a "/\" ((a `) "/\" (b `)) = (a "/\" (a `)) "/\" (b `)
by LATTICES:def 7;
A11:
(a `) "/\" ((a `) "/\" b) = ((a `) "/\" (a `)) "/\" b
by LATTICES:def 7;
a <=> (a <=> b) = (a "/\" (a <=> b)) "\/" ((a `) "/\" ((a <=> b) `))
by Th50;
hence
a <=> (a <=> b) = b
by A8, A5, A1, A2, A9, A6, A11, A10, A7, A4, A3; verum