:: deftheorem Def10 defines Topen_unit_circle TOPREALB:def 10 :
for p being Point of (Tunit_circle 2)
for b₂ being strict SubSpace of Tunit_circle 2 holds
( b₂ = Topen_unit_circle p iff the carrier of b₂ = the carrier of (Tunit_circle 2) \ {p} );