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

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