let s, t be Real; :: thesis: ( s <= t implies - t <= - s )
assume s <= t ; :: thesis: - t <= - s
then s - t <= t - t by Lm5;
then (s - t) - s <= 0 - s by Lm5;
hence - t <= - s ; :: thesis: verum