let B be set ; :: thesis: ( B is cap-closed implies for X being set
for S being finite Subset-Family of X st X in B & S c= B holds
Intersect S in B )
assume A1: B is cap-closed ; :: thesis: for X being set
for S being finite Subset-Family of X st X in B & S c= B holds
Intersect S in B
let X be set ; :: thesis: for S being finite Subset-Family of X st X in B & S c= B holds
Intersect S in B
let S be finite Subset-Family of X; :: thesis: ( X in B & S c= B implies Intersect S in B )
assume that
A2: X in B and
A3: S c= B ; :: thesis: Intersect S in B
defpred S1[ set ] means for sf being Subset-Family of X st sf = $1 holds
Intersect sf in B;
A4: now :: thesis: for x, b being set st x in S & b c= S & S1[b] holds
S1[b \/ {x}]
let x, b be set ; :: thesis: ( x in S & b c= S & S1[b] implies S1[b \/ {x}] )
assume that
A5: x in S and
A6: b c= S and
A7: S1[b] ; :: thesis: S1[b \/ {x}]
thus S1[b \/ {x}] :: thesis: verum
proof
reconsider fx = {x} as Subset-Family of X by A5, ZFMISC_1:31;
reconsider fb = b as Subset-Family of X by A6, XBOOLE_1:1;
reconsider sx = x as Subset of X by A5;
A8: Intersect (fb \/ fx) = (Intersect fb) /\ (Intersect fx) by MSSUBFAM:8
.= (Intersect fb) /\ sx by MSSUBFAM:9 ;
A9: Intersect fb in B by A7;
let sf be Subset-Family of X; :: thesis: ( sf = b \/ {x} implies Intersect sf in B )
assume sf = b \/ {x} ; :: thesis: Intersect sf in B
hence Intersect sf in B by A1, A3, A5, A9, A8; :: thesis: verum
end;
end;
A10: S is finite ;
A11: S1[ {} ] by A2, SETFAM_1:def 9;
S1[S] from FINSET_1:sch 2(A10, A11, A4);
hence Intersect S in B ; :: thesis: verum