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

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

assume A1: X (/\) Y = EmptyMS I ; :: thesis: X (\) Y = X
thus X (\) Y = X (\) (X (/\) Y) by Th70
.= X by A1, Th59 ; :: thesis: verum

end;

thus ( X (\) Y = X implies X (/\) Y = EmptyMS I ) by Th63; :: thesis: verum