let B be set ; :: thesis: ( B is (B2) 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 (B2) ; :: 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 S₁[ set ] means for sf being Subset-Family of X st sf = $1 holds
Intersect sf in B;
A4: S is finite ;
A5: S₁[ {} ] by A2, SETFAM_1:def 10;

A6: now

let x, b be set ; :: thesis: ( x in S & b c= S & S₁[b] implies S₁[b \/ {x}] )
assume that
A7: x in S and
A8: b c= S and
A9: S₁[b] ; :: thesis: S₁[b \/ {x}]
thus S₁[b \/ {x}] :: thesis: verum

proof

let sf be Subset-Family of X; :: thesis: ( sf = b \/ {x} implies Intersect sf in B )
assume A10: sf = b \/ {x} ; :: thesis: Intersect sf in B
reconsider sx = x as Subset of X by A7;
reconsider fb = b as Subset-Family of X by A8, XBOOLE_1:1;
reconsider fx = {x} as Subset-Family of X by A7, ZFMISC_1:37;
A11: Intersect fb in B by A9;
Intersect (fb \/ fx) = (Intersect fb) /\ (Intersect fx) by MSSUBFAM:8
.= (Intersect fb) /\ sx by MSSUBFAM:9 ;
hence Intersect sf in B by A1, A3, A7, A10, A11, FINSUB_1:def 2; :: thesis: verum

end;

end;

S₁[S] from FINSET_1:sch 2(A4, A5, A6);
hence Intersect S in B ; :: thesis: verum