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)

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;

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

union (A /\ B) c= X0 /\ X1
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;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

proof

then A23:
X0 /\ X1 = union (A /\ B)
by A8, XBOOLE_0:def 10;
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;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

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 = {}

hence
X0 /\ X1 is_a_dependent_set_of PA
by A23, A25; :: thesis: verumassume 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;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