let a, b, c be positive Real; :: thesis: for n being positive Real holds (((a + b) + c) to_power n) / ((a + b) to_power n) < ((a + c) to_power n) / (a to_power n)
let n be positive Real; :: thesis: (((a + b) + c) to_power n) / ((a + b) to_power n) < ((a + c) to_power n) / (a to_power n)
( (((a + b) + c) to_power n) / ((a + b) to_power n) = (((a + b) + c) / (a + b)) to_power n & ((a + c) to_power n) / (a to_power n) = ((a + c) / a) to_power n ) by POWER:31;
hence (((a + b) + c) to_power n) / ((a + b) to_power n) < ((a + c) to_power n) / (a to_power n) by FRAC, POWER:37; :: thesis: verum