let I be set ; :: thesis: for X, Y being ManySortedSet of holds X \ Y misses Y \ X
let X, Y be ManySortedSet of ; :: thesis: X \ Y misses Y \ X
let i be set ; :: according to PBOOLE:def 11 :: 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 Def9;
hence (X \ Y) . i misses (Y \ X) . i by XBOOLE_1:82; :: thesis: verum