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_{1}[ 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_{1}[n,y] )

for n being object st n in NAT holds

S_{1}[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

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

( 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

proof

A5:
ex G being sequence of (X \ S) st
let n be object ; :: thesis: ( n in NAT implies ex y being object st

( y in X \ S & S_{1}[n,y] ) )

assume n in NAT ; :: thesis: ex y being object st

( y in X \ S & S_{1}[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_{1}[n,V ` ] )

(V `) ` in S by A3;

hence ( V ` in X \ S & S_{1}[n,V ` ] )
by A4, SETFAM_1:def 7; :: thesis: verum

end;( y in X \ S & S

assume n in NAT ; :: thesis: ex y being object st

( y in X \ S & S

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

(V `) ` in S by A3;

hence ( V ` in X \ S & S

for n being object st n in NAT holds

S

A6: NAT = dom F by FUNCT_2:def 1;

ex G being sequence of (bool X) st X \ S = rng G

proof

hence
X \ S is N_Sub_set_fam of X
by SUPINF_2:def 8; :: thesis: verum
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

take G ; :: thesis: X \ S = rng G

thus X \ S = rng G by A9; :: thesis: verum

end;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

reconsider G = G as sequence of (bool X) by FUNCT_2:7;
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;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

take G ; :: thesis: X \ S = rng G

thus X \ S = rng G by A9; :: thesis: verum