let I be set ; :: thesis:
let M be ManySortedSet of I; :: thesis:
let A, B be SubsetFamily of M; :: thesis:
reconsider MA = MSUnion A as ManySortedSubset of M ;
reconsider MA = MA as ManySortedSet of I ;
reconsider MB = MSUnion B as ManySortedSubset of M ;
reconsider MB = MB as ManySortedSet of I ;
assume A1: A c= B ; :: thesis:
for i being object st i in I holds
MA . i c= MB . i

let i be object ; :: thesis:
assume A2: i in I ; :: thesis:
for v being object st v in MA . i holds
v in MB . i

A3: MA . i = union { (f . i) where f is Element of Bool M : f in A } by A2, Def2;
let v be object ; :: thesis:
assume v in MA . i ; :: thesis:
then consider h being set such that
A4: v in h and
A5: h in { (f . i) where f is Element of Bool M : f in A } by A3, TARSKI:def 4;
ex g being Element of Bool M st
( h = g . i & g in A ) by A5;
then h in { (k . i) where k is Element of Bool M : k in B } by A1;
then v in union { (k . i) where k is Element of Bool M : k in B } by A4, TARSKI:def 4;
hence v in MB . i by A2, Def2; :: thesis:

end;

hence MA . i c= MB . i ; :: thesis:

end;