:: deftheorem Def2 defines omega WAYBEL19:def 2 :
for R being non empty RelStr
for b₂ being Subset-Family of R holds
( b₂ = omega R iff for T being correct lower TopAugmentation of R holds b₂ = the topology of T );