let p be Point of (Tunit_circle 2); :: thesis: for x being Point of (TOP-REAL 2) st x is Point of (Topen_unit_circle p) holds
( - 1 <= x `1 & x `1 <= 1 & - 1 <= x `2 & x `2 <= 1 )
let x be Point of (TOP-REAL 2); :: thesis: ( x is Point of (Topen_unit_circle p) implies ( - 1 <= x `1 & x `1 <= 1 & - 1 <= x `2 & x `2 <= 1 ) )
assume x is Point of (Topen_unit_circle p) ; :: thesis: ( - 1 <= x `1 & x `1 <= 1 & - 1 <= x `2 & x `2 <= 1 )
then A1: x in the carrier of (Topen_unit_circle p) ;
the carrier of (Topen_unit_circle p) is Subset of the carrier of (Tunit_circle 2) by TSEP_1:1;
hence ( - 1 <= x `1 & x `1 <= 1 & - 1 <= x `2 & x `2 <= 1 ) by A1, Th13; :: thesis: verum