let a, b, c be positive Real; :: thesis: (a + b) * (a + c) > a * ((a + b) + c)
(a * ((a + b) + c)) + (b * c) > (a * ((a + b) + c)) + 0 by XREAL_1:6;
hence (a + b) * (a + c) > a * ((a + b) + c) ; :: thesis: verum