:: deftheorem Def2 defines Omega WAYBEL25:def 2 :
for T being TopStruct
for b₂ being strict TopRelStr holds
( b₂ = Omega T iff ( TopStruct(# the carrier of b₂, the topology of b₂ #) = TopStruct(# the carrier of T, the topology of T #) & ( for x, y being Element of b₂ holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ) ) );