let x be R_eal; :: thesis: ( 0. < x implies ex y being R_eal st
( 0. < y & y < x ) )
assume A1: 0. < x ; :: thesis: ex y being R_eal st
( 0. < y & y < x )
A2: ( x in REAL or x in {-infty ,+infty } ) by XBOOLE_0:def 3, XXREAL_0:def 4;

per cases ( x in REAL or x = +infty ) by A1, A2, SUPINF_2:19, TARSKI:def 2;

suppose x in REAL ; :: thesis: ex y being R_eal st
( 0. < y & y < x )

then reconsider z = x as Real ;
consider t being real number such that
A3: ( 0 < t & t < z ) by A1, XREAL_1:7;
reconsider t = t as Real by XREAL_0:def 1;
reconsider y = t as R_eal by XXREAL_0:def 1;
take y ; :: thesis: ( 0. < y & y < x )
thus ( 0. < y & y < x ) by A3; :: thesis: verum

end;

suppose A4: x = +infty ; :: thesis: ex y being R_eal st
( 0. < y & y < x )

consider z being real number such that
A5: 0 < z by XREAL_1:3;
reconsider z = z as Real by XREAL_0:def 1;
reconsider y = z as R_eal by XXREAL_0:def 1;
take y ; :: thesis: ( 0. < y & y < x )
thus ( 0. < y & y < x ) by A4, A5, XXREAL_0:4; :: thesis: verum

end;

end;