let Y be non empty set ; for PA, PB being a_partition of Y
for p0, x, y being set
for f being FinSequence of Y st p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Nat st 1 <= i & i < len f holds
ex p2, p3, u being set st
( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB holds
y in p0
let PA, PB be a_partition of Y; for p0, x, y being set
for f being FinSequence of Y st p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Nat st 1 <= i & i < len f holds
ex p2, p3, u being set st
( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB holds
y in p0
let p0, x, y be set ; for f being FinSequence of Y st p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Nat st 1 <= i & i < len f holds
ex p2, p3, u being set st
( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB holds
y in p0
let f be FinSequence of Y; ( p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Nat st 1 <= i & i < len f holds
ex p2, p3, u being set st
( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB implies y in p0 )
assume that
A1:
p0 c= Y
and
A2:
( x in p0 & f . 1 = x )
and
A3:
( f . (len f) = y & 1 <= len f )
and
A4:
for i being Nat st 1 <= i & i < len f holds
ex p2, p3, u being set st
( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 )
and
A5:
p0 is_a_dependent_set_of PA
and
A6:
p0 is_a_dependent_set_of PB
; y in p0
consider A1 being set such that
A7:
A1 c= PA
and
A1 <> {}
and
A8:
p0 = union A1
by A5;
consider B1 being set such that
A9:
B1 c= PB
and
B1 <> {}
and
A10:
p0 = union B1
by A6;
A11:
union PA = Y
by EQREL_1:def 4;
A12:
for A being set st A in PA holds
( A <> {} & ( for B being set holds
( not B in PA or A = B or A misses B ) ) )
by EQREL_1:def 4;
A13:
for A being set st A in PB holds
( A <> {} & ( for B being set holds
( not B in PB or A = B or A misses B ) ) )
by EQREL_1:def 4;
for k being Nat st 1 <= k & k <= len f holds
f . k in p0
proof
defpred S1[
Nat]
means ( 1
<= $1 & $1
<= len f implies
f . $1
in p0 );
A14:
S1[
0 ]
;
A15:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A16:
S1[
k]
;
S1[k + 1]
assume that A17:
1
<= k + 1
and A18:
k + 1
<= len f
;
f . (k + 1) in p0
A19:
k < len f
by A18, NAT_1:13;
A20:
( 1
<= k or 1
= k + 1 )
by A17, NAT_1:8;
now f . (k + 1) in p0per cases
( 1 <= k or 0 = k )
by A20;
suppose A21:
1
<= k
;
f . (k + 1) in p0then consider p2,
p3,
u being
set such that A22:
p2 in PA
and A23:
p3 in PB
and A24:
f . k in p2
and A25:
u in p2
and A26:
u in p3
and A27:
f . (k + 1) in p3
by A4, A19;
consider A being
set such that A28:
f . k in A
and A29:
A in PA
by A1, A11, A16, A18, A21, NAT_1:13, TARSKI:def 4;
A30:
(
p2 = A or
p2 misses A )
by A22, A29, EQREL_1:def 4;
consider a being
set such that A31:
f . k in a
and A32:
a in A1
by A8, A16, A18, A21, NAT_1:13, TARSKI:def 4;
(
a = p2 or
a misses p2 )
by A7, A12, A22, A32;
then A33:
A c= p0
by A8, A24, A28, A30, A31, A32, XBOOLE_0:3, ZFMISC_1:74;
consider B being
set such that A34:
u in B
and A35:
B in PB
by A23, A26;
A36:
(
p3 = B or
p3 misses B )
by A23, A35, EQREL_1:def 4;
consider b being
set such that A37:
u in b
and A38:
b in B1
by A10, A24, A25, A28, A30, A33, TARSKI:def 4, XBOOLE_0:3;
(
p3 = b or
p3 misses b )
by A9, A13, A23, A38;
then
B c= p0
by A10, A26, A34, A36, A37, A38, XBOOLE_0:3, ZFMISC_1:74;
hence
f . (k + 1) in p0
by A26, A27, A34, A36, XBOOLE_0:3;
verum end;
hence
f . (k + 1) in p0
;
verum
end;
thus
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A14, A15); verum
end;
hence
y in p0
by A3; verum