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

( 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