theorem Th18: :: INTEGR26:18

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