defpred S₁[ set , set ] means $1 in $2;
let X be set ; :: thesis: for F being Subset-Family of X st F is finite holds
for A being Subset of X st not A is finite & A c= union F holds
ex Y being Subset of X st
( Y in F & not Y /\ A is finite )
let F be Subset-Family of X; :: thesis: ( F is finite implies for A being Subset of X st not A is finite & A c= union F holds
ex Y being Subset of X st
( Y in F & not Y /\ A is finite ) )
assume A1: F is finite ; :: thesis: for A being Subset of X st not A is finite & A c= union F holds
ex Y being Subset of X st
( Y in F & not Y /\ A is finite )
let A be Subset of X; :: thesis: ( not A is finite & A c= union F implies ex Y being Subset of X st
( Y in F & not Y /\ A is finite ) )
assume that
A2: not A is finite and
A3: A c= union F ; :: thesis: ex Y being Subset of X st
( Y in F & not Y /\ A is finite )
set I = INTERSECTION F,{A};
card [:F,{A}:] = card F by CARD_2:13;
then card (INTERSECTION F,{A}) c= card F by TOPGEN_4:25;
then A4: INTERSECTION F,{A} is finite by A1;
A5: for x being set st x in A holds
ex y being set st
( y in INTERSECTION F,{A} & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in A implies ex y being set st
( y in INTERSECTION F,{A} & S₁[x,y] ) )
assume A6: x in A ; :: thesis: ex y being set st
( y in INTERSECTION F,{A} & S₁[x,y] )
consider y being set such that
A7: x in y and
A8: y in F by A3, A6, TARSKI:def 4;
take y /\ A ; :: thesis: ( y /\ A in INTERSECTION F,{A} & S₁[x,y /\ A] )
A in {A} by TARSKI:def 1;
hence ( y /\ A in INTERSECTION F,{A} & S₁[x,y /\ A] ) by A6, A7, A8, SETFAM_1:def 5, XBOOLE_0:def 4; :: thesis: verum

end;

consider p being Function of A,(INTERSECTION F,{A}) such that
A9: for x being set st x in A holds
S₁[x,p . x] from FUNCT_2:sch 1(A5);
consider x being set such that
A10: x in A by A2, XBOOLE_0:def 1;
ex y being set st
( y in INTERSECTION F,{A} & S₁[x,y] ) by A5, A10;
then dom p = A by FUNCT_2:def 1;
then consider t being set such that
A11: t in rng p and
A12: not p " {t} is finite by A2, A4, Th24;
consider Y, Z being set such that
A13: Y in F and
A14: Z in {A} and
A15: t = Y /\ Z by A11, SETFAM_1:def 5;
reconsider Y = Y as Subset of X by A13;
take Y ; :: thesis: ( Y in F & not Y /\ A is finite )
A16: Z = A by A14, TARSKI:def 1;
p " {t} c= Y /\ A

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in p " {t} or z in Y /\ A )
assume A17: z in p " {t} ; :: thesis: z in Y /\ A
p . z in {t} by A17, FUNCT_1:def 13;
then p . z = t by TARSKI:def 1;
hence z in Y /\ A by A9, A15, A16, A17; :: thesis: verum

end;

hence ( Y in F & not Y /\ A is finite ) by A12, A13; :: thesis: verum