let a, b, c be real number ; :: thesis: ( a < b implies ( c in RAT a,b iff ( not c is irrational & a < c & c < b ) ) )
assume a < b ; :: 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 c in RAT a,b ; :: thesis: ( not c is irrational & a < c & c < b )
then ( c in RAT & c in ].a,b.[ ) by XBOOLE_0:def 4;
hence ( not c is irrational & a < c & c < b ) by XXREAL_1:4; :: thesis: verum

end;

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