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 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 )

then reconsider F' = F as non empty Subset-Family of Y ;
assume A2: ( Intersect F <> {} & ( 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 );
A3: 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 A2;
hence ex B being set st S₁[X,B] by Def1; :: thesis: verum

end;

consider f being Function such that
A4: ( dom f = F & ( for X being set st X in F holds
S₁[X,f . X] ) ) from CLASSES1:sch 1(A3);
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
A5: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
f . x c= PA by A4, A5;
then y c= bool Y by A5, XBOOLE_1:1;
hence y in bool (bool Y) ; :: thesis: verum

end;

then reconsider f = f as Function of F',(bool (bool Y)) by A4, FUNCT_2:def 1, RELSET_1:11;
defpred S₂[ set ] means $1 in F;
deffunc H₁( Element of F') -> Element of bool (bool Y) = f . $1;
reconsider T = { H₁(X) where X is Element of F' : 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 A6: x in B ; :: thesis: x in PA
consider X being set such that
A7: X in F by A1, XBOOLE_0:def 1;
f . X in T by A7;
then A8: x in f . X by A6, SETFAM_1:58;
f . X c= PA by A4, A7;
hence x in PA by A8; :: thesis: verum

end;

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

proof

consider X being set such that
A9: X in F by A1, XBOOLE_0:def 1;
A10: f . X in T by A9;
consider A being set such that
A11: A in Intersect F by A2, XBOOLE_0:def 1;
reconsider A = A as Element of Y by A11;
set AA = EqClass A,PA;
A12: A in meet F by A1, A11, 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 F' such that
A13: ( X = f . z & z in F ) ;
A14: f . z c= PA by A4;
A15: z = union (f . z) by A4;
A in z by A12, SETFAM_1:def 1;
then ex A0 being set st
( A in A0 & A0 in f . z ) by A15, TARSKI:def 4;
hence EqClass A,PA in X by A13, A14, EQREL_1:def 8; :: thesis: verum

end;

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

end;

thus Intersect F = union B :: thesis: verum

proof

A16: 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 A17: x in Intersect F ; :: thesis: x in union B
then A18: x in meet F by A1, SETFAM_1:def 10;
reconsider x = x as Element of Y by A17;
reconsider PA = PA as a_partition of Y ;
set A = EqClass x,PA;
consider X being set such that
A19: X in F by A1, XBOOLE_0:def 1;
A20: f . X in T by A19;
A21: x in EqClass x,PA by EQREL_1:def 8;
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 F' such that
A22: ( X = f . z & z in F ) ;
A23: f . z c= PA by A4;
z = union (f . z) by A4;
then x in union (f . z) by A18, 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 A22, A23, EQREL_1:def 8; :: thesis: verum

end;

then EqClass x,PA in meet T by A20, SETFAM_1:def 1;
then EqClass x,PA in Intersect T by A20, SETFAM_1:def 10;
hence x in union B by A21, 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 A24: x in union B ; :: thesis: x in Intersect F
consider X being set such that
A25: X in F by A1, XBOOLE_0:def 1;
A26: f . X in T by A25;
consider y being set such that
A27: ( x in y & y in B ) by A24, TARSKI:def 4;
A28: y in meet T by A26, A27, 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 A29: X in F ; :: thesis: x in X
then f . X in T ;
then A30: y in f . X by A28, SETFAM_1:def 1;
X = union (f . X) by A4, A29;
hence x in X by A27, A30, TARSKI:def 4; :: thesis: verum

end;

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

end;

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

end;

end;

end;