let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A1: x in ((IRRAT (2,4)) \/ {4}) \/ {5} ; :: thesis:
then reconsider x = x as Real ;
A2: ( x in (IRRAT (2,4)) \/ {4} or x in {5} ) by A1, XBOOLE_0:def 3;

per cases by A2, XBOOLE_0:def 3;

suppose x in IRRAT (2,4) ; :: thesis:

then x > 2 by Th29;
then x > 1 by XXREAL_0:2;
hence x in ].1,+infty.[ by XXREAL_1:235; :: thesis:

end;

suppose x in {4} ; :: thesis:

then x = 4 by TARSKI:def 1;
hence x in ].1,+infty.[ by XXREAL_1:235; :: thesis:

end;

suppose x in {5} ; :: thesis:

then x = 5 by TARSKI:def 1;
hence x in ].1,+infty.[ by XXREAL_1:235; :: thesis:

end;

end;