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 S1[ 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 & S1[n,y] )
proof
let n be object ; :: thesis: ( n in NAT implies ex y being object st
( y in X \ S & S1[n,y] ) )

assume n in NAT ; :: thesis: ex y being object st
( y in X \ S & S1[n,y] )

then consider V being set such that
A3: V in S and
A4: V = F . n by ;
reconsider V = V as Subset of X by A3;
take V ` ; :: thesis: ( V ` in X \ S & S1[n,V ` ] )
(V `) ` in S by A3;
hence ( V ` in X \ S & S1[n,V ` ] ) by ; :: thesis: verum
end;
A5: ex G being sequence of (X \ S) st
for n being object st n in NAT holds
S1[n,G . n] from 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 ;
then consider n being object such that
A11: n in NAT and
A12: F . n = B ` by ;
ex V being Subset of X st
( V = F . n & G . n = V ` ) by ;
hence x in rng G by ; :: 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