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 by EQREL_1:def 6;
A2: 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;
A3: ( Y is_a_dependent_set_of PA & 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 ;
A4: Y c= Y ;
A5: Y in XX by A3, A4;
A6: 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 A7: X1 in XX ; :: thesis: y in X1
A8: 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 ) by A7;
thus y in X1 by A8; :: thesis: verum

end;

A9: y in meet XX by A5, A6, SETFAM_1:def 1;
A10: Intersect XX <> {} by A9, SETFAM_1:def 10;
take Intersect XX ; :: thesis: ( y in Intersect XX & Intersect XX is_min_depend PA,PB )
A11: 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 A12: X1 in XX ; :: thesis: X1 is_a_dependent_set_of PA
A13: 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 ) by A12;
thus X1 is_a_dependent_set_of PA by A13; :: thesis: verum

end;

A14: Intersect XX is_a_dependent_set_of PA by A10, A11, Th10;
A15: 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 A16: X1 in XX ; :: thesis: X1 is_a_dependent_set_of PB
A17: 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 ) by A16;
thus X1 is_a_dependent_set_of PB by A17; :: thesis: verum

end;

A18: Intersect XX is_a_dependent_set_of PB by A10, A15, Th10;
A19: 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 that
A20: d c= Intersect XX and
A21: d is_a_dependent_set_of PA and
A22: d is_a_dependent_set_of PB ; :: thesis: d = Intersect XX
consider Ad being set such that
A23: Ad c= PA and
A24: Ad <> {} and
A25: d = union Ad by A21, Def1;
A26: d c= Y by A1, A23, A25, ZFMISC_1:95;

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

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

A28: d in XX by A21, A22, A26, A27;
A29: 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 A30: X1 in Intersect XX ; :: thesis: X1 in d
A31: X1 in meet XX by A5, A30, SETFAM_1:def 10;
thus X1 in d by A28, A31, SETFAM_1:def 1; :: thesis: verum

end;

thus d = Intersect XX by A20, A29, XBOOLE_0:def 10; :: thesis: verum

end;

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

reconsider d = d as Subset of Y by A1, A23, A25, ZFMISC_1:95;
A33: d ` = Y \ d by SUBSET_1:def 5;
A34: y in d ` by A32, A33, XBOOLE_0:def 5;
A35: d misses d ` by SUBSET_1:44;
A36: d /\ (d ` ) = {} by A35, XBOOLE_0:def 7;
A37: d <> Y by A32;
A38: ( d ` is_a_dependent_set_of PA & d ` is_a_dependent_set_of PB ) by A21, A22, A37, Th12;
A39: d ` in XX by A34, A38;
A40: 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 A41: X1 in Intersect XX ; :: thesis: X1 in d `
A42: X1 in meet XX by A5, A41, SETFAM_1:def 10;
thus X1 in d ` by A39, A42, SETFAM_1:def 1; :: thesis: verum

end;

A43: d /\ (Intersect XX) = {} by A36, A40, XBOOLE_1:3, XBOOLE_1:26;
A44: d /\ d c= d /\ (Intersect XX) by A20, XBOOLE_1:26;
A45: union Ad = {} by A25, A43, A44;
consider ad being set such that
A46: ad in Ad by A24, XBOOLE_0:def 1;
A47: ad <> {} by A2, A23, A46;
A48: ad c= {} by A45, A46, ZFMISC_1:92;
thus d = Intersect XX by A47, A48; :: thesis: verum

end;

end;

end;

thus ( y in Intersect XX & Intersect XX is_min_depend PA,PB ) by A5, A9, A14, A18, A19, Def2, SETFAM_1:def 10; :: thesis: verum