theorem Th25: :: BORSUK_5:26

for a, b being Real st a < b holds
ex p1, p2 being Rational st
( a < p1 & p1 < p2 & p2 < b )