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 Th2; :: thesis: verum