let Y be non empty set ; 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; 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; ( 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
; 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, Def1;
consider B being set such that
A6:
B c= PA
and
B <> {}
and
A7:
X1 = union B
by A2, Def1;
A8:
X0 /\ X1 c= union (A /\ B)
proof
let x be
set ;
TARSKI:def 3 ( not x in X0 /\ X1 or x in union (A /\ B) )
assume A9:
x in X0 /\ X1
;
x in union (A /\ B)
A10:
x in X0
by A9, 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;
A18:
y meets z
by A12, A14, XBOOLE_0:3;
A19:
y = z
by A16, A17, A18, EQREL_1:def 6;
A20:
y in A /\ B
by A13, A15, A19, XBOOLE_0:def 4;
thus
x in union (A /\ B)
by A12, A20, TARSKI:def 4;
verum
end;
A21:
union (A /\ B) c= X0 /\ X1
proof
let x be
set ;
TARSKI:def 3 ( not x in union (A /\ B) or x in X0 /\ X1 )
assume A22:
x in union (A /\ B)
;
x in X0 /\ X1
consider y being
set such that A23:
x in y
and A24:
y in A /\ B
by A22, TARSKI:def 4;
A25:
y in A
by A24, XBOOLE_0:def 4;
A26:
y in B
by A24, XBOOLE_0:def 4;
A27:
x in X0
by A5, A23, A25, TARSKI:def 4;
A28:
x in X1
by A7, A23, A26, TARSKI:def 4;
thus
x in X0 /\ X1
by A27, A28, XBOOLE_0:def 4;
verum
end;
A29:
X0 /\ X1 = union (A /\ B)
by A8, A21, XBOOLE_0:def 10;
A30:
A \/ B c= PA
by A4, A6, XBOOLE_1:8;
A31:
( A /\ B c= A & A c= A \/ B )
by XBOOLE_1:7, XBOOLE_1:17;
A32:
A /\ B c= A \/ B
by A31, XBOOLE_1:1;
A33:
A /\ B c= PA
by A30, A32, XBOOLE_1:1;
thus
X0 /\ X1 is_a_dependent_set_of PA
by A29, A33, A34, Def1; verum