let X be complex-membered set ; :: thesis: ( ( for c being complex number holds c in X ) implies X = COMPLEX )
assume A1: for c being complex number holds c in X ; :: thesis: X = COMPLEX
thus X c= COMPLEX by Th1; :: according to XBOOLE_0:def 10 :: thesis: COMPLEX c= X
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in COMPLEX or e in X )
assume e in COMPLEX ; :: thesis: e in X
then e is complex ;
hence e in X by A1; :: thesis: verum