let a, b, c be real number ; :: thesis: ( c in RAT a,b iff ( not c is irrational & a < c & c < b ) )

hereby :: thesis: ( not c is irrational & a < c & c < b implies c in RAT a,b )

assume A1: c in RAT a,b ; :: thesis: ( not c is irrational & a < c & c < b )
then c in ].a,b.[ by XBOOLE_0:def 4;
hence ( not c is irrational & a < c & c < b ) by A1, XXREAL_1:4; :: thesis: verum

end;

assume that
A2: not c is irrational and
A3: a < c and
A4: c < b ; :: thesis: c in RAT a,b
A5: c in RAT by A2, RAT_1:def 2;
c in ].a,b.[ by A3, A4, XXREAL_1:4;
hence c in RAT a,b by A5, XBOOLE_0:def 4; :: thesis: verum