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
( a <=> (a <=> b) = (a "/\" (a <=> b)) "\/" ((a ` ) "/\" ((a <=> b) ` )) & a <=> b = (a "/\" b) "\/" ((a ` ) "/\" (b ` )) & (a <=> b) ` = (a "/\" (b ` )) "\/" ((a ` ) "/\" b) & a "/\" ((a "/\" b) "\/" ((a ` ) "/\" (b ` ))) = (a "/\" (a "/\" b)) "\/" (a "/\" ((a ` ) "/\" (b ` ))) & (a ` ) "/\" ((a "/\" (b ` )) "\/" ((a ` ) "/\" b)) = ((a ` ) "/\" (a "/\" (b ` ))) "\/" ((a ` ) "/\" ((a ` ) "/\" b)) & a "/\" (a "/\" b) = (a "/\" a) "/\" b & (a ` ) "/\" (a "/\" (b ` )) = ((a ` ) "/\" a) "/\" (b ` ) & a "/\" a = a & (a ` ) "/\" (a ` ) = a ` & (a ` ) "/\" ((a ` ) "/\" b) = ((a ` ) "/\" (a ` )) "/\" b & a "/\" ((a ` ) "/\" (b ` )) = (a "/\" (a ` )) "/\" (b ` ) & (Bottom B) "/\" b = Bottom B & a "/\" (a ` ) = Bottom B & (a ` ) "/\" a = Bottom B & (a "/\" b) "\/" (Bottom B) = a "/\" b & (Bottom B) "\/" ((a ` ) "/\" b) = (a ` ) "/\" b & (a "/\" b) "\/" ((a ` ) "/\" b) = (a "\/" (a ` )) "/\" b & a "\/" (a ` ) = Top B & (Top B) "/\" b = b & (Bottom B) "/\" (b ` ) = Bottom B ) by Th51, Th52, LATTICES:18, LATTICES:39, LATTICES:40, LATTICES:43, LATTICES:47, LATTICES:48, LATTICES:def 7, LATTICES:def 11;
hence a <=> (a <=> b) = b ; :: thesis: verum