let X be set ; for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for A, B, P being set st P = DisUnion S & A in P & B in P & A misses B holds
A \/ B in P
let S be with_empty_element cap-closed semi-diff-closed Subset-Family of X; for A, B, P being set st P = DisUnion S & A in P & B in P & A misses B holds
A \/ B in P
let A, B, P be set ; ( P = DisUnion S & A in P & B in P & A misses B implies A \/ B in P )
assume that
A1:
P = DisUnion S
and
A2:
( A in P & B in P & A misses B )
; A \/ B in P
consider A1 being Subset of X such that
A3:
( A = A1 & ex g being disjoint_valued FinSequence of S st A1 = Union g )
by A1, A2;
consider g1 being disjoint_valued FinSequence of S such that
A4:
A1 = Union g1
by A3;
consider B1 being Subset of X such that
A5:
( B = B1 & ex g being disjoint_valued FinSequence of S st B1 = Union g )
by A1, A2;
consider g2 being disjoint_valued FinSequence of S such that
A6:
B1 = Union g2
by A5;
set F = g1 ^ g2;
then reconsider F = g1 ^ g2 as disjoint_valued FinSequence of S by PROB_2:def 2;
rng F = (rng g1) \/ (rng g2)
by FINSEQ_1:31;
then
Union F = A1 \/ B1
by A4, A6, ZFMISC_1:78;
hence
A \/ B in P
by A1, A3, A5; verum