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