let Y be non empty set ; :: thesis: for PA being a_partition of Y
for X0, X1 being Subset of Y st X0 is_a_dependent_set_of PA & X1 is_a_dependent_set_of PA & X0 meets X1 holds
X0 /\ X1 is_a_dependent_set_of PA
let PA be a_partition of Y; :: thesis: for X0, X1 being Subset of Y st X0 is_a_dependent_set_of PA & X1 is_a_dependent_set_of PA & X0 meets X1 holds
X0 /\ X1 is_a_dependent_set_of PA
let X0, X1 be Subset of Y; :: thesis: ( X0 is_a_dependent_set_of PA & X1 is_a_dependent_set_of PA & X0 meets X1 implies X0 /\ X1 is_a_dependent_set_of PA )
assume A1: ( X0 is_a_dependent_set_of PA & X1 is_a_dependent_set_of PA & X0 meets X1 ) ; :: thesis: X0 /\ X1 is_a_dependent_set_of PA
then consider A being set such that
A2: ( A c= PA & A <> {} & X0 = union A ) by Def1;
consider B being set such that
A3: ( B c= PA & B <> {} & X1 = union B ) by A1, Def1;
A4: X0 /\ X1 = union (A /\ B)

proof

A5: X0 /\ X1 c= union (A /\ B)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X0 /\ X1 or x in union (A /\ B) )
assume x in X0 /\ X1 ; :: thesis: x in union (A /\ B)
then A6: ( x in X0 & x in X1 ) by XBOOLE_0:def 4;
then consider y being set such that
A7: ( x in y & y in A ) by A2, TARSKI:def 4;
consider z being set such that
A8: ( x in z & z in B ) by A3, A6, TARSKI:def 4;
A9: y in PA by A2, A7;
A10: z in PA by A3, A8;
y meets z by A7, A8, XBOOLE_0:3;
then y = z by A9, A10, EQREL_1:def 6;
then y in A /\ B by A7, A8, XBOOLE_0:def 4;
hence x in union (A /\ B) by A7, TARSKI:def 4; :: thesis: verum

end;

union (A /\ B) c= X0 /\ X1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union (A /\ B) or x in X0 /\ X1 )
assume x in union (A /\ B) ; :: thesis: x in X0 /\ X1
then consider y being set such that
A11: ( x in y & y in A /\ B ) by TARSKI:def 4;
( y in A & y in B ) by A11, XBOOLE_0:def 4;
then ( x in X0 & x in X1 ) by A2, A3, A11, TARSKI:def 4;
hence x in X0 /\ X1 by XBOOLE_0:def 4; :: thesis: verum

end;

hence X0 /\ X1 = union (A /\ B) by A5, XBOOLE_0:def 10; :: thesis: verum

end;

A12: A \/ B c= PA by A2, A3, XBOOLE_1:8;
A13: A /\ B c= A by XBOOLE_1:17;
A c= A \/ B by XBOOLE_1:7;
then A /\ B c= A \/ B by A13, XBOOLE_1:1;
then A14: A /\ B c= PA by A12, XBOOLE_1:1;

now

assume A15: A /\ B = {} ; :: thesis: contradiction
consider y being set such that
A16: ( y in X0 & y in X1 ) by A1, XBOOLE_0:3;
thus contradiction by A4, A15, A16, XBOOLE_0:def 4, ZFMISC_1:2; :: thesis: verum

end;

hence X0 /\ X1 is_a_dependent_set_of PA by A4, A14, Def1; :: thesis: verum