let x be ExtReal; :: 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 A1: x in REAL ; :: thesis: x in ].-infty,+infty.[
then A2: -infty < x by XXREAL_0:12;
x < +infty by A1, XXREAL_0:9;
hence x in ].-infty,+infty.[ by A2, Th4; :: thesis: verum

end;

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