theorem Th16: :: BORSUK_5:17

for x being Real holds
( x is irrational iff x in IRRAT )