let R be CLatAugmentation of L; 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; verum