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