let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for y being Element of Y st G <> {} holds
ex X being Subset of Y st
( y in X & X is_upper_min_depend_of G )
let G be Subset of (PARTITIONS Y); :: thesis: for y being Element of Y st G <> {} holds
ex X being Subset of Y st
( y in X & X is_upper_min_depend_of G )
let y be Element of Y; :: thesis: ( G <> {} implies ex X being Subset of Y st
( y in X & X is_upper_min_depend_of G ) )
defpred S₁[ set ] means ( y in $1 & ( for d being a_partition of Y st d in G holds
$1 is_a_dependent_set_of d ) );
reconsider XX = { X where X is Subset of Y : S₁[X] } as Subset-Family of Y from DOMAIN_1:sch 7();
reconsider XX = XX as Subset-Family of Y ;
assume G <> {} ; :: thesis: ex X being Subset of Y st
( y in X & X is_upper_min_depend_of G )
then consider g being object such that
A1: g in G by XBOOLE_0:def 1;
reconsider g = g as a_partition of Y by A1, PARTIT1:def 3;
A2: union g = Y by EQREL_1:def 4;
take Intersect XX ; :: thesis: ( y in Intersect XX & Intersect XX is_upper_min_depend_of G )
( Y c= Y & ( for d being a_partition of Y st d in G holds
Y is_a_dependent_set_of d ) ) by PARTIT1:7;
then A3: Y in XX ;
A4: for A being set st A in g holds
( A <> {} & ( for B being set holds
( not B in g or A = B or A misses B ) ) ) by EQREL_1:def 4;
A5: for e being set st e c= Intersect XX & ( for d being a_partition of Y st d in G holds
e is_a_dependent_set_of d ) holds
e = Intersect XX

proof

let e be set ; :: thesis: ( e c= Intersect XX & ( for d being a_partition of Y st d in G holds
e is_a_dependent_set_of d ) implies e = Intersect XX )
assume that
A6: e c= Intersect XX and
A7: for d being a_partition of Y st d in G holds
e is_a_dependent_set_of d ; :: thesis: e = Intersect XX
consider Ad being set such that
A8: Ad c= g and
A9: Ad <> {} and
A10: e = union Ad by A1, A7, PARTIT1:def 1;
A11: e c= Y by A2, A8, A10, ZFMISC_1:77;

per cases ( y in e or not y in e ) ;

suppose y in e ; :: thesis: e = Intersect XX

then A12: e in XX by A7, A11;
Intersect XX c= e

proof

let X1 be object ; :: according to TARSKI:def 3 :: thesis: ( not X1 in Intersect XX or X1 in e )
assume X1 in Intersect XX ; :: thesis: X1 in e
then X1 in meet XX by A3, SETFAM_1:def 9;
hence X1 in e by A12, SETFAM_1:def 1; :: thesis: verum

end;

hence e = Intersect XX by A6, XBOOLE_0:def 10; :: thesis: verum

end;

suppose A13: not y in e ; :: thesis: e = Intersect XX

reconsider e = e as Subset of Y by A2, A8, A10, ZFMISC_1:77;
e ` = Y \ e by SUBSET_1:def 4;
then A14: y in e ` by A13, XBOOLE_0:def 5;
e <> Y by A13;
then for d being a_partition of Y st d in G holds
e ` is_a_dependent_set_of d by A7, PARTIT1:10;
then A15: e ` in XX by A14;
A16: Intersect XX c= e `

proof

let X1 be object ; :: according to TARSKI:def 3 :: thesis: ( not X1 in Intersect XX or X1 in e ` )
assume X1 in Intersect XX ; :: thesis: X1 in e `
then X1 in meet XX by A3, SETFAM_1:def 9;
hence X1 in e ` by A15, SETFAM_1:def 1; :: thesis: verum

end;

A17: e /\ e = e ;
consider ad being object such that
A18: ad in Ad by A9, XBOOLE_0:def 1;
reconsider ad = ad as set by TARSKI:1;
e /\ (e `) = {} by SUBSET_1:24, XBOOLE_0:def 7;
then e /\ (Intersect XX) = {} by A16, XBOOLE_1:3, XBOOLE_1:26;
then e c= {} by A6, A17, XBOOLE_1:26;
then union Ad = {} by A10;
then A19: ad c= {} by A18, ZFMISC_1:74;
ad <> {} by A4, A8, A18;
hence e = Intersect XX by A19; :: thesis: verum

end;

end;

end;

for X1 being set st X1 in XX holds
y in X1

proof

let X1 be set ; :: thesis: ( X1 in XX implies y in X1 )
assume X1 in XX ; :: thesis: y in X1
then ex X being Subset of Y st
( X = X1 & y in X & ( for d being a_partition of Y st d in G holds
X is_a_dependent_set_of d ) ) ;
hence y in X1 ; :: thesis: verum

end;

then A20: y in meet XX by A3, SETFAM_1:def 1;
then A21: Intersect XX <> {} by SETFAM_1:def 9;
for d being a_partition of Y st d in G holds
Intersect XX is_a_dependent_set_of d

proof

let d be a_partition of Y; :: thesis: ( d in G implies Intersect XX is_a_dependent_set_of d )
assume A22: d in G ; :: thesis: Intersect XX is_a_dependent_set_of d
for X1 being set st X1 in XX holds
X1 is_a_dependent_set_of d

proof

let X1 be set ; :: thesis: ( X1 in XX implies X1 is_a_dependent_set_of d )
assume X1 in XX ; :: thesis: X1 is_a_dependent_set_of d
then ex X being Subset of Y st
( X = X1 & y in X & ( for d being a_partition of Y st d in G holds
X is_a_dependent_set_of d ) ) ;
hence X1 is_a_dependent_set_of d by A22; :: thesis: verum

end;

hence Intersect XX is_a_dependent_set_of d by A21, PARTIT1:8; :: thesis: verum

end;

hence ( y in Intersect XX & Intersect XX is_upper_min_depend_of G ) by A3, A20, A5, SETFAM_1:def 9; :: thesis: verum