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

( - 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