:: deftheorem Def12 defines CLatAugmentation ROBBINS3:def 12 :
for R being OrthoLattStr
for b₂ being OrthoLattRelStr holds
( b₂ is CLatAugmentation of R iff OrthoLattStr(# the carrier of b₂, the L_join of b₂, the L_meet of b₂, the Compl of b₂ #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) );