let X be set ; :: thesis:
let S be N_Sub_set_fam of X; :: thesis:
consider F being sequence of (bool X) such that
A1: S = rng F by SUPINF_2:def 8;
defpred S₁[ object , object ] means ex V being Subset of X st
( V = F . $1 & $2 = V ` );
A2: for n being object st n in NAT holds
ex y being object st
( y in X \ S & S₁[n,y] )

let n be object ; :: thesis:
assume n in NAT ; :: thesis:
then consider V being set such that
A3: V in S and
A4: V = F . n by A1, FUNCT_2:4;
reconsider V = V as Subset of X by A3;
take V ` ; :: thesis:
(V `) ` in S by A3;
hence ( V ` in X \ S & S₁[n,V ` ] ) by A4, SETFAM_1:def 7; :: thesis:

end;

A5: ex G being sequence of (X \ S) st
for n being object st n in NAT holds
S₁[n,G . n] from FUNCT_2:sch 1(A2);
A6: NAT = dom F by FUNCT_2:def 1;
ex G being sequence of (bool X) st X \ S = rng G

consider G being sequence of (X \ S) such that
A7: for n being object st n in NAT holds
ex V being Subset of X st
( V = F . n & G . n = V ` ) by A5;
A8: dom G = NAT by FUNCT_2:def 1;
A9: X \ S c= rng G

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A10: x in X \ S ; :: thesis:
then reconsider B = x as Subset of X ;
B ` in S by A10, SETFAM_1:def 7;
then consider n being object such that
A11: n in NAT and
A12: F . n = B ` by A1, A6, FUNCT_1:def 3;
ex V being Subset of X st
( V = F . n & G . n = V ` ) by A7, A11;
hence x in rng G by A8, A11, A12, FUNCT_1:def 3; :: thesis:

end;

reconsider G = G as sequence of (bool X) by FUNCT_2:7;
take G ; :: thesis:
thus X \ S = rng G by A9; :: thesis:

end;