let p be Point of (Topen_unit_circle c[-10] ); :: thesis: ( p = c[10] implies Circle2IntervalL is_continuous_at p )
assume A1: p = c[10] ; :: thesis: Circle2IntervalL is_continuous_at p
set aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10] ) & 0 <= q `2 ) } ;
set aX2 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10] ) & 0 >= q `2 ) } ;
A2: { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10] ) & 0 <= q `2 ) } c= the carrier of (Topen_unit_circle c[-10] )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10] ) & 0 <= q `2 ) } or x in the carrier of (Topen_unit_circle c[-10] ) )
assume x in { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10] ) & 0 <= q `2 ) } ; :: thesis: x in the carrier of (Topen_unit_circle c[-10] )
then ex q being Point of (TOP-REAL 2) st
( x = q & q in the carrier of (Topen_unit_circle c[-10] ) & 0 <= q `2 ) ;
hence x in the carrier of (Topen_unit_circle c[-10] ) ; :: thesis: verum

end;

A3: { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10] ) & 0 >= q `2 ) } c= the carrier of (Topen_unit_circle c[-10] )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10] ) & 0 >= q `2 ) } or x in the carrier of (Topen_unit_circle c[-10] ) )
assume x in { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10] ) & 0 >= q `2 ) } ; :: thesis: x in the carrier of (Topen_unit_circle c[-10] )
then ex q being Point of (TOP-REAL 2) st
( x = q & q in the carrier of (Topen_unit_circle c[-10] ) & 0 >= q `2 ) ;
hence x in the carrier of (Topen_unit_circle c[-10] ) ; :: thesis: verum

end;

reconsider c1 = c[10] as Point of (TOP-REAL 2) ;
A4: c1 `2 = 0 by EUCLID:56;
c[10] is Point of (Topen_unit_circle c[-10] ) by Lm16, Th24;
then A5: ( c[10] in { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10] ) & 0 <= q `2 ) } & c[10] in { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10] ) & 0 >= q `2 ) } ) by A4;
then reconsider aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10] ) & 0 <= q `2 ) } , aX2 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10] ) & 0 >= q `2 ) } as non empty Subset of (Topen_unit_circle c[-10] ) by A2, A3;
set X1 = (Topen_unit_circle c[-10] ) | aX1;
set X2 = (Topen_unit_circle c[-10] ) | aX2;
A6: the carrier of ((Topen_unit_circle c[-10] ) | aX1) = aX1 by PRE_TOPC:29;
reconsider x1 = p as Point of ((Topen_unit_circle c[-10] ) | aX1) by A1, A5, PRE_TOPC:29;
A7: the carrier of ((Topen_unit_circle c[-10] ) | aX2) = aX2 by PRE_TOPC:29;
reconsider x2 = p as Point of ((Topen_unit_circle c[-10] ) | aX2) by A1, A5, PRE_TOPC:29;
A8: Topen_unit_circle c[-10] is SubSpace of Topen_unit_circle c[-10] by TSEP_1:2;
the carrier of (Topen_unit_circle c[-10] ) = aX1 \/ aX2

proof

thus the carrier of (Topen_unit_circle c[-10] ) c= aX1 \/ aX2 :: according to XBOOLE_0:def 10 :: thesis: aX1 \/ aX2 c= the carrier of (Topen_unit_circle c[-10] )

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of (Topen_unit_circle c[-10] ) or a in aX1 \/ aX2 )
assume A9: a in the carrier of (Topen_unit_circle c[-10] ) ; :: thesis: a in aX1 \/ aX2
then reconsider a = a as Point of (TOP-REAL 2) by Lm9;
( 0 >= a `2 or 0 <= a `2 ) ;
then ( a in aX1 or a in aX2 ) by A9;
hence a in aX1 \/ aX2 by XBOOLE_0:def 3; :: thesis: verum

end;

thus aX1 \/ aX2 c= the carrier of (Topen_unit_circle c[-10] ) ; :: thesis: verum

end;

then A10: Topen_unit_circle c[-10] = ((Topen_unit_circle c[-10] ) | aX1) union ((Topen_unit_circle c[-10] ) | aX2) by A6, A7, A8, TSEP_1:def 2;
Circle2IntervalL | ((Topen_unit_circle c[-10] ) | aX1) is continuous by Lm59;
then A11: Circle2IntervalL | ((Topen_unit_circle c[-10] ) | aX1) is_continuous_at x1 by TMAP_1:49;
Circle2IntervalL | ((Topen_unit_circle c[-10] ) | aX2) is continuous by Lm60;
then Circle2IntervalL | ((Topen_unit_circle c[-10] ) | aX2) is_continuous_at x2 by TMAP_1:49;
hence Circle2IntervalL is_continuous_at p by A10, A11, TMAP_1:125; :: thesis: verum