let I be set ; for x, y, X being ManySortedSet of I st ( X = EmptyMS I or X = {x} or X = {y} or X = {x,y} ) holds
X (\) {x,y} = EmptyMS I
let x, y, X be ManySortedSet of I; ( ( X = EmptyMS I or X = {x} or X = {y} or X = {x,y} ) implies X (\) {x,y} = EmptyMS I )
assume A1:
( X = EmptyMS I or X = {x} or X = {y} or X = {x,y} )
; X (\) {x,y} = EmptyMS I
hence
X (\) {x,y} = EmptyMS I
; verum