let Y be non empty set ; :: thesis:
let G be Subset of (PARTITIONS Y); :: thesis:
let y be Element of Y; :: thesis:
assume G <> {} ; :: thesis:
then consider g being set 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 & ( 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 6;
A3: Y c= Y ;
A4: for d being a_partition of Y st d in G holds
Y is_a_dependent_set_of d by PARTIT1:9;
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 ;
A5: Y in XX by A3, A4;
for X1 being set st X1 in XX holds
y in X1

let X1 be set ; :: thesis:
assume X1 in XX ; :: thesis:
then consider X being Subset of Y such that
A6: ( X = X1 & y in X & ( for d being a_partition of Y st d in G holds
X is_a_dependent_set_of d ) ) ;
thus y in X1 by A6; :: thesis:

end;

then A7: y in meet XX by A5, SETFAM_1:def 1;
then A8: Intersect XX <> {} by SETFAM_1:def 10;
take Intersect XX ; :: thesis:
A9: for d being a_partition of Y st d in G holds
Intersect XX is_a_dependent_set_of d

let d be a_partition of Y; :: thesis:
assume A10: d in G ; :: thesis:
for X1 being set st X1 in XX holds
X1 is_a_dependent_set_of d

let X1 be set ; :: thesis:
assume X1 in XX ; :: thesis:
then consider X being Subset of Y such that
A11: ( X = X1 & y in X & ( for d being a_partition of Y st d in G holds
X is_a_dependent_set_of d ) ) ;
thus X1 is_a_dependent_set_of d by A10, A11; :: thesis:

end;

hence Intersect XX is_a_dependent_set_of d by A8, PARTIT1:10; :: thesis:

end;

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

let e be set ; :: thesis:
assume A12: ( e c= Intersect XX & ( for d being a_partition of Y st d in G holds
e is_a_dependent_set_of d ) ) ; :: thesis:
then e is_a_dependent_set_of g by A1;
then consider Ad being set such that
A13: ( Ad c= g & Ad <> {} & e = union Ad ) by PARTIT1:def 1;
A14: e c= Y by A2, A13, ZFMISC_1:95;

per cases ;

suppose y in e ; :: thesis:

then A15: e in XX by A12, A14;
Intersect XX c= e

let X1 be set ; :: according to TARSKI:def 3 :: thesis:
assume X1 in Intersect XX ; :: thesis:
then X1 in meet XX by A5, SETFAM_1:def 10;
hence X1 in e by A15, SETFAM_1:def 1; :: thesis:

end;

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

end;

suppose A16: not y in e ; :: thesis:

reconsider e = e as Subset of Y by A2, A13, ZFMISC_1:95;
e ` = Y \ e by SUBSET_1:def 5;
then A17: y in e ` by A16, XBOOLE_0:def 5;
e misses e ` by SUBSET_1:44;
then A18: e /\ (e ` ) = {} by XBOOLE_0:def 7;
e <> Y by A16;
then for d being a_partition of Y st d in G holds
e ` is_a_dependent_set_of d by A12, PARTIT1:12;
then A19: e ` in XX by A17;
Intersect XX c= e `

let X1 be set ; :: according to TARSKI:def 3 :: thesis:
assume X1 in Intersect XX ; :: thesis:
then X1 in meet XX by A5, SETFAM_1:def 10;
hence X1 in e ` by A19, SETFAM_1:def 1; :: thesis:

end;

then A20: e /\ (Intersect XX) = {} by A18, XBOOLE_1:3, XBOOLE_1:26;
e /\ e = e ;
then e c= {} by A12, A20, XBOOLE_1:26;
then A21: union Ad = {} by A13;
consider ad being set such that
A22: ad in Ad by A13, XBOOLE_0:def 1;
A23: ad <> {} by A2, A13, A22;
A24: ad c= {} by A21, A22, ZFMISC_1:92;
consider add being set such that
A25: add in ad by A23, XBOOLE_0:def 1;
thus e = Intersect XX by A24, A25; :: thesis:

end;

hence ( y in Intersect XX & Intersect XX is_upper_min_depend_of G ) by A5, A7, A9, Def2, SETFAM_1:def 10; :: thesis: