let I be set ; :: thesis: for X, Y being ManySortedSet of I holds
( X (\) Y = EmptyMS I iff X c= Y )
let X, Y be ManySortedSet of I; :: thesis: ( X (\) Y = EmptyMS I iff X c= Y )

hereby :: thesis: ( X c= Y implies X (\) Y = EmptyMS I )

assume A1: X (\) Y = EmptyMS I ; :: thesis: X c= Y

now :: thesis: for i being object st i in I holds
X . i c= Y . i

let i be object ; :: thesis: ( i in I implies X . i c= Y . i )
assume i in I ; :: thesis: X . i c= Y . i
then (X . i) \ (Y . i) = (X (\) Y) . i by Def6
.= {} by A1 ;
hence X . i c= Y . i by XBOOLE_1:37; :: thesis: verum

end;

hence X c= Y ; :: thesis: verum

end;

assume A2: X c= Y ; :: thesis: X (\) Y = EmptyMS I

now :: thesis: for i being object st i in I holds
(X (\) Y) . i = {}

let i be object ; :: thesis: ( i in I implies (X (\) Y) . i = {} )
assume A3: i in I ; :: thesis: (X (\) Y) . i = {}
then A4: X . i c= Y . i by A2;
thus (X (\) Y) . i = (X . i) \ (Y . i) by A3, Def6
.= {} by A4, XBOOLE_1:37 ; :: thesis: verum

end;

hence X (\) Y = EmptyMS I by Th6; :: thesis: verum