let x be ext-real number ; :: according to MEMBERED:def 14 :: thesis: ( ( not x in REAL or x in ].-infty ,+infty .[ ) & ( not x in ].-infty ,+infty .[ or x in REAL ) )
thus ( x in REAL implies x in ].-infty ,+infty .[ ) :: thesis: ( not x in ].-infty ,+infty .[ or x in REAL )

proof

assume x in REAL ; :: thesis: x in ].-infty ,+infty .[
then ( -infty < x & x < +infty ) by XXREAL_0:9, XXREAL_0:12;
hence x in ].-infty ,+infty .[ by Th4; :: thesis: verum

end;

assume x in ].-infty ,+infty .[ ; :: thesis: x in REAL
then ( -infty < x & x < +infty ) by Th4;
hence x in REAL by XXREAL_0:14; :: thesis: verum