let p be Point of (Tunit_circle 2); :: thesis: Topen_unit_circle p = (Tunit_circle 2) | (([#] (Tunit_circle 2)) \ {p})
[#] (Topen_unit_circle p) = ([#] (Tunit_circle 2)) \ {p} by Def10;
hence Topen_unit_circle p = (Tunit_circle 2) | (([#] (Tunit_circle 2)) \ {p}) by PRE_TOPC:def 5; :: thesis: verum