let I be set ; for X, Y, Z being ManySortedSet of I st X is V39() & X c= [|Y,Z|] holds
ex A being ManySortedSet of I st
( A is V39() & A c= Y & X c= [|A,Z|] )
let X, Y, Z be ManySortedSet of I; ( X is V39() & X c= [|Y,Z|] implies ex A being ManySortedSet of I st
( A is V39() & A c= Y & X c= [|A,Z|] ) )
assume that
A1:
X is V39()
and
A2:
X c= [|Y,Z|]
; ex A being ManySortedSet of I st
( A is V39() & A c= Y & X c= [|A,Z|] )
defpred S1[ object , object ] means ex D being set st
( D = $2 & D is finite & D c= Y . $1 & X . $1 c= [:D,(Z . $1):] );
A3:
for i being object st i in I holds
ex j being object st S1[i,j]
consider A being ManySortedSet of I such that
A7:
for i being object st i in I holds
S1[i,A . i]
from PBOOLE:sch 3(A3);
take
A
; ( A is V39() & A c= Y & X c= [|A,Z|] )
thus
A is V39()
( A c= Y & X c= [|A,Z|] )
thus
A c= Y
X c= [|A,Z|]
thus
X c= [|A,Z|]
verum