let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((IRRAT (2,4)) \/ {4}) \/ {5} or x in ].1,+infty.[ )
assume A1: x in ((IRRAT (2,4)) \/ {4}) \/ {5} ; :: thesis: x in ].1,+infty.[
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 ( x in IRRAT (2,4) or x in {4} or x in {5} ) by A2, XBOOLE_0:def 3;

suppose x in IRRAT (2,4) ; :: thesis: x in ].1,+infty.[

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

end;

suppose x in {4} ; :: thesis: x in ].1,+infty.[

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

end;

suppose x in {5} ; :: thesis: x in ].1,+infty.[

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

end;

end;