let a, b, c be Real; :: thesis: ( c in RAT (a,b) iff ( c is rational & a < c & c < b ) )

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

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

end;

assume that
A2: c is rational 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