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 S_{1}[ 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_{1}[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 A3;

for X1 being set st X1 in XX holds

y in X1

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

for X1 being set st X1 in XX holds

X1 is_a_dependent_set_of PB

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

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 S

reconsider XX = { X where X is Subset of Y : S

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

then A5:
y in meet XX
by A4, SETFAM_1:def 1;
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;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

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

then A7:
Intersect XX is_a_dependent_set_of PA
by A6, Th8;
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;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

for X1 being set st X1 in XX holds

X1 is_a_dependent_set_of PB

proof

then A8:
Intersect XX is_a_dependent_set_of PB
by A6, Th8;
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;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

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

hence
( y in Intersect XX & Intersect XX is_min_depend PA,PB )
by A4, A5, A7, A8, SETFAM_1:def 9; :: thesis: verum
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

A12: Ad c= PA and

A13: Ad <> {} and

A14: d = union Ad by A10;

A15: d c= Y by A1, A12, A14, ZFMISC_1:77;

end;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

A12: Ad c= PA and

A13: Ad <> {} and

A14: d = union Ad by A10;

A15: d c= Y by A1, A12, A14, ZFMISC_1:77;

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

end;

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

then A16:
d in XX
by A10, A11, A15;

Intersect XX c= d

end;Intersect XX c= d

proof

hence
d = Intersect XX
by A9, XBOOLE_0:def 10; :: thesis: verum
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 A4, SETFAM_1:def 9;

hence X1 in d by A16, SETFAM_1:def 1; :: thesis: verum

end;assume X1 in Intersect XX ; :: thesis: X1 in d

then X1 in meet XX by A4, SETFAM_1:def 9;

hence X1 in d by A16, SETFAM_1:def 1; :: thesis: verum

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

reconsider d = d as Subset of Y by A1, A12, A14, ZFMISC_1:77;

d ` = Y \ d by SUBSET_1:def 4;

then A18: y in d ` by A17, XBOOLE_0:def 5;

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 A10, A11, Th10;

then A20: d ` in XX by A18;

Intersect XX c= d `

d /\ d c= d /\ (Intersect XX) by A9, XBOOLE_1:26;

then A22: union Ad = {} by A14, A21;

consider ad being object such that

A23: ad in Ad by A13, XBOOLE_0:def 1;

A24: ad <> {} by A2, A12, A23;

reconsider ad = ad as set by TARSKI:1;

ad c= {} by A22, A23, ZFMISC_1:74;

hence d = Intersect XX by A24; :: thesis: verum

end;d ` = Y \ d by SUBSET_1:def 4;

then A18: y in d ` by A17, XBOOLE_0:def 5;

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 A10, A11, Th10;

then A20: d ` in XX by A18;

Intersect XX c= d `

proof

then A21:
d /\ (Intersect XX) = {}
by A19, XBOOLE_1:3, XBOOLE_1:26;
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 A4, SETFAM_1:def 9;

hence X1 in d ` by A20, SETFAM_1:def 1; :: thesis: verum

end;assume X1 in Intersect XX ; :: thesis: X1 in d `

then X1 in meet XX by A4, SETFAM_1:def 9;

hence X1 in d ` by A20, SETFAM_1:def 1; :: thesis: verum

d /\ d c= d /\ (Intersect XX) by A9, XBOOLE_1:26;

then A22: union Ad = {} by A14, A21;

consider ad being object such that

A23: ad in Ad by A13, XBOOLE_0:def 1;

A24: ad <> {} by A2, A12, A23;

reconsider ad = ad as set by TARSKI:1;

ad c= {} by A22, A23, ZFMISC_1:74;

hence d = Intersect XX by A24; :: thesis: verum