let a, b be Real; :: thesis: ( a <= b implies - b <= - a )
assume a <= b ; :: thesis: - b <= - a
then a - b <= b - b by Lm7;
then (a - b) - a <= 0 - a by Lm7;
hence - b <= - a ; :: thesis: verum