let p be Point of (TOP-REAL 2); :: thesis: ( abs (p `1 ) <= |.p.| & abs (p `2 ) <= |.p.| )
|.p.| = sqrt (((p `1 ) ^2 ) + ((p `2 ) ^2 )) by Th47;
hence ( abs (p `1 ) <= |.p.| & abs (p `2 ) <= |.p.| ) by COMPLEX1:165; :: thesis: verum