let I be set ; :: thesis: for x, y, X being ManySortedSet of I holds
( [|{x,y},X|] = [|{x},X|] (\/) [|{y},X|] & [|X,{x,y}|] = [|X,{x}|] (\/) [|X,{y}|] )
let x, y, X be ManySortedSet of I; :: thesis: ( [|{x,y},X|] = [|{x},X|] (\/) [|{y},X|] & [|X,{x,y}|] = [|X,{x}|] (\/) [|X,{y}|] )

now :: thesis: for i being object st i in I holds
[|{x,y},X|] . i = ([|{x},X|] (\/) [|{y},X|]) . i

let i be object ; :: thesis: ( i in I implies [|{x,y},X|] . i = ([|{x},X|] (\/) [|{y},X|]) . i )
assume A1: i in I ; :: thesis: [|{x,y},X|] . i = ([|{x},X|] (\/) [|{y},X|]) . i
hence [|{x,y},X|] . i = [:({x,y} . i),(X . i):] by PBOOLE:def 16
.= [:{(x . i),(y . i)},(X . i):] by A1, Def2
.= [:{(x . i)},(X . i):] \/ [:{(y . i)},(X . i):] by ZFMISC_1:109
.= [:({x} . i),(X . i):] \/ [:{(y . i)},(X . i):] by A1, Def1
.= [:({x} . i),(X . i):] \/ [:({y} . i),(X . i):] by A1, Def1
.= ([|{x},X|] . i) \/ [:({y} . i),(X . i):] by A1, PBOOLE:def 16
.= ([|{x},X|] . i) \/ ([|{y},X|] . i) by A1, PBOOLE:def 16
.= ([|{x},X|] (\/) [|{y},X|]) . i by A1, PBOOLE:def 4 ;
:: thesis: verum

end;

hence [|{x,y},X|] = [|{x},X|] (\/) [|{y},X|] ; :: thesis: [|X,{x,y}|] = [|X,{x}|] (\/) [|X,{y}|]

now :: thesis: for i being object st i in I holds
[|X,{x,y}|] . i = ([|X,{x}|] (\/) [|X,{y}|]) . i

let i be object ; :: thesis: ( i in I implies [|X,{x,y}|] . i = ([|X,{x}|] (\/) [|X,{y}|]) . i )
assume A2: i in I ; :: thesis: [|X,{x,y}|] . i = ([|X,{x}|] (\/) [|X,{y}|]) . i
hence [|X,{x,y}|] . i = [:(X . i),({x,y} . i):] by PBOOLE:def 16
.= [:(X . i),{(x . i),(y . i)}:] by A2, Def2
.= [:(X . i),{(x . i)}:] \/ [:(X . i),{(y . i)}:] by ZFMISC_1:109
.= [:(X . i),({x} . i):] \/ [:(X . i),{(y . i)}:] by A2, Def1
.= [:(X . i),({x} . i):] \/ [:(X . i),({y} . i):] by A2, Def1
.= ([|X,{x}|] . i) \/ [:(X . i),({y} . i):] by A2, PBOOLE:def 16
.= ([|X,{x}|] . i) \/ ([|X,{y}|] . i) by A2, PBOOLE:def 16
.= ([|X,{x}|] (\/) [|X,{y}|]) . i by A2, PBOOLE:def 4 ;
:: thesis: verum

end;

hence [|X,{x,y}|] = [|X,{x}|] (\/) [|X,{y}|] ; :: thesis: verum