let X be set ; :: thesis: for F being finite Subset-Family of X 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}) ) )
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: S₁[ 0 ]

proof

let F be finite Subset-Family of X; :: thesis: ( card F = 0 implies 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}) ) ) )
assume A2: card F = 0 ; :: thesis: 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}) ) )
take G = F; :: thesis: ( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
thus G c= F ; :: thesis: ( union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
thus union G = union F ; :: thesis: for g being Subset of X st g in G holds
not g c= union (G \ {g})
thus for g being Subset of X st g in G holds
not g c= union (G \ {g}) by A2; :: thesis: verum

end;

A3: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

proof

let F be finite Subset-Family of X; :: thesis: ( card F = n + 1 implies 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}) ) ) )
assume A5: card F = n + 1 ; :: thesis: 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}) ) )

per cases ( ex g being Subset of X st
( g in F & g c= union (F \ {g}) ) or for g being Subset of X holds
( not g in F or not g c= union (F \ {g}) ) ) ;

suppose ex g being Subset of X st
( g in F & g c= union (F \ {g}) ) ; :: thesis: 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}) ) )

then consider g being Subset of X such that
A6: ( g in F & g c= union (F \ {g}) ) ;
reconsider FF = F \ {g} as finite Subset-Family of X ;
{g} c= F by A6, ZFMISC_1:37;
then A7: F = FF \/ {g} by XBOOLE_1:45;
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:54;
then consider G being finite Subset-Family of X such that
A8: G c= FF and
A9: union G = union FF and
A10: for g being Subset of X st g in G holds
not g c= union (G \ {g}) by A4, A5, A7, XCMPLX_1:2;
take G ; :: thesis: ( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
FF c= F by A7, XBOOLE_1:7;
hence G c= F by A8, XBOOLE_1:1; :: thesis: ( union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
A11: union FF c= union F by A7, XBOOLE_1:7, ZFMISC_1:95;
union F c= union FF

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union F or x in union FF )
assume x in union F ; :: thesis: x in union FF
then consider X being set such that
A12: ( x in X & X in F ) by TARSKI:def 4;

per cases ( X in FF or X in {g} ) by A7, A12, XBOOLE_0:def 3;

suppose X in FF ; :: thesis: x in union FF

then X c= union FF by ZFMISC_1:92;
hence x in union FF by A12; :: thesis: verum

end;

suppose X in {g} ; :: thesis: x in union FF

then X = g by TARSKI:def 1;
hence x in union FF by A6, A12; :: thesis: verum

end;

end;

end;

hence union G = union F by A9, A11, XBOOLE_0:def 10; :: thesis: for g being Subset of X st g in G holds
not g c= union (G \ {g})
thus for g being Subset of X st g in G holds
not g c= union (G \ {g}) by A10; :: thesis: verum

end;

suppose A13: for g being Subset of X holds
( not g in F or not g c= union (F \ {g}) ) ; :: thesis: 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}) ) )

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

end;

end;

end;

end;

A14: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
let F be finite Subset-Family of X; :: thesis: 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}) ) )
card F = card F ;
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: verum