let u be ExtReal; :: thesis: for x being Real holds
( x in ].u,+infty.[ iff u < x )
let x be Real; :: 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 Th4; :: thesis: verum