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, Th14;
hence contradiction by A4, TARSKI:def 1; :: thesis: verum

end;

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