let X be finite set ; :: thesis: ( X c= FinSETS implies X in FinSETS )
consider p being Function such that
A1: rng p = X and
A2: dom p in omega by FINSET_1:def 1;
defpred S₁[ object , object ] means $2 = {(p . $1)};
A3: for x being object st x in dom p holds
ex y being object st S₁[x,y] ;
consider g being Function such that
A4: dom g = dom p and
A5: for x being object st x in dom p holds
S₁[x,g . x] from CLASSES1:sch 1(A3);
assume A6: X c= FinSETS ; :: thesis: X in FinSETS
A7: rng g c= FinSETS

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g or x in FinSETS )
assume x in rng g ; :: thesis: x in FinSETS
then consider y being object such that
A8: y in dom g and
A9: x = g . y by FUNCT_1:def 3;
A10: x = {(p . y)} by A4, A9, A8, A5;
p . y in rng p by A8, A4, FUNCT_1:def 3;
hence x in FinSETS by A6, A1, A10, CLASSES2:57; :: thesis: verum

end;

union (rng g) = X

proof

thus union (rng g) c= X :: according to XBOOLE_0:def 10 :: thesis: X c= union (rng g)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng g) or x in X )
reconsider x9 = x as set by TARSKI:1;
assume x in union (rng g) ; :: thesis: x in X
then consider y being set such that
A11: x9 in y and
A12: y in rng g by TARSKI:def 4;
consider z being object such that
A13: z in dom g and
A14: y = g . z by A12, FUNCT_1:def 3;
y = {(p . z)} by A13, A14, A4, A5;
then x9 = p . z by A11, TARSKI:def 1;
hence x in X by A1, A13, A4, FUNCT_1:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in union (rng g) )
assume x in X ; :: thesis: x in union (rng g)
then consider y being object such that
A15: y in dom p and
A16: x = p . y by A1, FUNCT_1:def 3;
g . y = {x} by A15, A16, A5;
then ( x in {x} & {x} in rng g ) by TARSKI:def 1, A15, A4, FUNCT_1:def 3;
hence x in union (rng g) by TARSKI:def 4; :: thesis: verum

end;

hence X in FinSETS by A7, A2, A4, CLASSES4:5, CLASSES4:43; :: thesis: verum