:: deftheorem Def9 defines LatAugmentation ROBBINS3:def 9 :
for R being LattStr
for b₂ being LattRelStr holds
( b₂ is LatAugmentation of R iff LattStr(# the carrier of b₂, the L_join of b₂, the L_meet of b₂ #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) );