let u be ext-real number ; :: thesis: for x being real number holds
( x in [.u,+infty.[ iff u <= x )
let x be real number ; :: thesis: ( x in [.u,+infty.[ iff u <= x )
x in REAL by XREAL_0:def 1;
then x < +infty by XXREAL_0:9;
hence ( x in [.u,+infty.[ iff u <= x ) by Th3; :: thesis: verum