let R be LatAugmentation of L; :: thesis: R is meet-associative
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 R is meet-associative by Th12; :: thesis: verum