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:22;
hence |.p.| <= (abs (p `1)) + (abs (p `2)) by COMPLEX1:78; :: thesis: verum