let I be set ; for x, y, A being ManySortedSet of I st {x,y} c= {A} holds
{x,y} = {A}
let x, y, A be ManySortedSet of I; ( {x,y} c= {A} implies {x,y} = {A} )
assume A1:
{x,y} c= {A}
; {x,y} = {A}
now for i being object st i in I holds
{x,y} . i = {A} . ilet i be
object ;
( i in I implies {x,y} . i = {A} . i )assume A2:
i in I
;
{x,y} . i = {A} . ithen
{x,y} . i c= {A} . i
by A1;
then
{(x . i),(y . i)} c= {A} . i
by A2, Def2;
then A3:
{(x . i),(y . i)} c= {(A . i)}
by A2, Def1;
thus {x,y} . i =
{(x . i),(y . i)}
by A2, Def2
.=
{(A . i)}
by A3, ZFMISC_1:21
.=
{A} . i
by A2, Def1
;
verum end;
hence
{x,y} = {A}
; verum