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