let x be Point of ; :: thesis: ( x is Point of implies ( - 1 <= x `1 & x `1 < 1 ) )
assume A1: x is Point of ; :: thesis: ( - 1 <= x `1 & x `1 < 1 )

A2: now

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