let X be set ; :: thesis:
defpred S₁[ Nat] means for F being finite Subset-Family of X st card F = $1 holds
ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) );

A1: now :: thesis:

let n be Nat; :: thesis:
assume A2: S₁[n] ; :: thesis:
thus S₁[n + 1] :: thesis:

let F be finite Subset-Family of X; :: thesis:
assume A3: card F = n + 1 ; :: thesis:

suppose ex g being Subset of X st
( g in F & g c= union (F \ {g}) ) ; :: thesis:

then consider g being Subset of X such that
A4: g in F and
A5: g c= union (F \ {g}) ;
reconsider FF = F \ {g} as finite Subset-Family of X ;
{g} c= F by A4, ZFMISC_1:31;
then A6: F = FF \/ {g} by XBOOLE_1:45;
A7: union F c= union FF

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union F ; :: thesis:
then consider X being set such that
A8: x in X and
A9: X in F by TARSKI:def 4;

per cases by A6, A9, XBOOLE_0:def 3;

suppose X in FF ; :: thesis:

then X c= union FF by ZFMISC_1:74;
hence x in union FF by A8; :: thesis:

end;

suppose X in {g} ; :: thesis:

then X = g by TARSKI:def 1;
hence x in union FF by A5, A8; :: thesis:

end;

end;

end;

g in {g} by TARSKI:def 1;
then not g in FF by XBOOLE_0:def 5;
then card (FF \/ {g}) = (card FF) + 1 by CARD_2:41;
then consider G being finite Subset-Family of X such that
A10: G c= FF and
A11: union G = union FF and
A12: for g being Subset of X st g in G holds
not g c= union (G \ {g}) by A2, A3, A6, XCMPLX_1:2;
take G ; :: thesis:
FF c= F by A6, XBOOLE_1:7;
hence G c= F by A10; :: thesis:
union FF c= union F by A6, XBOOLE_1:7, ZFMISC_1:77;
hence union G = union F by A11, A7; :: thesis:
thus for g being Subset of X st g in G holds
not g c= union (G \ {g}) by A12; :: thesis:

end;

suppose A13: for g being Subset of X holds
( not g in F or not g c= union (F \ {g}) ) ; :: thesis:

take G = F; :: thesis:
thus G c= F ; :: thesis:
thus union G = union F ; :: thesis:
thus for g being Subset of X st g in G holds
not g c= union (G \ {g}) by A13; :: thesis:

end;

end;

end;

end;

let F be finite Subset-Family of X; :: thesis:
A14: card F = card F ;
A15: S₁[ 0 ]

let F be finite Subset-Family of X; :: thesis:
assume A16: card F = 0 ; :: thesis:
take G = F; :: thesis:
thus G c= F ; :: thesis:
thus union G = union F ; :: thesis:
thus for g being Subset of X st g in G holds
not g c= union (G \ {g}) by A16; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A15, A1);
hence ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) ) by A14; :: thesis: