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

(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