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 ;
consider y being set such that
A12: x in y and
A13: y in A by ;
consider z being set such that
A14: x in z and
A15: z in B by ;
A16: y in PA by ;
A17: z in PA by ;
y meets z by ;
then y = z by ;
then y in A /\ B by ;
hence x in union (A /\ B) by ; :: 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 ;
A21: y in B by ;
A22: x in X0 by ;
x in X1 by ;
hence x in X0 /\ X1 by ; :: thesis: verum
end;
then A23: X0 /\ X1 = union (A /\ B) by ;
A24: A \/ B c= PA by ;
( A /\ B c= A & A c= A \/ B ) by ;
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 ;
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 ; :: thesis: verum