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

proof

let i be set ; :: thesis: ( i in I implies MA . i c= MB . i )
assume A2: i in I ; :: thesis: MA . i c= MB . i
for v being set st v in MA . i holds
v in MB . i

proof

let v be set ; :: thesis: ( v in MA . i implies v in MB . i )
assume A3: v in MA . i ; :: thesis: v in MB . i
MA . i = union { (f . i) where f is Element of Bool M : f in A } by A2, Def4;
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;
consider g being Element of Bool M such that
A6: h = g . i and
A7: g in A by A5;
h in { (k . i) where k is Element of Bool M : k in B } by A1, A6, A7;
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, Def4; :: thesis: verum

end;

hence MA . i c= MB . i by TARSKI:def 3; :: thesis: verum

end;

hence MSUnion A c= MSUnion B by PBOOLE:def 5; :: thesis: verum