let R be CLatAugmentation of L; :: thesis: R is meet-commutative
OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
then 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 #) ;
hence R is meet-commutative by Th10; :: thesis: verum