let p be Point of (TOP-REAL 2); :: thesis: ( |.p.| <= 1 implies ( - 1 <= p `1 & p `1 <= 1 & - 1 <= p `2 & p `2 <= 1 ) )
assume A1: |.p.| <= 1 ; :: 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 ) >= 0 by XREAL_1:65;
then ((|.p.| ^2 ) - ((p `1 ) ^2 )) + ((p `1 ) ^2 ) >= 0 + ((p `1 ) ^2 ) by XREAL_1:9;
then A3: ( - |.p.| <= p `1 & p `1 <= |.p.| ) by SQUARE_1:117;
(|.p.| ^2 ) - ((p `2 ) ^2 ) >= 0 by A2, XREAL_1:65;
then ((|.p.| ^2 ) - ((p `2 ) ^2 )) + ((p `2 ) ^2 ) >= 0 + ((p `2 ) ^2 ) by XREAL_1:9;
then A4: ( - |.p.| <= p `2 & p `2 <= |.p.| ) by SQUARE_1:117;
- |.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