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 that
A1: X0 is_a_dependent_set_of PA and
A2: X1 is_a_dependent_set_of PA and
A3: X0 meets X1 ; :: thesis: X0 /\ X1 is_a_dependent_set_of PA
consider A being set such that
A4: A c= PA and
A <> {} and
A5: X0 = union A by A1;
consider B being set such that
A6: B c= PA and
B <> {} and
A7: X1 = union B by A2;
A8: X0 /\ X1 c= union (A /\ B)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X0 /\ X1 or x in union (A /\ B) )
assume A9: x in X0 /\ X1 ; :: thesis: x in union (A /\ B)
then A10: x in X0 by XBOOLE_0:def 4;
A11: x in X1 by A9, XBOOLE_0:def 4;
consider y being set such that
A12: x in y and
A13: y in A by A5, A10, TARSKI:def 4;
consider z being set such that
A14: x in z and
A15: z in B by A7, A11, TARSKI:def 4;
A16: y in PA by A4, A13;
A17: z in PA by A6, A15;
y meets z by A12, A14, XBOOLE_0:3;
then y = z by A16, A17, EQREL_1:def 4;
then y in A /\ B by A13, A15, XBOOLE_0:def 4;
hence x in union (A /\ B) by A12, TARSKI:def 4; :: thesis: verum

end;

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

proof

let x be object ; :: 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
A18: x in y and
A19: y in A /\ B by TARSKI:def 4;
A20: y in A by A19, XBOOLE_0:def 4;
A21: y in B by A19, XBOOLE_0:def 4;
A22: x in X0 by A5, A18, A20, TARSKI:def 4;
x in X1 by A7, A18, A21, TARSKI:def 4;
hence x in X0 /\ X1 by A22, XBOOLE_0:def 4; :: thesis: verum

end;

then A23: X0 /\ X1 = union (A /\ B) by A8, XBOOLE_0:def 10;
A24: A \/ B c= PA by A4, A6, XBOOLE_1:8;
( A /\ B c= A & A c= A \/ B ) by XBOOLE_1:7, XBOOLE_1:17;
then A /\ B c= A \/ B ;
then A25: A /\ B c= PA by A24;

now :: thesis: not A /\ B = {}

assume A26: A /\ B = {} ; :: thesis: contradiction
ex y being object st
( y in X0 & y in X1 ) by A3, XBOOLE_0:3;
hence contradiction by A8, A26, XBOOLE_0:def 4, ZFMISC_1:2; :: thesis: verum

end;

hence X0 /\ X1 is_a_dependent_set_of PA by A23, A25; :: thesis: verum