let x be Real; :: thesis: ( ( for e being Real st 0 < e holds
x <= e ) implies x <= 0 )
assume A1: for e being Real st 0 < e holds
x <= e ; :: thesis: x <= 0
assume A2: not x <= 0 ; :: thesis: contradiction
then x <= x / 2 by A1;
then x - (x / 2) <= (x / 2) - (x / 2) by XREAL_1:9;
hence contradiction by A2; :: thesis: verum