let u be ext-real number ; :: thesis: for x being real number holds
( x in ].-infty,u.] iff x <= u )
let x be real number ; :: 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