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