let a, b be positive Real; :: thesis: for n being positive light Real holds (a to_power n) + (b to_power n) > (a + b) to_power n
let n be positive light Real; :: thesis: (a to_power n) + (b to_power n) > (a + b) to_power n
reconsider m = 1 - n as Real ;
(a to_power (m + n)) + (b to_power (m + n)) = (a + b) to_power (m + n) ;
hence (a to_power n) + (b to_power n) > (a + b) to_power n by NEW; :: thesis: verum