let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n) holds |.(p + q).| <= |.p.| + |.q.|
let p, q be Point of (TOP-REAL n); :: thesis: |.(p + q).| <= |.p.| + |.q.|
A1: 0 <= |.p.| by Th60;
0 <= |.q.| by Th60;
then A2: 0 + 0 <= |.p.| + |.q.| by A1, XREAL_1:9;
A3: |.(p + q).| ^2 = ((|.p.| ^2 ) + (2 * |(q,p)|)) + (|.q.| ^2 ) by Th67;
A4: |(p,q)| <= abs |(p,q)| by ABSVALUE:11;
abs |(p,q)| <= |.p.| * |.q.| by Th73;
then |(p,q)| <= |.p.| * |.q.| by A4, XXREAL_0:2;
then 2 * |(p,q)| <= 2 * (|.p.| * |.q.|) by XREAL_1:66;
then (|.p.| ^2 ) + (2 * |(p,q)|) <= (|.p.| ^2 ) + (2 * (|.p.| * |.q.|)) by XREAL_1:9;
then A5: |.(p + q).| ^2 <= ((|.p.| ^2 ) + ((2 * |.p.|) * |.q.|)) + (|.q.| ^2 ) by A3, XREAL_1:9;
0 <= |.(p + q).| ^2 by XREAL_1:65;
then sqrt (|.(p + q).| ^2 ) <= sqrt ((|.p.| + |.q.|) ^2 ) by A5, SQUARE_1:94;
then |.(p + q).| <= sqrt ((|.p.| + |.q.|) ^2 ) by Th60, SQUARE_1:89;
hence |.(p + q).| <= |.p.| + |.q.| by A2, SQUARE_1:89; :: thesis: verum