let x, y, z be Element of REAL+ ; :: thesis: ( y -' z <> {} & z <=' y & x <> {} implies (x *' z) - (x *' y) = [{},(x *' (y -' z))] )
assume y -' z <> {} ; :: thesis: ( not z <=' y or not x <> {} or (x *' z) - (x *' y) = [{},(x *' (y -' z))] )
then A1: y <> z by Lm3;
assume z <=' y ; :: thesis: ( not x <> {} or (x *' z) - (x *' y) = [{},(x *' (y -' z))] )
then not y <=' z by A1, Th4;
hence ( not x <> {} or (x *' z) - (x *' y) = [{},(x *' (y -' z))] ) by Th27; :: thesis: verum