let x be Point of (TOP-REAL 2); :: thesis: ( x is Point of (Topen_unit_circle c[-10]) implies ( - 1 < x `1 & x `1 <= 1 ) )

assume A1: x is Point of (Topen_unit_circle c[-10]) ; :: thesis: ( - 1 < x `1 & x `1 <= 1 )

hence ( - 1 < x `1 & x `1 <= 1 ) by A1, A2, Th26, XXREAL_0:1; :: thesis: verum

assume A1: x is Point of (Topen_unit_circle c[-10]) ; :: thesis: ( - 1 < x `1 & x `1 <= 1 )

A2: now :: thesis: not x `1 = - 1

- 1 <= x `1
by A1, Th26;A3:
the carrier of (Topen_unit_circle c[-10]) = the carrier of (Tunit_circle 2) \ {c[-10]}
by Def10;

then A4: not x in {c[-10]} by A1, XBOOLE_0:def 5;

A5: x = |[(x `1),(x `2)]| by EUCLID:53;

assume A6: x `1 = - 1 ; :: thesis: contradiction

x in the carrier of (Tunit_circle 2) by A1, A3, XBOOLE_0:def 5;

then x = c[-10] by A6, A5, Th15;

hence contradiction by A4, TARSKI:def 1; :: thesis: verum

end;then A4: not x in {c[-10]} by A1, XBOOLE_0:def 5;

A5: x = |[(x `1),(x `2)]| by EUCLID:53;

assume A6: x `1 = - 1 ; :: thesis: contradiction

x in the carrier of (Tunit_circle 2) by A1, A3, XBOOLE_0:def 5;

then x = c[-10] by A6, A5, Th15;

hence contradiction by A4, TARSKI:def 1; :: thesis: verum

hence ( - 1 < x `1 & x `1 <= 1 ) by A1, A2, Th26, XXREAL_0:1; :: thesis: verum