let I be set ; for A, B, X, Y being ManySortedSet of I st A is V2() & ( [|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|] ) holds
B c= Y
let A, B, X, Y be ManySortedSet of I; ( A is V2() & ( [|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|] ) implies B c= Y )
assume that
A1:
A is V2()
and
A2:
( [|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|] )
; B c= Y
per cases
( [|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|] )
by A2;
suppose A3:
[|A,B|] c= [|X,Y|]
;
B c= Ylet i be
object ;
PBOOLE:def 2 ( not i in I or B . i c= Y . i )assume A4:
i in I
;
B . i c= Y . ithen
[|A,B|] . i c= [|X,Y|] . i
by A3;
then
[:(A . i),(B . i):] c= [|X,Y|] . i
by A4, PBOOLE:def 16;
then A5:
[:(A . i),(B . i):] c= [:(X . i),(Y . i):]
by A4, PBOOLE:def 16;
not
A . i is
empty
by A1, A4;
hence
B . i c= Y . i
by A5, ZFMISC_1:115;
verum end; suppose A6:
[|B,A|] c= [|Y,X|]
;
B c= Ylet i be
object ;
PBOOLE:def 2 ( not i in I or B . i c= Y . i )assume A7:
i in I
;
B . i c= Y . ithen
[|B,A|] . i c= [|Y,X|] . i
by A6;
then
[:(B . i),(A . i):] c= [|Y,X|] . i
by A7, PBOOLE:def 16;
then A8:
[:(B . i),(A . i):] c= [:(Y . i),(X . i):]
by A7, PBOOLE:def 16;
not
A . i is
empty
by A1, A7;
hence
B . i c= Y . i
by A8, ZFMISC_1:115;
verum end;