for a, b, k being Real st k > 0 holds
( |.(a + b).| to_power k <= (|.a.| + |.b.|) to_power k & (|.a.| + |.b.|) to_power k <= (2 * (max (|.a.|,|.b.|))) to_power k & |.(a + b).| to_power k <= (2 * (max (|.a.|,|.b.|))) to_power k )