let I be set ; :: thesis: for x, X, y being ManySortedSet of holds
( ( x in X & y in X ) iff {x,y} /\ X = {x,y} )
let x, X, y be ManySortedSet of ; :: 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 A1: ( x in X & y in X ) ; :: thesis: {x,y} /\ X = {x,y}

now

let i be set ; :: thesis: ( i in I implies ({x,y} /\ X) . i = {x,y} . i )
assume A2: i in I ; :: thesis: ({x,y} /\ X) . i = {x,y} . i
then A3: ( x . i in X . i & y . i in X . i ) by A1, PBOOLE:def 4;
thus ({x,y} /\ X) . i = ({x,y} . i) /\ (X . i) by A2, PBOOLE:def 8
.= {(x . i),(y . i)} /\ (X . i) by A2, Def2
.= {(x . i),(y . i)} by A3, ZFMISC_1:53
.= {x,y} . i by A2, Def2 ; :: thesis: verum

end;

hence {x,y} /\ X = {x,y} by PBOOLE:3; :: thesis: verum

end;

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

proof

let i be set ; :: according to PBOOLE:def 4 :: thesis: ( not i in I or x . i in X . i )
assume A5: 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 A5, PBOOLE:def 8
.= {(x . i),(y . i)} by A4, A5, Def2 ;
hence x . i in X . i by ZFMISC_1:63; :: thesis: verum

end;

let i be set ; :: according to PBOOLE:def 4 :: thesis: ( not i in I or y . i in X . i )
assume A6: 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 A6, PBOOLE:def 8
.= {(x . i),(y . i)} by A4, A6, Def2 ;
hence y . i in X . i by ZFMISC_1:63; :: thesis: verum