reconsider c1 = c[10] as Point of (TOP-REAL 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 ) } ;
set aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[-10]) & 0 <= q `2 ) } ;
A1: { 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 object ; :: 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;
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 object ; :: 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: Topen_unit_circle c[-10] is SubSpace of Topen_unit_circle c[-10] by TSEP_1:2;
A4: c1 `2 = 0 by EUCLID:52;
A5: c[10] is Point of (Topen_unit_circle c[-10]) by Lm15, Th23;
then A6: 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;
A7: 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, A5;
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 A1, A2, A6;
set X1 = (Topen_unit_circle c[-10]) | aX1;
let p be Point of (Topen_unit_circle c[-10]); :: thesis: ( p = c[10] implies Circle2IntervalL is_continuous_at p )
assume A8: p = c[10] ; :: thesis: Circle2IntervalL is_continuous_at p
reconsider x1 = p as Point of ((Topen_unit_circle c[-10]) | aX1) by A8, A6, PRE_TOPC:8;
set X2 = (Topen_unit_circle c[-10]) | aX2;
reconsider x2 = p as Point of ((Topen_unit_circle c[-10]) | aX2) by A8, A7, PRE_TOPC:8;
A9: the carrier of ((Topen_unit_circle c[-10]) | aX2) = aX2 by PRE_TOPC:8;
the carrier of (Topen_unit_circle c[-10]) c= aX1 \/ aX2
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of (Topen_unit_circle c[-10]) or a in aX1 \/ aX2 )
assume A10: 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 Lm8;
( 0 >= a `2 or 0 <= a `2 ) ;
then ( a in aX1 or a in aX2 ) by A10;
hence a in aX1 \/ aX2 by XBOOLE_0:def 3; :: thesis: verum
end;
then A11: the carrier of (Topen_unit_circle c[-10]) = aX1 \/ aX2 ;
Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX2) is continuous by Lm60;
then A12: Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX2) is_continuous_at x2 ;
Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1) is continuous by Lm59;
then A13: Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1) is_continuous_at x1 ;
the carrier of ((Topen_unit_circle c[-10]) | aX1) = aX1 by PRE_TOPC:8;
then Topen_unit_circle c[-10] = ((Topen_unit_circle c[-10]) | aX1) union ((Topen_unit_circle c[-10]) | aX2) by A9, A3, A11, TSEP_1:def 2;
hence Circle2IntervalL is_continuous_at p by A13, A12, TMAP_1:113; :: thesis: verum