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 .]
A1: -infty <= r by XXREAL_0:5;
r <= +infty by XXREAL_0:3;
hence r in [.-infty ,+infty .] by A1, Th1; :: thesis: verum