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 S1[ 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 & S1[A] holds
S1[A \/ {s}]
let s, A be set ; :: thesis: ( s in S & A c= S & S1[A] implies S1[b2 \/ {b1}] )
assume that
A8: s in S and
A c= S and
A9: S1[A] ; :: thesis: S1[b2 \/ {b1}]
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: S1[b2 \/ {b1}]
hence S1[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: S1[b2 \/ {b1}]
then consider f being Subset-Family of X such that
A10: ( A = {} or ( A <> {} & A = f & Intersect f <> x & Intersect f in B ) ) ;
thus S1[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: S1[A \/ {s}]
hence S1[A \/ {s}] by A4, A6, A8, A12; :: thesis: verum
end;
suppose A13: ( A <> {} & A = f & Intersect f <> x & Intersect f in B ) ; :: thesis: S1[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 S1[A \/ {s}] :: thesis: verum
proof
per cases ( Intersect As <> x or Intersect As = x ) ;
suppose A16: Intersect As <> x ; :: thesis: S1[A \/ {s}]
Intersect As in B by A1, A4, A8, A11, A12, A13, A15, A14;
hence S1[A \/ {s}] by A16; :: thesis: verum
end;
suppose Intersect As = x ; :: thesis: S1[A \/ {s}]
hence S1[A \/ {s}] by A4, A6, A8, A11, A12, A13, A15, A14; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
A17: S1[ {} ] ;
A18: S is finite ;
S1[S] from FINSET_1:sch 2(A18, A17, A7);
hence contradiction by A2, A3, A5, SETFAM_1:def 9; :: thesis: verum