let Y be non empty set ; :: thesis: for PA being a_partition of Y

for F being Subset-Family of Y st Intersect F <> {} & ( for X being set st X in F holds

X is_a_dependent_set_of PA ) holds

Intersect F is_a_dependent_set_of PA

let PA be a_partition of Y; :: thesis: for F being Subset-Family of Y st Intersect F <> {} & ( for X being set st X in F holds

X is_a_dependent_set_of PA ) holds

Intersect F is_a_dependent_set_of PA

let F be Subset-Family of Y; :: thesis: ( Intersect F <> {} & ( for X being set st X in F holds

X is_a_dependent_set_of PA ) implies Intersect F is_a_dependent_set_of PA )

for F being Subset-Family of Y st Intersect F <> {} & ( for X being set st X in F holds

X is_a_dependent_set_of PA ) holds

Intersect F is_a_dependent_set_of PA

let PA be a_partition of Y; :: thesis: for F being Subset-Family of Y st Intersect F <> {} & ( for X being set st X in F holds

X is_a_dependent_set_of PA ) holds

Intersect F is_a_dependent_set_of PA

let F be Subset-Family of Y; :: thesis: ( Intersect F <> {} & ( for X being set st X in F holds

X is_a_dependent_set_of PA ) implies Intersect F is_a_dependent_set_of PA )

per cases
( F = {} or F <> {} )
;

end;

suppose
F = {}
; :: thesis: ( Intersect F <> {} & ( for X being set st X in F holds

X is_a_dependent_set_of PA ) implies Intersect F is_a_dependent_set_of PA )

X is_a_dependent_set_of PA ) implies Intersect F is_a_dependent_set_of PA )

then
Intersect F = Y
by SETFAM_1:def 9;

hence ( Intersect F <> {} & ( for X being set st X in F holds

X is_a_dependent_set_of PA ) implies Intersect F is_a_dependent_set_of PA ) by Th7; :: thesis: verum

end;hence ( Intersect F <> {} & ( for X being set st X in F holds

X is_a_dependent_set_of PA ) implies Intersect F is_a_dependent_set_of PA ) by Th7; :: thesis: verum

suppose A1:
F <> {}
; :: thesis: ( Intersect F <> {} & ( for X being set st X in F holds

X is_a_dependent_set_of PA ) implies Intersect F is_a_dependent_set_of PA )

X is_a_dependent_set_of PA ) implies Intersect F is_a_dependent_set_of PA )

then reconsider F9 = F as non empty Subset-Family of Y ;

assume that

A2: Intersect F <> {} and

A3: for X being set st X in F holds

X is_a_dependent_set_of PA ; :: thesis: Intersect F is_a_dependent_set_of PA

defpred S_{1}[ object , object ] means ex A being set st

( A = $2 & A c= PA & $2 <> {} & $1 = union A );

A4: for X being object st X in F holds

ex B being object st S_{1}[X,B]

A5: ( dom f = F & ( for X being object st X in F holds

S_{1}[X,f . X] ) )
from CLASSES1:sch 1(A4);

rng f c= bool (bool Y)

defpred S_{2}[ set ] means $1 in F;

deffunc H_{1}( Element of F9) -> Element of bool (bool Y) = f . $1;

reconsider T = { H_{1}(X) where X is Element of F9 : S_{2}[X] } as Subset-Family of (bool Y) from DOMAIN_1:sch 8();

reconsider T = T as Subset-Family of (bool Y) ;

take B = Intersect T; :: according to PARTIT1:def 1 :: thesis: ( B c= PA & B <> {} & Intersect F = union B )

thus B c= PA :: thesis: ( B <> {} & Intersect F = union B )

end;assume that

A2: Intersect F <> {} and

A3: for X being set st X in F holds

X is_a_dependent_set_of PA ; :: thesis: Intersect F is_a_dependent_set_of PA

defpred S

( A = $2 & A c= PA & $2 <> {} & $1 = union A );

A4: for X being object st X in F holds

ex B being object st S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in F implies ex B being object st S_{1}[x,B] )

reconsider X = x as set by TARSKI:1;

assume x in F ; :: thesis: ex B being object st S_{1}[x,B]

then X is_a_dependent_set_of PA by A3;

then ex B being set st

( B c= PA & B <> {} & X = union B ) ;

then ex B being object st S_{1}[X,B]
;

hence ex B being object st S_{1}[x,B]
; :: thesis: verum

