let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st X c= Y holds
( [|X,Z|] c= [|Y,Z|] & [|Z,X|] c= [|Z,Y|] )
let X, Y, Z be ManySortedSet of I; :: thesis: ( X c= Y implies ( [|X,Z|] c= [|Y,Z|] & [|Z,X|] c= [|Z,Y|] ) )
assume A1: X c= Y ; :: thesis: ( [|X,Z|] c= [|Y,Z|] & [|Z,X|] c= [|Z,Y|] )
thus [|X,Z|] c= [|Y,Z|] :: thesis: [|Z,X|] c= [|Z,Y|]

proof

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or [|X,Z|] . i c= [|Y,Z|] . i )
assume A2: i in I ; :: thesis: [|X,Z|] . i c= [|Y,Z|] . i
then X . i c= Y . i by A1;
then [:(X . i),(Z . i):] c= [:(Y . i),(Z . i):] by ZFMISC_1:95;
then [|X,Z|] . i c= [:(Y . i),(Z . i):] by A2, PBOOLE:def 16;
hence [|X,Z|] . i c= [|Y,Z|] . i by A2, PBOOLE:def 16; :: thesis: verum

end;

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or [|Z,X|] . i c= [|Z,Y|] . i )
assume A3: i in I ; :: thesis: [|Z,X|] . i c= [|Z,Y|] . i
then X . i c= Y . i by A1;
then [:(Z . i),(X . i):] c= [:(Z . i),(Y . i):] by ZFMISC_1:95;
then [|Z,X|] . i c= [:(Z . i),(Y . i):] by A3, PBOOLE:def 16;
hence [|Z,X|] . i c= [|Z,Y|] . i by A3, PBOOLE:def 16; :: thesis: verum