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

proof

let i be object ; :: according to PBOOLE:def 2 :: 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:7;
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 object ; :: according to PBOOLE:def 2 :: 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:7;
then {y} . i c= {(x . i),(y . i)} by A2, Def1;
hence {y} . i c= {x,y} . i by A2, Def2; :: thesis: verum