[(In (c,COMPLEX)),(In (d,COMPLEX))] in [:COMPLEX,COMPLEX:] by ZFMISC_1:87;
hence In ([c,d],[:COMPLEX,COMPLEX:]) = [c,d] ; :: thesis: verum