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 )
A2: now :: thesis: not x `1 = - 1
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;
- 1 <= x `1 by A1, Th26;
hence ( - 1 < x `1 & x `1 <= 1 ) by A1, A2, Th26, XXREAL_0:1; :: thesis: verum