let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)

for y being Element of Y st G <> {} holds

ex X being Subset of Y st

( y in X & X is_upper_min_depend_of G )

let G be Subset of (PARTITIONS Y); :: thesis: for y being Element of Y st G <> {} holds

ex X being Subset of Y st

( y in X & X is_upper_min_depend_of G )

let y be Element of Y; :: thesis: ( G <> {} implies ex X being Subset of Y st

( y in X & X is_upper_min_depend_of G ) )

defpred S_{1}[ 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_{1}[X] } as Subset-Family of Y from DOMAIN_1:sch 7();

reconsider XX = XX as Subset-Family of Y ;

assume G <> {} ; :: thesis: ex X being Subset of Y st

( y in X & X is_upper_min_depend_of G )

then consider g being object 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 by EQREL_1:def 4;

take Intersect XX ; :: thesis: ( y in Intersect XX & Intersect XX is_upper_min_depend_of G )

( Y c= Y & ( for d being a_partition of Y st d in G holds

Y is_a_dependent_set_of d ) ) by PARTIT1:7;

then A3: Y in XX ;

A4: 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 4;

A5: 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

y in X1

then A21: Intersect XX <> {} by SETFAM_1:def 9;

for d being a_partition of Y st d in G holds

Intersect XX is_a_dependent_set_of d

for y being Element of Y st G <> {} holds

ex X being Subset of Y st

( y in X & X is_upper_min_depend_of G )

let G be Subset of (PARTITIONS Y); :: thesis: for y being Element of Y st G <> {} holds

ex X being Subset of Y st

( y in X & X is_upper_min_depend_of G )

let y be Element of Y; :: thesis: ( G <> {} implies ex X being Subset of Y st

( y in X & X is_upper_min_depend_of G ) )

defpred S

$1 is_a_dependent_set_of d ) );

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

reconsider XX = XX as Subset-Family of Y ;

assume G <> {} ; :: thesis: ex X being Subset of Y st

( y in X & X is_upper_min_depend_of G )

then consider g being object 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 by EQREL_1:def 4;

take Intersect XX ; :: thesis: ( y in Intersect XX & Intersect XX is_upper_min_depend_of G )

( Y c= Y & ( for d being a_partition of Y st d in G holds

Y is_a_dependent_set_of d ) ) by PARTIT1:7;

then A3: Y in XX ;

A4: 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 4;

A5: 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

proof

for X1 being set st X1 in XX holds
let e be set ; :: thesis: ( e c= Intersect XX & ( for d being a_partition of Y st d in G holds

e is_a_dependent_set_of d ) implies e = Intersect XX )

assume that

A6: e c= Intersect XX and

A7: for d being a_partition of Y st d in G holds

e is_a_dependent_set_of d ; :: thesis: e = Intersect XX

consider Ad being set such that

A8: Ad c= g and

A9: Ad <> {} and

A10: e = union Ad by A1, A7, PARTIT1:def 1;

A11: e c= Y by A2, A8, A10, ZFMISC_1:77;

end;e is_a_dependent_set_of d ) implies e = Intersect XX )

assume that

A6: e c= Intersect XX and

A7: for d being a_partition of Y st d in G holds

e is_a_dependent_set_of d ; :: thesis: e = Intersect XX

consider Ad being set such that

A8: Ad c= g and

A9: Ad <> {} and

A10: e = union Ad by A1, A7, PARTIT1:def 1;

A11: e c= Y by A2, A8, A10, ZFMISC_1:77;

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

end;

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

then A12:
e in XX
by A7, A11;

Intersect XX c= e

end;Intersect XX c= e

proof

hence
e = Intersect XX
by A6, XBOOLE_0:def 10; :: thesis: verum
let X1 be object ; :: according to TARSKI:def 3 :: thesis: ( not X1 in Intersect XX or X1 in e )

assume X1 in Intersect XX ; :: thesis: X1 in e

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

hence X1 in e by A12, SETFAM_1:def 1; :: thesis: verum

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

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

hence X1 in e by A12, SETFAM_1:def 1; :: thesis: verum

suppose A13:
not y in e
; :: thesis: e = Intersect XX

