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 object ; :: according to PBOOLE:def 1 :: 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 4 ;
hence x . i in A . i by ZFMISC_1:41; :: thesis: verum

end;

let i be object ; :: according to PBOOLE:def 1 :: 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 4 ;
hence y . i in A . i by ZFMISC_1:41; :: thesis: verum

end;

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

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

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

end;

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