theorem Th26: :: BORSUK_5:27

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