let x be Real; :: thesis: ( x is irrational iff x in IRRAT )
A1: x in REAL by XREAL_0:def 1;

hereby :: thesis: ( x in IRRAT implies x is irrational )

assume x is irrational ; :: thesis: x in IRRAT
then not x in RAT ;
hence x in IRRAT by A1, XBOOLE_0:def 5; :: thesis: verum

end;

assume x in IRRAT ; :: thesis: x is irrational
then not x in RAT by XBOOLE_0:def 5;
hence x is irrational by RAT_1:def 2; :: thesis: verum