let R be LatAugmentation of L; :: thesis: not R is empty
LattStr(# the carrier of L,the L_join of L,the L_meet of L #) = LattStr(# the carrier of R,the L_join of R,the L_meet of R #) by Def9;
hence not R is empty ; :: thesis: verum