thus ( X c= Y implies for c being complex number st c in X holds
c in Y ) ; :: thesis: ( ( for c being complex number st c in X holds
c in Y ) implies X c= Y )
assume A1: for c being complex number st c in X holds
c in Y ; :: thesis: X c= Y
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Y )
assume A2: x in X ; :: thesis: x in Y
thus x in Y by A1, A2; :: thesis: verum