theorem LM04: :: PETRI_3:3

for I being set
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)