let x, y be Real; :: thesis: ( x < y implies ex z being Element of REAL st
( x < z & z < y ) )
assume x < y ; :: thesis: ex z being Element of REAL st
( x < z & z < y )
then consider z being Real such that
A1: x < z and
A2: z < y by XREAL_1:5;
reconsider z = z as Element of REAL by XREAL_0:def 1;
take z ; :: thesis: ( x < z & z < y )
thus ( x < z & z < y ) by A1, A2; :: thesis: verum