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