let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st X c= Y (\) Z & ( for i, j being object st i in I & j in I & i <> j holds
(Y . i) /\ (Z . j) = {} ) holds
Union X c= (Union Y) \ (Union Z)
let X, Y, Z be ManySortedSet of I; :: thesis: ( X c= Y (\) Z & ( for i, j being object st i in I & j in I & i <> j holds
(Y . i) /\ (Z . j) = {} ) implies Union X c= (Union Y) \ (Union Z) )
assume X c= Y (\) Z ; :: thesis: ( ex i, j being object st
( i in I & j in I & i <> j & not (Y . i) /\ (Z . j) = {} ) or Union X c= (Union Y) \ (Union Z) )
then B1: Union X c= Union (Y (\) Z) by MSAFREE4:1;
assume for i, j being object st i in I & j in I & i <> j holds
(Y . i) /\ (Z . j) = {} ; :: thesis: Union X c= (Union Y) \ (Union Z)
hence Union X c= (Union Y) \ (Union Z) by LM03, B1; :: thesis: verum