let I be set ; :: thesis: for X, Y being ManySortedSet of I holds X (\) Y misses Y (\) X
let X, Y be ManySortedSet of I; :: thesis: X (\) Y misses Y (\) X
let i be object ; :: according to PBOOLE:def 8 :: thesis: ( i in I implies (X (\) Y) . i misses (Y (\) X) . i )
assume i in I ; :: thesis: (X (\) Y) . i misses (Y (\) X) . i
then ( (X (\) Y) . i = (X . i) \ (Y . i) & (Y (\) X) . i = (Y . i) \ (X . i) ) by Def6;
hence (X (\) Y) . i misses (Y (\) X) . i by XBOOLE_1:82; :: thesis: verum