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 that
A1: |.p.| <= 1 and
A2: p `1 <> 0 and
A3: p `2 <> 0 ; :: thesis: ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 )
set a = |.p.|;
A4: |.p.| ^2 = ((p `1) ^2) + ((p `2) ^2) by JGRAPH_3:1;
then ((|.p.| ^2) - ((p `1) ^2)) + ((p `1) ^2) > 0 + ((p `1) ^2) by A3, SQUARE_1:12, XREAL_1:8;
then A5: ( - |.p.| < p `1 & p `1 < |.p.| ) by SQUARE_1:48;
((|.p.| ^2) - ((p `2) ^2)) + ((p `2) ^2) > 0 + ((p `2) ^2) by A2, A4, SQUARE_1:12, XREAL_1:8;
then A6: ( - |.p.| < p `2 & p `2 < |.p.| ) by SQUARE_1:48;
- |.p.| >= - 1 by A1, XREAL_1:24;
hence ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) by A1, A5, A6, XXREAL_0:2; :: thesis: verum