let a, b be real number ; :: thesis: IRRAT a,b c= [.a,+infty .[

per cases ( a < b or a >= b ) ;

suppose A1: a < b ; :: thesis: IRRAT a,b c= [.a,+infty .[

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in IRRAT a,b or x in [.a,+infty .[ )
assume A2: x in IRRAT a,b ; :: thesis: x in [.a,+infty .[
then reconsider x = x as real number ;
( x is irrational & a < x & x < b ) by A1, A2, BORSUK_5:53;
hence x in [.a,+infty .[ by XXREAL_1:236; :: thesis: verum

end;

suppose a >= b ; :: thesis: IRRAT a,b c= [.a,+infty .[

then IRRAT a,b = {} by Th35;
hence IRRAT a,b c= [.a,+infty .[ by XBOOLE_1:2; :: thesis: verum

end;

end;