( the L_join of (L .: ) absorbs the L_meet of (L .: ) & the L_meet of (L .: ) absorbs the L_join of (L .: ) ) by Th40, Th41;
hence L .: is Lattice-like by Th17; :: thesis: verum