let u be ExtReal; :: thesis: for x being Real holds
( x in ].-infty,u.[ iff x < u )
let x be Real; :: thesis: ( x in ].-infty,u.[ iff x < u )
x in REAL by XREAL_0:def 1;
then -infty < x by XXREAL_0:12;
hence ( x in ].-infty,u.[ iff x < u ) by Th4; :: thesis: verum