let p be Point of (TOP-REAL 2); :: thesis: |.p.| <= (abs (p `1 )) + (abs (p `2 ))
|.p.| ^2 = ((p `1 ) ^2 ) + ((p `2 ) ^2 ) by Th46;
then sqrt (((p `1 ) ^2 ) + ((p `2 ) ^2 )) = |.p.| by SQUARE_1:89;
hence |.p.| <= (abs (p `1 )) + (abs (p `2 )) by COMPLEX1:164; :: thesis: verum