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