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])

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 Circle2IntervalR is_continuous_at p )

assume A8: p = c[-10] ; :: thesis: Circle2IntervalR 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

Circle2IntervalR | ((Topen_unit_circle c[10]) | aX2) is continuous by Lm43;

then A12: Circle2IntervalR | ((Topen_unit_circle c[10]) | aX2) is_continuous_at x2 ;

Circle2IntervalR | ((Topen_unit_circle c[10]) | aX1) is continuous by Lm42;

then A13: Circle2IntervalR | ((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 Circle2IntervalR is_continuous_at p by A13, A12, TMAP_1:113; :: thesis: verum

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

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])
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;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

proof

A3:
Topen_unit_circle c[10] is SubSpace of Topen_unit_circle c[10]
by TSEP_1:2;
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;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

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 Circle2IntervalR is_continuous_at p )

assume A8: p = c[-10] ; :: thesis: Circle2IntervalR 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

then A11:
the carrier of (Topen_unit_circle c[10]) = aX1 \/ aX2
;
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;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

Circle2IntervalR | ((Topen_unit_circle c[10]) | aX2) is continuous by Lm43;

then A12: Circle2IntervalR | ((Topen_unit_circle c[10]) | aX2) is_continuous_at x2 ;

Circle2IntervalR | ((Topen_unit_circle c[10]) | aX1) is continuous by Lm42;

then A13: Circle2IntervalR | ((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 Circle2IntervalR is_continuous_at p by A13, A12, TMAP_1:113; :: thesis: verum