let I be set ; for A, X being ManySortedSet of I st A c= X holds
[|A,A|] c= [|X,X|]
let A, X be ManySortedSet of I; ( A c= X implies [|A,A|] c= [|X,X|] )
assume A1:
A c= X
; [|A,A|] c= [|X,X|]
let i be object ; PBOOLE:def 2 ( not i in I or [|A,A|] . i c= [|X,X|] . i )
assume A2:
i in I
; [|A,A|] . i c= [|X,X|] . i
then
A . i c= X . i
by A1;
then
[:(A . i),(A . i):] c= [:(X . i),(X . i):]
by ZFMISC_1:96;
then
[|A,A|] . i c= [:(X . i),(X . i):]
by A2, PBOOLE:def 16;
hence
[|A,A|] . i c= [|X,X|] . i
by A2, PBOOLE:def 16; verum