let X be ext-real-membered set ; :: thesis: ( ( for e being ExtReal holds e in X ) implies X = ExtREAL )
assume A1: for e being ExtReal holds e in X ; :: thesis: X = ExtREAL
thus X c= ExtREAL by Th2; :: according to XBOOLE_0:def 10 :: thesis: ExtREAL c= X
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in ExtREAL or e in X )
assume e in ExtREAL ; :: thesis: e in X
hence e in X by A1; :: thesis: verum