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 A1, XXREAL_0:14;

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
A2: ( 0 < t & t < z ) by A1, XREAL_1:7;
take t ; :: thesis: ( 0 < t & t < x )
thus ( 0 < t & t < x ) by A2; :: thesis: verum

end;

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

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

end;

end;