end;reconsider X = x as set by TARSKI:1;

assume x in F ; :: thesis: ex B being object st S

then X is_a_dependent_set_of PA by A3;

then ex B being set st

( B c= PA & B <> {} & X = union B ) ;

then ex B being object st S

hence ex B being object st S

A5: ( dom f = F & ( for X being object st X in F holds

S

rng f c= bool (bool Y)

proof

then reconsider f = f as Function of F9,(bool (bool Y)) by A5, FUNCT_2:def 1, RELSET_1:4;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in bool (bool Y) )

reconsider yy = y as set by TARSKI:1;

assume y in rng f ; :: thesis: y in bool (bool Y)

then consider x being object such that

A6: x in dom f and

A7: y = f . x by FUNCT_1:def 3;

S_{1}[x,f . x]
by A5, A6;

then f . x c= PA ;

then yy c= bool Y by A7, XBOOLE_1:1;

hence y in bool (bool Y) ; :: thesis: verum

end;reconsider yy = y as set by TARSKI:1;

assume y in rng f ; :: thesis: y in bool (bool Y)

then consider x being object such that

A6: x in dom f and

A7: y = f . x by FUNCT_1:def 3;

S

then f . x c= PA ;

then yy c= bool Y by A7, XBOOLE_1:1;

hence y in bool (bool Y) ; :: thesis: verum

defpred S

deffunc H

reconsider T = { H

reconsider T = T as Subset-Family of (bool Y) ;

take B = Intersect T; :: according to PARTIT1:def 1 :: thesis: ( B c= PA & B <> {} & Intersect F = union B )

thus B c= PA :: thesis: ( B <> {} & Intersect F = union B )

proof

thus
B <> {}
:: thesis: Intersect F = union B
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in PA )

assume A8: x in B ; :: thesis: x in PA

consider X being object such that

A9: X in F by A1, XBOOLE_0:def 1;

f . X in T by A9;

then A10: x in f . X by A8, SETFAM_1:43;

S_{1}[X,f . X]
by A5, A9;

then f . X c= PA ;

hence x in PA by A10; :: thesis: verum

end;assume A8: x in B ; :: thesis: x in PA

consider X being object such that

A9: X in F by A1, XBOOLE_0:def 1;

f . X in T by A9;

then A10: x in f . X by A8, SETFAM_1:43;

S

then f . X c= PA ;

hence x in PA by A10; :: thesis: verum

proof

A18:
Intersect F c= union B
consider X being object such that

A11: X in F by A1, XBOOLE_0:def 1;

A12: f . X in T by A11;

consider A being object such that

A13: A in Intersect F by A2, XBOOLE_0:def 1;

reconsider A = A as Element of Y by A13;

set AA = EqClass (A,PA);

A14: A in meet F by A1, A13, SETFAM_1:def 9;

for X being set st X in T holds

EqClass (A,PA) in X

hence B <> {} by SETFAM_1:def 9; :: thesis: verum

end;A11: X in F by A1, XBOOLE_0:def 1;

A12: f . X in T by A11;

consider A being object such that

A13: A in Intersect F by A2, XBOOLE_0:def 1;

reconsider A = A as Element of Y by A13;

set AA = EqClass (A,PA);

A14: A in meet F by A1, A13, SETFAM_1:def 9;

for X being set st X in T holds

EqClass (A,PA) in X

proof

then
EqClass (A,PA) in meet T
by A12, SETFAM_1:def 1;
let X be set ; :: thesis: ( X in T implies EqClass (A,PA) in X )

assume X in T ; :: thesis: EqClass (A,PA) in X

then consider z being Element of F9 such that

A15: X = f . z and

z in F ;

A16: S_{1}[z,f . z]
by A5;

then A17: f . z c= PA ;

( z = union (f . z) & A in z ) by A14, SETFAM_1:def 1, A16;

then ex A0 being set st

( A in A0 & A0 in f . z ) by TARSKI:def 4;

hence EqClass (A,PA) in X by A15, A17, EQREL_1:def 6; :: thesis: verum

end;assume X in T ; :: thesis: EqClass (A,PA) in X

then consider z being Element of F9 such that

A15: X = f . z and

z in F ;

A16: S

then A17: f . z c= PA ;

( z = union (f . z) & A in z ) by A14, SETFAM_1:def 1, A16;

then ex A0 being set st

( A in A0 & A0 in f . z ) by TARSKI:def 4;

hence EqClass (A,PA) in X by A15, A17, EQREL_1:def 6; :: thesis: verum

hence B <> {} by SETFAM_1:def 9; :: thesis: verum

proof

union B c= Intersect F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Intersect F or x in union B )

