let X be set ; :: thesis: ( X is empty implies X is add-closed )
assume A1: X is empty ; :: thesis: X is add-closed
let x be complex number ; :: according to MEMBERED:def 25 :: thesis: for y being complex number st x in X & y in X holds
x + y in X
thus for y being complex number st x in X & y in X holds
x + y in X by A1; :: thesis: verum