let x be ext-real number ; :: thesis: ( 0 < x implies ex y being real number st
( 0 < y & y < x ) )
assume A1: 0 < x ; :: thesis: ex y being real number st
( 0 < y & y < x )

per cases ( x in REAL or x = +infty ) by XXREAL_0:14, A1;

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

then reconsider z = x as real number ;
consider t being real number such that
A3: ( 0 < t & t < z ) by A1, XREAL_1:7;
take t ; :: thesis: ( 0 < t & t < x )
thus ( 0 < t & t < x ) by A3; :: thesis: verum

end;

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

consider z being real number such that
A5: 0 < z by XREAL_1:3;
take z ; :: thesis: ( 0 < z & z < x )
thus ( 0 < z & z < x ) by A4, A5, XXREAL_0:4; :: thesis: verum

end;

end;