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 `) = a `
by LATTICES:18;
A4:
a "/\" a = a
by LATTICES:18;
A5:
(Bottom B) "/\" (b `) = Bottom B
by LATTICES:40;
A6:
a "\/" (a `) = Top B
by LATTICES:48;
A7:
(a "/\" b) "\/" ((a `) "/\" b) = (a "\/" (a `)) "/\" b
by LATTICES:def 11;
A8:
(Bottom B) "\/" ((a `) "/\" b) = (a `) "/\" b
by LATTICES:39;
A9:
(a <=> b) ` = (a "/\" (b `)) "\/" ((a `) "/\" b)
by Th52;
A10:
(a `) "/\" (a "/\" (b `)) = ((a `) "/\" a) "/\" (b `)
by LATTICES:def 7;
A11:
(a "/\" b) "\/" (Bottom B) = a "/\" b
by LATTICES:39;
A12:
a "/\" (a `) = Bottom B
by LATTICES:47;
A13:
a <=> b = (a "/\" b) "\/" ((a `) "/\" (b `))
by Th51;
A14:
a "/\" (a "/\" b) = (a "/\" a) "/\" b
by LATTICES:def 7;
A15:
a "/\" ((a `) "/\" (b `)) = (a "/\" (a `)) "/\" (b `)
by LATTICES:def 7;
A16:
(a `) "/\" ((a `) "/\" b) = ((a `) "/\" (a `)) "/\" b
by LATTICES:def 7;
a <=> (a <=> b) = (a "/\" (a <=> b)) "\/" ((a `) "/\" ((a <=> b) `))
by Th51;
hence
a <=> (a <=> b) = b
by A13, A9, A1, A2, A14, A10, A4, A3, A16, A15, A12, A11, A8, A7, A6, A5, LATTICES:43; verum