A1: the carrier of (Tunit_circle 2) c= circle (0,0,1)
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in the carrier of (Tunit_circle 2) or u in circle (0,0,1) )
assume u in the carrier of (Tunit_circle 2) ; :: thesis: u in circle (0,0,1)
then u in the carrier of (Tcircle ((0. (TOP-REAL 2)),1)) by TOPREALB:def 7;
then u in Sphere ((0. (TOP-REAL 2)),1) by TOPREALB:9;
hence u in circle (0,0,1) by EUCLID:54, TOPREAL9:52; :: thesis: verum
end;
circle (0,0,1) c= the carrier of (Tunit_circle 2)
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in circle (0,0,1) or u in the carrier of (Tunit_circle 2) )
assume u in circle (0,0,1) ; :: thesis: u in the carrier of (Tunit_circle 2)
then u in Sphere ((0. (TOP-REAL 2)),1) by TOPREAL9:52, EUCLID:54;
then u in the carrier of (Tcircle ((0. (TOP-REAL 2)),1)) by TOPREALB:9;
hence u in the carrier of (Tunit_circle 2) by TOPREALB:def 7; :: thesis: verum
end;
hence the carrier of (Tunit_circle 2) = circle (0,0,1) by A1; :: thesis: verum