let B be B_Lattice; :: thesis: for a, b being Element of B holds a <=> (a <=> b) = b
let a, b be Element of B; :: thesis: 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; :: thesis: verum