let a, b, c be Real; :: 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 A1: c in IRRAT (a,b) ; :: thesis: ( c is irrational & a < c & c < b )
then A2: c in ].a,b.[ by XBOOLE_0:def 4;
c in IRRAT by A1, XBOOLE_0:def 4;
hence ( c is irrational & a < c & c < b ) by A2, Th16, XXREAL_1:4; :: thesis: verum

end;

assume that
A3: c is irrational and
A4: a < c and
A5: c < b ; :: thesis: c in IRRAT (a,b)
A6: c in ].a,b.[ by A4, A5, XXREAL_1:4;
c in IRRAT by A3, Th16;
hence c in IRRAT (a,b) by A6, XBOOLE_0:def 4; :: thesis: verum