let I be set ; :: thesis: for x, y being ManySortedSet of holds
( {x} c= {x,y} & {y} c= {x,y} )
let x, y be ManySortedSet of ; :: thesis: ( {x} c= {x,y} & {y} c= {x,y} )
thus {x} c= {x,y} :: thesis: {y} c= {x,y}

proof

let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or {x} . i c= {x,y} . i )
assume A1: i in I ; :: thesis: {x} . i c= {x,y} . i
{(x . i)} c= {(x . i),(y . i)} by ZFMISC_1:12;
then {x} . i c= {(x . i),(y . i)} by A1, Def1;
hence {x} . i c= {x,y} . i by A1, Def2; :: thesis: verum

end;

let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or {y} . i c= {x,y} . i )
assume A2: i in I ; :: thesis: {y} . i c= {x,y} . i
{(y . i)} c= {(x . i),(y . i)} by ZFMISC_1:12;
then {y} . i c= {(x . i),(y . i)} by A2, Def1;
hence {y} . i c= {x,y} . i by A2, Def2; :: thesis: verum