let r, s be real number ; :: thesis: ( r <= 0 & s >= 0 implies r * s <= 0 )
assume that
A1: r <= 0 and
A2: s >= 0 ; :: thesis: r * s <= 0

per cases ( r = 0 or s = 0 or ( r < 0 & s > 0 ) ) by A1, A2, Lm4;

suppose ( r = 0 or s = 0 ) ; :: thesis: r * s <= 0

hence r * s <= 0 ; :: thesis: verum

end;

suppose ( r < 0 & s > 0 ) ; :: thesis: r * s <= 0

hence r * s <= 0 by Lm22; :: thesis: verum

end;

end;