let p be Point of (TOP-REAL 2); :: thesis: ( |.p.| <= 1 & p `1 <> 0 & p `2 <> 0 implies ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) )
assume A1: ( |.p.| <= 1 & p `1 <> 0 & p `2 <> 0 ) ; :: thesis: ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 )
set a = |.p.|;
A2: |.p.| ^2 = ((p `1 ) ^2 ) + ((p `2 ) ^2 ) by JGRAPH_3:10;
then ((|.p.| ^2 ) - ((p `1 ) ^2 )) + ((p `1 ) ^2 ) > 0 + ((p `1 ) ^2 ) by A1, SQUARE_1:74, XREAL_1:10;
then A3: ( - |.p.| < p `1 & p `1 < |.p.| ) by SQUARE_1:118;
((|.p.| ^2 ) - ((p `2 ) ^2 )) + ((p `2 ) ^2 ) > 0 + ((p `2 ) ^2 ) by A1, A2, SQUARE_1:74, XREAL_1:10;
then A4: ( - |.p.| < p `2 & p `2 < |.p.| ) by SQUARE_1:118;
- |.p.| >= - 1 by A1, XREAL_1:26;
hence ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) by A1, A3, A4, XXREAL_0:2; :: thesis: verum