let x, y, z be Element of REAL+ ; :: thesis: ( z <=' y implies x *' (y -' z) = (x *' y) - (x *' z) )
assume z <=' y ; :: thesis: x *' (y -' z) = (x *' y) - (x *' z)
then x *' z <=' x *' y by Th8;
then (x *' y) - (x *' z) = (x *' y) -' (x *' z) by Def2;
hence x *' (y -' z) = (x *' y) - (x *' z) by Lm14; :: thesis: verum