for a, b, c being Real holds
( c in RAT (a,b) iff ( c is rational & a < c & c < b ) )