let a, b be Real; :: thesis: IRRAT (a,b) c= [.a,+infty.[
let x be object ; :: 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 ;
a < x by A1, BORSUK_5:30;
hence x in [.a,+infty.[ by XXREAL_1:236; :: thesis: verum