let I be set ; 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; ( X c= Y implies ( [|X,Z|] c= [|Y,Z|] & [|Z,X|] c= [|Z,Y|] ) )
assume A1:
X c= Y
; ( [|X,Z|] c= [|Y,Z|] & [|Z,X|] c= [|Z,Y|] )
thus
[|X,Z|] c= [|Y,Z|]
[|Z,X|] c= [|Z,Y|]proof
let i be
object ;
PBOOLE:def 2 ( not i in I or [|X,Z|] . i c= [|Y,Z|] . i )
assume A2:
i in I
;
[|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;
verum
end;
let i be object ; PBOOLE:def 2 ( not i in I or [|Z,X|] . i c= [|Z,Y|] . i )
assume A3:
i in I
; [|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; verum