let a, b be real number ; :: 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 A1: x in IRRAT a,b ; :: thesis: x in [.a,+infty .[
then reconsider x = x as real number ;
a < x by A1, BORSUK_5:53;
hence x in [.a,+infty .[ by XXREAL_1:236; :: thesis: verum