let x be set ; :: 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 number ;
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 Th53;
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;