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

proof

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

proof

let i be set ; :: according to PBOOLE:def 4 :: thesis: ( not i in I or x . i in A . i )
assume A2: i in I ; :: thesis: x . i in A . i
then {(x . i),(y . i)} \/ (A . i) = ({x,y} . i) \/ (A . i) by Def2
.= A . i by A1, A2, PBOOLE:def 7 ;
hence x . i in A . i by ZFMISC_1:47; :: thesis: verum

end;

let i be set ; :: according to PBOOLE:def 4 :: thesis: ( not i in I or y . i in A . i )
assume A3: i in I ; :: thesis: y . i in A . i
then {(x . i),(y . i)} \/ (A . i) = ({x,y} . i) \/ (A . i) by Def2
.= A . i by A1, A3, PBOOLE:def 7 ;
hence y . i in A . i by ZFMISC_1:47; :: thesis: verum

end;

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

now

let i be set ; :: thesis: ( i in I implies ({x,y} \/ A) . i = A . i )
assume A5: i in I ; :: thesis: ({x,y} \/ A) . i = A . i
then A6: ( x . i in A . i & y . i in A . i ) by A4, PBOOLE:def 4;
thus ({x,y} \/ A) . i = ({x,y} . i) \/ (A . i) by A5, PBOOLE:def 7
.= {(x . i),(y . i)} \/ (A . i) by A5, Def2
.= A . i by A6, ZFMISC_1:48 ; :: thesis: verum

end;

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