let Y be non empty set ; :: thesis: for PA, PB being a_partition of Y
for y being Element of Y ex X being Subset of Y st
( y in X & X is_min_depend PA,PB )
let PA, PB be a_partition of Y; :: thesis: for y being Element of Y ex X being Subset of Y st
( y in X & X is_min_depend PA,PB )
let y be Element of Y; :: thesis: ex X being Subset of Y st
( y in X & X is_min_depend PA,PB )
A1: ( union PA = Y & ( for A being set st A in PA holds
( A <> {} & ( for B being set holds
( not B in PA or A = B or A misses B ) ) ) ) ) by EQREL_1:def 6;
A2: Y is_a_dependent_set_of PA by Th9;
A3: Y is_a_dependent_set_of PB by Th9;
defpred S₁[ set ] means ( y in $1 & $1 is_a_dependent_set_of PA & $1 is_a_dependent_set_of PB );
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 ;
Y c= Y ;
then A4: Y in XX by A2, A3;
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 consider X being Subset of Y such that
A5: ( X = X1 & y in X & X is_a_dependent_set_of PA & X is_a_dependent_set_of PB ) ;
thus y in X1 by A5; :: thesis: verum

end;

then A6: y in meet XX by A4, SETFAM_1:def 1;
then A7: Intersect XX <> {} by SETFAM_1:def 10;
take Intersect XX ; :: thesis: ( y in Intersect XX & Intersect XX is_min_depend PA,PB )
for X1 being set st X1 in XX holds
X1 is_a_dependent_set_of PA

proof

let X1 be set ; :: thesis: ( X1 in XX implies X1 is_a_dependent_set_of PA )
assume X1 in XX ; :: thesis: X1 is_a_dependent_set_of PA
then ex X being Subset of Y st
( X = X1 & y in X & X is_a_dependent_set_of PA & X is_a_dependent_set_of PB ) ;
hence X1 is_a_dependent_set_of PA ; :: thesis: verum

end;

then A8: Intersect XX is_a_dependent_set_of PA by A7, Th10;
for X1 being set st X1 in XX holds
X1 is_a_dependent_set_of PB

proof

let X1 be set ; :: thesis: ( X1 in XX implies X1 is_a_dependent_set_of PB )
assume X1 in XX ; :: thesis: X1 is_a_dependent_set_of PB
then ex X being Subset of Y st
( X = X1 & y in X & X is_a_dependent_set_of PA & X is_a_dependent_set_of PB ) ;
hence X1 is_a_dependent_set_of PB ; :: thesis: verum

end;

then A9: Intersect XX is_a_dependent_set_of PB by A7, Th10;
for d being set st d c= Intersect XX & d is_a_dependent_set_of PA & d is_a_dependent_set_of PB holds
d = Intersect XX

proof

let d be set ; :: thesis: ( d c= Intersect XX & d is_a_dependent_set_of PA & d is_a_dependent_set_of PB implies d = Intersect XX )
assume A10: ( d c= Intersect XX & d is_a_dependent_set_of PA & d is_a_dependent_set_of PB ) ; :: thesis: d = Intersect XX
then consider Ad being set such that
A11: ( Ad c= PA & Ad <> {} & d = union Ad ) by Def1;
A12: d c= Y by A1, A11, ZFMISC_1:95;

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

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

then A13: d in XX by A10, A12;
Intersect XX c= d

proof

let X1 be set ; :: according to TARSKI:def 3 :: thesis: ( not X1 in Intersect XX or X1 in d )
assume X1 in Intersect XX ; :: thesis: X1 in d
then X1 in meet XX by A4, SETFAM_1:def 10;
hence X1 in d by A13, SETFAM_1:def 1; :: thesis: verum

end;

hence d = Intersect XX by A10, XBOOLE_0:def 10; :: thesis: verum

end;

suppose A14: not y in d ; :: thesis: d = Intersect XX

reconsider d = d as Subset of Y by A1, A11, ZFMISC_1:95;
d ` = Y \ d by SUBSET_1:def 5;
then A15: y in d ` by A14, XBOOLE_0:def 5;
d misses d ` by SUBSET_1:44;
then A16: d /\ (d ` ) = {} by XBOOLE_0:def 7;
A17: d <> Y by A14;
then A18: d ` is_a_dependent_set_of PA by A10, Th12;
d ` is_a_dependent_set_of PB by A10, A17, Th12;
then A19: d ` in XX by A15, A18;
Intersect XX c= d `

proof

let X1 be set ; :: according to TARSKI:def 3 :: thesis: ( not X1 in Intersect XX or X1 in d ` )
assume X1 in Intersect XX ; :: thesis: X1 in d `
then X1 in meet XX by A4, SETFAM_1:def 10;
hence X1 in d ` by A19, SETFAM_1:def 1; :: thesis: verum

end;

then A20: d /\ (Intersect XX) = {} by A16, XBOOLE_1:3, XBOOLE_1:26;
d /\ d c= d /\ (Intersect XX) by A10, XBOOLE_1:26;
then A21: union Ad = {} by A11, A20;
consider ad being set such that
A22: ad in Ad by A11, XBOOLE_0:def 1;
A23: ad <> {} by A1, A11, A22;
A24: ad c= {} by A21, A22, ZFMISC_1:92;
ex add being set st add in ad by A23, XBOOLE_0:def 1;
hence d = Intersect XX by A24; :: thesis: verum

end;

end;

end;

hence ( y in Intersect XX & Intersect XX is_min_depend PA,PB ) by A4, A6, A8, A9, Def2, SETFAM_1:def 10; :: thesis: verum