let Y be non empty set ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( S1[k] implies S1[k + 1] )
assume A16: S1[k] ; :: thesis: S1[k + 1]
assume that
A17: 1 <= k + 1 and
A18: k + 1 <= len f ; :: thesis: f . (k + 1) in p0
A19: k < len f by ;
A20: ( 1 <= k or 1 = k + 1 ) by ;
now :: thesis: f . (k + 1) in p0
per cases ( 1 <= k or 0 = k ) by A20;
suppose A21: 1 <= k ; :: thesis: f . (k + 1) in p0
then 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 ;
consider A being set such that
A28: f . k in A and
A29: A in PA by ;
A30: ( p2 = A or p2 misses A ) by ;
consider a being set such that
A31: f . k in a and
A32: a in A1 by ;
( a = p2 or a misses p2 ) by A7, A12, A22, A32;
then A33: A c= p0 by ;
consider B being set such that
A34: u in B and
A35: B in PB by ;
A36: ( p3 = B or p3 misses B ) by ;
consider b being set such that
A37: u in b and
A38: b in B1 by ;
( p3 = b or p3 misses b ) by A9, A13, A23, A38;
then B c= p0 by ;
hence f . (k + 1) in p0 by ; :: thesis: verum
end;
suppose 0 = k ; :: thesis: f . (k + 1) in p0
hence f . (k + 1) in p0 by A2; :: thesis: verum
end;
end;
end;
hence f . (k + 1) in p0 ; :: thesis: verum
end;
thus for k being Nat holds S1[k] from :: thesis: verum
end;
hence y in p0 by A3; :: thesis: verum