let x, y be real number ; :: thesis: ( x < y implies ex z being Real st
( x < z & z < y ) )
assume x < y ; :: thesis: ex z being Real st
( x < z & z < y )
then consider z being real number such that
A1: ( x < z & z < y ) by XREAL_1:7;
reconsider z = z as Real by XREAL_0:def 1;
take z ; :: thesis: ( x < z & z < y )
thus ( x < z & z < y ) by A1; :: thesis: verum