:: deftheorem defines RelAugmentation ROBBINS3:def 8 :
for R being RelStr
for b₂ being LattRelStr holds
( b₂ is RelAugmentation of R iff RelStr(# the carrier of b₂, the InternalRel of b₂ #) = RelStr(# the carrier of R, the InternalRel of R #) );