let I be set ; for x1, x2, A being ManySortedSet of I st ( A = EmptyMS I or A = {x1} or A = {x2} or A = {x1,x2} ) holds
A c= {x1,x2}
let x1, x2, A be ManySortedSet of I; ( ( A = EmptyMS I or A = {x1} or A = {x2} or A = {x1,x2} ) implies A c= {x1,x2} )
assume A1:
( A = EmptyMS I or A = {x1} or A = {x2} or A = {x1,x2} )
; A c= {x1,x2}
let i be object ; PBOOLE:def 2 ( not i in I or A . i c= {x1,x2} . i )
assume A2:
i in I
; A . i c= {x1,x2} . i