theorem Th5: :: XREAL_1:5

for a, b being Real st a < b holds
ex c being Real st
( a < c & c < b )