defpred S₁[ set , set ] means $1 in $2;

A1: now

A2: union D = X by Def6;
let e be set ; :: thesis: ( e in X implies ex u being set st
( u in D & S₁[e,u] ) )
assume e in X ; :: thesis: ex u being set st
( u in D & S₁[e,u] )
then ex u being set st
( e in u & u in D ) by A2, TARSKI:def 4;
hence ex u being set st
( u in D & S₁[e,u] ) ; :: thesis: verum

end;

consider F being Function of X,D such that
A3: for e being set st e in X holds
S₁[e,F . e] from FUNCT_2:sch 1(A1);
take F ; :: thesis: for p being Element of X holds p in F . p
let p be Element of X; :: thesis: p in F . p
thus p in F . p by A3; :: thesis: verum