let r be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not r in [.-infty,+infty.] or r in ExtREAL ) & ( not r in ExtREAL or r in [.-infty,+infty.] ) )
thus ( r in [.-infty,+infty.] implies r in ExtREAL ) by XXREAL_0:def 1; :: thesis: ( not r in ExtREAL or r in [.-infty,+infty.] )
assume r in ExtREAL ; :: thesis: r in [.-infty,+infty.]
A1: -infty <= r by XXREAL_0:5;
r <= +infty by XXREAL_0:3;
hence r in [.-infty,+infty.] by A1, Th1; :: thesis: verum