reconsider A = the carrier of (Tunit_circle 2) \ {p} as Subset of (Tunit_circle 2) ;

take (Tunit_circle 2) | A ; :: thesis: the carrier of ((Tunit_circle 2) | A) = the carrier of (Tunit_circle 2) \ {p}

thus the carrier of ((Tunit_circle 2) | A) = the carrier of (Tunit_circle 2) \ {p} by PRE_TOPC:8; :: thesis: verum

take (Tunit_circle 2) | A ; :: thesis: the carrier of ((Tunit_circle 2) | A) = the carrier of (Tunit_circle 2) \ {p}

thus the carrier of ((Tunit_circle 2) | A) = the carrier of (Tunit_circle 2) \ {p} by PRE_TOPC:8; :: thesis: verum