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

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