let X be set ; :: thesis: for B being non empty Subset-Family of X st B is cap-closed holds
for x being Element of B st x is_/\-irreducible_in B & x <> X holds
for S being finite Subset-Family of X st S c= B & x = Intersect S holds
x in S
let B be non empty Subset-Family of X; :: thesis: ( B is cap-closed implies for x being Element of B st x is_/\-irreducible_in B & x <> X holds
for S being finite Subset-Family of X st S c= B & x = Intersect S holds
x in S )
assume A1: B is (B2) ; :: thesis: for x being Element of B st x is_/\-irreducible_in B & x <> X holds
for S being finite Subset-Family of X st S c= B & x = Intersect S holds
x in S
let x be Element of B; :: thesis: ( x is_/\-irreducible_in B & x <> X implies for S being finite Subset-Family of X st S c= B & x = Intersect S holds
x in S )
assume that
A2: x is_/\-irreducible_in B and
A3: x <> X ; :: thesis: for S being finite Subset-Family of X st S c= B & x = Intersect S holds
x in S
defpred S₁[ set ] means ( ex a, b being Element of B st
( x <> a & x <> b & x = a /\ b ) or ex f being Subset-Family of X st
( $1 = {} or ( $1 <> {} & $1 = f & Intersect f <> x & Intersect f in B ) ) );
let S be finite Subset-Family of X; :: thesis: ( S c= B & x = Intersect S implies x in S )
assume that
A4: S c= B and
A5: x = Intersect S and
A6: not x in S ; :: thesis: contradiction

A7: now :: thesis: for s, A being set st s in S & A c= S & S₁[A] holds
S₁[A \/ {s}]

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

per cases ( ex a, b being Element of B st
( x <> a & x <> b & x = a /\ b ) or ex f being Subset-Family of X st
( A = {} or ( A = f & Intersect f <> x & Intersect f in B ) ) ) by A9;

suppose ex a, b being Element of B st
( x <> a & x <> b & x = a /\ b ) ; :: thesis: S₁[b₂ \/ {b₁}]

hence S₁[A \/ {s}] ; :: thesis: verum

end;

suppose ex f being Subset-Family of X st
( A = {} or ( A = f & Intersect f <> x & Intersect f in B ) ) ; :: thesis: S₁[b₂ \/ {b₁}]

then consider f being Subset-Family of X such that
A10: ( A = {} or ( A <> {} & A = f & Intersect f <> x & Intersect f in B ) ) ;
thus S₁[A \/ {s}] :: thesis: verum

proof

reconsider sf = {s} as Subset-Family of X by A8, ZFMISC_1:31;
A11: Intersect sf = meet sf by SETFAM_1:def 9;
then A12: Intersect sf = s by SETFAM_1:10;

per cases ( A = {} or ( A <> {} & A = f & Intersect f <> x & Intersect f in B ) ) by A10;

suppose A = {} ; :: thesis: S₁[A \/ {s}]

hence S₁[A \/ {s}] by A4, A6, A8, A12; :: thesis: verum

end;

suppose A13: ( A <> {} & A = f & Intersect f <> x & Intersect f in B ) ; :: thesis: S₁[A \/ {s}]

then reconsider As = A \/ sf as non empty Subset-Family of X by XBOOLE_1:8;
A14: Intersect As = meet As by SETFAM_1:def 9
.= (meet A) /\ (meet sf) by A13, SETFAM_1:9 ;
A15: Intersect f = meet f by A13, SETFAM_1:def 9;
thus S₁[A \/ {s}] :: thesis: verum

proof

per cases ( Intersect As <> x or Intersect As = x ) ;

suppose A16: Intersect As <> x ; :: thesis: S₁[A \/ {s}]

Intersect As in B by A1, A4, A8, A11, A12, A13, A15, A14;
hence S₁[A \/ {s}] by A16; :: thesis: verum

end;

suppose Intersect As = x ; :: thesis: S₁[A \/ {s}]

hence S₁[A \/ {s}] by A4, A6, A8, A11, A12, A13, A15, A14; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

A17: S₁[ {} ] ;
A18: S is finite ;
S₁[S] from FINSET_1:sch 2(A18, A17, A7);
hence contradiction by A2, A3, A5, SETFAM_1:def 9; :: thesis: verum