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 )

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

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 )

then Intersect F = Y by SETFAM_1:def 10;
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 Th9; :: thesis: verum

end;

suppose A3: 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 )

then reconsider F9 = F as non empty Subset-Family of Y ;
assume that
A4: Intersect F <> {} and
A5: 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₁[ set , set ] means ( $2 c= PA & $2 <> {} & $1 = union $2 );
A6: for X being set st X in F holds
ex B being set st S₁[X,B]

proof

let X be set ; :: thesis: ( X in F implies ex B being set st S₁[X,B] )
assume X in F ; :: thesis: ex B being set st S₁[X,B]
then X is_a_dependent_set_of PA by A5;
hence ex B being set st S₁[X,B] by Def1; :: thesis: verum

end;

consider f being Function such that
A9: ( dom f = F & ( for X being set st X in F holds
S₁[X,f . X] ) ) from CLASSES1:sch 1(A6);
rng f c= bool (bool Y)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in bool (bool Y) )
assume y in rng f ; :: thesis: y in bool (bool Y)
then consider x being set such that
A12: x in dom f and
A13: y = f . x by FUNCT_1:def 5;
f . x c= PA by A9, A12;
then y c= bool Y by A13, XBOOLE_1:1;
hence y in bool (bool Y) ; :: thesis: verum

end;

then reconsider f = f as Function of F9,(bool (bool Y)) by A9, FUNCT_2:def 1, RELSET_1:11;
defpred S₂[ set ] means $1 in F;
deffunc H₁( Element of F9) -> Element of bool (bool Y) = f . $1;
reconsider T = { H₁(X) where X is Element of F9 : S₂[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 )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in PA )
assume A16: x in B ; :: thesis: x in PA
consider X being set such that
A17: X in F by A3, XBOOLE_0:def 1;
f . X in T by A17;
then A19: x in f . X by A16, SETFAM_1:58;
f . X c= PA by A9, A17;
hence x in PA by A19; :: thesis: verum

end;

thus B <> {} :: thesis: Intersect F = union B

proof

consider X being set such that
A21: X in F by A3, XBOOLE_0:def 1;
A22: f . X in T by A21;
consider A being set such that
A23: A in Intersect F by A4, XBOOLE_0:def 1;
reconsider A = A as Element of Y by A23;
set AA = EqClass A,PA;
A24: A in meet F by A3, A23, SETFAM_1:def 10;
for X being set st X in T holds
EqClass A,PA in X

proof

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
A27: X = f . z and
z in F ;
A28: f . z c= PA by A9;
( z = union (f . z) & A in z ) by A9, A24, SETFAM_1:def 1;
then ex A0 being set st
( A in A0 & A0 in f . z ) by TARSKI:def 4;
hence EqClass A,PA in X by A27, A28, EQREL_1:def 8; :: thesis: verum

end;

then EqClass A,PA in meet T by A22, SETFAM_1:def 1;
hence B <> {} by SETFAM_1:def 10; :: thesis: verum

end;

A32: Intersect F c= union B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Intersect F or x in union B )
assume A33: x in Intersect F ; :: thesis: x in union B
then A34: x in meet F by A3, SETFAM_1:def 10;
reconsider x = x as Element of Y by A33;
reconsider PA = PA as a_partition of Y ;
set A = EqClass x,PA;
consider X being set such that
A35: X in F by A3, XBOOLE_0:def 1;
A36: f . X in T by A35;
for X being set st X in T holds
EqClass x,PA in X

proof

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
A39: X = f . z and
z in F ;
A40: f . z c= PA by A9;
z = union (f . z) by A9;
then x in union (f . z) by A34, 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 A39, A40, EQREL_1:def 8; :: thesis: verum

end;

then EqClass x,PA in meet T by A36, SETFAM_1:def 1;
then ( x in EqClass x,PA & EqClass x,PA in Intersect T ) by A36, EQREL_1:def 8, SETFAM_1:def 10;
hence x in union B by TARSKI:def 4; :: thesis: verum

end;

union B c= Intersect F

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union B or x in Intersect F )
assume A47: x in union B ; :: thesis: x in Intersect F
consider X being set such that
A48: X in F by A3, XBOOLE_0:def 1;
A49: f . X in T by A48;
consider y being set such that
A50: x in y and
A51: y in B by A47, TARSKI:def 4;
A52: y in meet T by A49, A51, SETFAM_1:def 10;
for X being set st X in F holds
x in X

proof

let X be set ; :: thesis: ( X in F implies x in X )
assume A54: X in F ; :: thesis: x in X
then f . X in T ;
then A56: y in f . X by A52, SETFAM_1:def 1;
X = union (f . X) by A9, A54;
hence x in X by A50, A56, TARSKI:def 4; :: thesis: verum

end;

then x in meet F by A3, SETFAM_1:def 1;
hence x in Intersect F by A3, SETFAM_1:def 10; :: thesis: verum

end;

hence Intersect F = union B by A32, XBOOLE_0:def 10; :: thesis: verum

end;

end;