let a, b, c be real number ; :: thesis: ( a < b implies ( c in IRRAT a,b iff ( c is irrational & a < c & c < b ) ) )
assume a < b ; :: thesis: ( c in IRRAT a,b iff ( c is irrational & a < c & c < b ) )

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

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

end;

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