for a, b, c being Real holds
( c in IRRAT (a,b) iff ( c is irrational & a < c & c < b ) )