let X be set ; :: thesis: for S being N_Sub_set_fam of X holds X \ S is N_Sub_set_fam of X
let S be N_Sub_set_fam of X; :: thesis: X \ S is N_Sub_set_fam of X
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] )

proof

let n be object ; :: thesis: ( n in NAT implies ex y being object st
( y in X \ S & S₁[n,y] ) )
assume n in NAT ; :: thesis: ex y being object st
( y in X \ S & S₁[n,y] )
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 X \ S & S₁[n,V ` ] )
(V `) ` in S by A3;
hence ( V ` in X \ S & S₁[n,V ` ] ) by A4, SETFAM_1:def 7; :: thesis: verum

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

proof

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X \ S or x in rng G )
assume A10: x in X \ S ; :: thesis: x in rng G
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: verum

end;

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

end;

hence X \ S is N_Sub_set_fam of X by SUPINF_2:def 8; :: thesis: verum