consider X being set such that
A1: for x being object holds
( x in X iff ( x in COMPLEX & P₁[x] ) ) from XBOOLE_0:sch 1();
X is complex-membered

proof

let x be object ; :: according to MEMBERED:def 1 :: thesis: ( x in X implies x is complex )
assume x in X ; :: thesis: x is complex
then x in COMPLEX by A1;
hence x is complex ; :: thesis: verum

end;

then reconsider X = X as complex-membered set ;
take X ; :: thesis: for c being Complex holds
( c in X iff P₁[c] )
let c be Complex; :: thesis: ( c in X iff P₁[c] )
c in COMPLEX by XCMPLX_0:def 2;
hence ( c in X iff P₁[c] ) by A1; :: thesis: verum