let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st X overlaps Y \ Z holds
Y overlaps X \ Z
let X, Y, Z be ManySortedSet of I; :: thesis: ( X overlaps Y \ Z implies Y overlaps X \ Z )
assume A1: X overlaps Y \ Z ; :: thesis: Y overlaps X \ Z
let i be set ; :: according to PBOOLE:def 10 :: thesis: ( i in I implies Y . i meets (X \ Z) . i )
assume A2: i in I ; :: thesis: Y . i meets (X \ Z) . i
then X . i meets (Y \ Z) . i by A1, Def10;
then X . i meets (Y . i) \ (Z . i) by A2, Def9;
then Y . i meets (X . i) \ (Z . i) by XBOOLE_1:81;
hence Y . i meets (X \ Z) . i by A2, Def9; :: thesis: verum