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 4;
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 4;
A3: ( Y is_a_dependent_set_of PA & Y is_a_dependent_set_of PB ) by Th7;
defpred S1[ 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 : S1[X] } as Subset-Family of Y from reconsider XX = XX as Subset-Family of Y ;
Y c= Y ;
then A4: Y in XX by 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 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 y in X1 ; :: thesis: verum
end;
then A5: y in meet XX by ;
then A6: Intersect XX <> {} by SETFAM_1:def 9;
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:
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 A7: Intersect XX is_a_dependent_set_of PA by ;
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:
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 A8: Intersect XX is_a_dependent_set_of PB by ;
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
A9: d c= Intersect XX and
A10: d is_a_dependent_set_of PA and
A11: d is_a_dependent_set_of PB ; :: thesis: d = Intersect XX
consider Ad being set such that
A14: d = union Ad by A10;
A15: d c= Y by ;
per cases ( y in d or not y in d ) ;
suppose y in d ; :: thesis: d = Intersect XX
then A16: d in XX by ;
Intersect XX c= d
proof
let X1 be object ; :: 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 ;
hence X1 in d by ; :: thesis: verum
end;
hence d = Intersect XX by ; :: thesis: verum
end;
suppose A17: not y in d ; :: thesis: d = Intersect XX
reconsider d = d as Subset of Y by ;
d ` = Y \ d by SUBSET_1:def 4;
then A18: y in d ` by ;
d misses d ` by SUBSET_1:24;
then A19: d /\ (d `) = {} by XBOOLE_0:def 7;
d <> Y by A17;
then ( d ` is_a_dependent_set_of PA & d ` is_a_dependent_set_of PB ) by ;
then A20: d ` in XX by A18;
Intersect XX c= d `
proof
let X1 be object ; :: 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 ;
hence X1 in d ` by ; :: thesis: verum
end;
then A21: d /\ () = {} by ;
d /\ d c= d /\ () by ;
then A22: union Ad = {} by ;
consider ad being object such that