let I be set ; :: thesis: for x, y, X being ManySortedSet of I holds
( ( x in X & y in X ) iff {x,y} (/\) X = {x,y} )
let x, y, X be ManySortedSet of I; :: thesis: ( ( x in X & y in X ) iff {x,y} (/\) X = {x,y} )
thus ( x in X & y in X implies {x,y} (/\) X = {x,y} ) :: thesis: ( {x,y} (/\) X = {x,y} implies ( x in X & y in X ) )

proof

assume that
A1: x in X and
A2: y in X ; :: thesis: {x,y} (/\) X = {x,y}

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

let i be object ; :: thesis: ( i in I implies ({x,y} (/\) X) . i = {x,y} . i )
assume A3: i in I ; :: thesis: ({x,y} (/\) X) . i = {x,y} . i
then A4: x . i in X . i by A1;
A5: y . i in X . i by A2, A3;
thus ({x,y} (/\) X) . i = ({x,y} . i) /\ (X . i) by A3, PBOOLE:def 5
.= {(x . i),(y . i)} /\ (X . i) by A3, Def2
.= {(x . i),(y . i)} by A4, A5, ZFMISC_1:47
.= {x,y} . i by A3, Def2 ; :: thesis: verum

end;

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

end;

assume A6: {x,y} (/\) X = {x,y} ; :: thesis: ( x in X & y in X )
thus x in X :: thesis: y in X

proof

let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or x . i in X . i )
assume A7: i in I ; :: thesis: x . i in X . i
then {(x . i),(y . i)} /\ (X . i) = ({x,y} . i) /\ (X . i) by Def2
.= ({x,y} (/\) X) . i by A7, PBOOLE:def 5
.= {(x . i),(y . i)} by A6, A7, Def2 ;
hence x . i in X . i by ZFMISC_1:55; :: thesis: verum

end;

let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or y . i in X . i )
assume A8: i in I ; :: thesis: y . i in X . i
then {(x . i),(y . i)} /\ (X . i) = ({x,y} . i) /\ (X . i) by Def2
.= ({x,y} (/\) X) . i by A8, PBOOLE:def 5
.= {(x . i),(y . i)} by A6, A8, Def2 ;
hence y . i in X . i by ZFMISC_1:55; :: thesis: verum