reconsider e = e as Subset of Y by A2, A8, A10, ZFMISC_1:77;

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

then A14: y in e ` by A13, XBOOLE_0:def 5;

e <> Y by A13;

then for d being a_partition of Y st d in G holds

e ` is_a_dependent_set_of d by A7, PARTIT1:10;

then A15: e ` in XX by A14;

A16: Intersect XX c= e `

consider ad being object such that

A18: ad in Ad by A9, XBOOLE_0:def 1;

reconsider ad = ad as set by TARSKI:1;

e /\ (e `) = {} by SUBSET_1:24, XBOOLE_0:def 7;

then e /\ (Intersect XX) = {} by A16, XBOOLE_1:3, XBOOLE_1:26;

then e c= {} by A6, A17, XBOOLE_1:26;

then union Ad = {} by A10;

then A19: ad c= {} by A18, ZFMISC_1:74;

ad <> {} by A4, A8, A18;

hence e = Intersect XX by A19; :: thesis: verum

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

then A14: y in e ` by A13, XBOOLE_0:def 5;

e <> Y by A13;

then for d being a_partition of Y st d in G holds

e ` is_a_dependent_set_of d by A7, PARTIT1:10;

then A15: e ` in XX by A14;

A16: Intersect XX c= e `

proof

A17:
e /\ e = e
;
let X1 be object ; :: according to TARSKI:def 3 :: thesis: ( not X1 in Intersect XX or X1 in e ` )

assume X1 in Intersect XX ; :: thesis: X1 in e `

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

hence X1 in e ` by A15, SETFAM_1:def 1; :: thesis: verum

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

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

hence X1 in e ` by A15, SETFAM_1:def 1; :: thesis: verum

consider ad being object such that

A18: ad in Ad by A9, XBOOLE_0:def 1;

reconsider ad = ad as set by TARSKI:1;

e /\ (e `) = {} by SUBSET_1:24, XBOOLE_0:def 7;

then e /\ (Intersect XX) = {} by A16, XBOOLE_1:3, XBOOLE_1:26;

then e c= {} by A6, A17, XBOOLE_1:26;

then union Ad = {} by A10;

then A19: ad c= {} by A18, ZFMISC_1:74;

ad <> {} by A4, A8, A18;

hence e = Intersect XX by A19; :: thesis: verum

y in X1

proof

then A20:
y in meet XX
by A3, 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 & ( for d being a_partition of Y st d in G holds

X is_a_dependent_set_of d ) ) ;

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 & ( for d being a_partition of Y st d in G holds

X is_a_dependent_set_of d ) ) ;

hence y in X1 ; :: thesis: verum

then A21: Intersect XX <> {} by SETFAM_1:def 9;

for d being a_partition of Y st d in G holds

Intersect XX is_a_dependent_set_of d

proof

hence
( y in Intersect XX & Intersect XX is_upper_min_depend_of G )
by A3, A20, A5, SETFAM_1:def 9; :: thesis: verum
let d be a_partition of Y; :: thesis: ( d in G implies Intersect XX is_a_dependent_set_of d )

assume A22: d in G ; :: thesis: Intersect XX is_a_dependent_set_of d

for X1 being set st X1 in XX holds

X1 is_a_dependent_set_of d

end;assume A22: d in G ; :: thesis: Intersect XX is_a_dependent_set_of d

for X1 being set st X1 in XX holds

X1 is_a_dependent_set_of d

proof

hence
Intersect XX is_a_dependent_set_of d
by A21, PARTIT1:8; :: thesis: verum
let X1 be set ; :: thesis: ( X1 in XX implies X1 is_a_dependent_set_of d )

assume X1 in XX ; :: thesis: X1 is_a_dependent_set_of d

then ex X being Subset of Y st

( X = X1 & y in X & ( for d being a_partition of Y st d in G holds

X is_a_dependent_set_of d ) ) ;

hence X1 is_a_dependent_set_of d by A22; :: thesis: verum

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

then ex X being Subset of Y st

( X = X1 & y in X & ( for d being a_partition of Y st d in G holds

X is_a_dependent_set_of d ) ) ;

hence X1 is_a_dependent_set_of d by A22; :: thesis: verum