let x, y be Real; :: thesis: ( ( for c being Real st c > 0 & c < 1 holds
c * x >= y ) implies y <= 0 )
assume A1: for c being Real st c > 0 & c < 1 holds
c * x >= y ; :: thesis: y <= 0
for c being real number st c > 0 & c < 1 holds
c * x >= y

proof

let c be real number ; :: thesis: ( c > 0 & c < 1 implies c * x >= y )
assume A2: ( c > 0 & c < 1 ) ; :: thesis: c * x >= y
c is Real by XREAL_0:def 1;
hence c * x >= y by A1, A2; :: thesis: verum

end;

hence y <= 0 by Th3; :: thesis: verum