let r be ext-real number ; :: 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 .]
( -infty <= r & r <= +infty ) by XXREAL_0:3, XXREAL_0:5;
hence r in [.-infty ,+infty .] by Th1; :: thesis: verum