let I be set ; :: thesis: for A, X being ManySortedSet of I st A c= X holds
[|A,A|] c= [|X,X|]
let A, X be ManySortedSet of I; :: thesis: ( A c= X implies [|A,A|] c= [|X,X|] )
assume A1: A c= X ; :: thesis: [|A,A|] c= [|X,X|]
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or [|A,A|] . i c= [|X,X|] . i )
assume A2: i in I ; :: thesis: [|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; :: thesis: verum