assume A19: x in Intersect F ; :: thesis: x in union B

then A20: x in meet F by A1, SETFAM_1:def 9;

reconsider x = x as Element of Y by A19;

reconsider PA = PA as a_partition of Y ;

set A = EqClass (x,PA);

consider X being object such that

A21: X in F by A1, XBOOLE_0:def 1;

A22: f . X in T by A21;

for X being set st X in T holds

EqClass (x,PA) in X

then ( x in EqClass (x,PA) & EqClass (x,PA) in Intersect T ) by A22, EQREL_1:def 6, SETFAM_1:def 9;

hence x in union B by TARSKI:def 4; :: thesis: verum

end;assume A19: x in Intersect F ; :: thesis: x in union B

then A20: x in meet F by A1, SETFAM_1:def 9;

reconsider x = x as Element of Y by A19;

reconsider PA = PA as a_partition of Y ;

set A = EqClass (x,PA);

consider X being object such that

A21: X in F by A1, XBOOLE_0:def 1;

A22: f . X in T by A21;

for X being set st X in T holds

EqClass (x,PA) in X

proof

then
EqClass (x,PA) in meet T
by A22, SETFAM_1:def 1;
let X be set ; :: thesis: ( X in T implies EqClass (x,PA) in X )

assume X in T ; :: thesis: EqClass (x,PA) in X

then consider z being Element of F9 such that

A23: X = f . z and

z in F ;

A24: S_{1}[z,f . z]
by A5;

then A25: f . z c= PA ;

z = union (f . z) by A24;

then x in union (f . z) by A20, SETFAM_1:def 1;

then ex A0 being set st

( x in A0 & A0 in f . z ) by TARSKI:def 4;

hence EqClass (x,PA) in X by A23, A25, EQREL_1:def 6; :: thesis: verum

end;assume X in T ; :: thesis: EqClass (x,PA) in X

then consider z being Element of F9 such that

A23: X = f . z and

z in F ;

A24: S

then A25: f . z c= PA ;

z = union (f . z) by A24;

then x in union (f . z) by A20, SETFAM_1:def 1;

then ex A0 being set st

( x in A0 & A0 in f . z ) by TARSKI:def 4;

hence EqClass (x,PA) in X by A23, A25, EQREL_1:def 6; :: thesis: verum

then ( x in EqClass (x,PA) & EqClass (x,PA) in Intersect T ) by A22, EQREL_1:def 6, SETFAM_1:def 9;

hence x in union B by TARSKI:def 4; :: thesis: verum

proof

hence
Intersect F = union B
by A18, XBOOLE_0:def 10; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union B or x in Intersect F )

assume A26: x in union B ; :: thesis: x in Intersect F

consider X being object such that

A27: X in F by A1, XBOOLE_0:def 1;

A28: f . X in T by A27;

consider y being set such that

A29: x in y and

A30: y in B by A26, TARSKI:def 4;

A31: y in meet T by A28, A30, SETFAM_1:def 9;

for X being set st X in F holds

x in X

hence x in Intersect F by A1, SETFAM_1:def 9; :: thesis: verum

end;assume A26: x in union B ; :: thesis: x in Intersect F

consider X being object such that

A27: X in F by A1, XBOOLE_0:def 1;

A28: f . X in T by A27;

consider y being set such that

A29: x in y and

A30: y in B by A26, TARSKI:def 4;

A31: y in meet T by A28, A30, SETFAM_1:def 9;

for X being set st X in F holds

x in X

proof

then
x in meet F
by A1, SETFAM_1:def 1;
let X be set ; :: thesis: ( X in F implies x in X )

assume A32: X in F ; :: thesis: x in X

then f . X in T ;

then A33: y in f . X by A31, SETFAM_1:def 1;

S_{1}[X,f . X]
by A5, A32;

then X = union (f . X) ;

hence x in X by A29, A33, TARSKI:def 4; :: thesis: verum

end;assume A32: X in F ; :: thesis: x in X

then f . X in T ;

then A33: y in f . X by A31, SETFAM_1:def 1;

S

then X = union (f . X) ;

hence x in X by A29, A33, TARSKI:def 4; :: thesis: verum

hence x in Intersect F by A1, SETFAM_1:def 9; :: thesis: verum