let X be set ; :: thesis: ( X is ext-real-membered implies X c= ExtREAL )
assume A1: X is ext-real-membered ; :: thesis: X c= ExtREAL
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in ExtREAL )
assume x in X ; :: thesis: x in ExtREAL
then x is ext-real by A1;
hence x in ExtREAL ; :: thesis: verum