let R be CLatAugmentation of L; :: thesis: R is with_Top
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 ComplLLattStr(# the carrier of L,the L_join of L,the Compl of L #) = ComplLLattStr(# the carrier of R,the L_join of R,the Compl of R #) ;
hence R is with_Top by Th19; :: thesis: verum