let I be set ; :: thesis: for x1, x2, X being ManySortedSet of I st ( for x being ManySortedSet of I holds
( x in X iff ( x = x1 or x = x2 ) ) ) holds
X = {x1,x2}
let x1, x2, X be ManySortedSet of I; :: thesis: ( ( for x being ManySortedSet of I holds
( x in X iff ( x = x1 or x = x2 ) ) ) implies X = {x1,x2} )
assume A1: for x being ManySortedSet of I holds
( x in X iff ( x = x1 or x = x2 ) ) ; :: thesis: X = {x1,x2}
then A2: x1 in X ;
A3: x2 in X by A1;

now :: thesis: for i being object st i in I holds
X . i = {x1,x2} . i

let i be object ; :: thesis: ( i in I implies X . i = {x1,x2} . i )
assume A4: i in I ; :: thesis: X . i = {x1,x2} . i

now :: thesis: for a being object holds
( a in X . i iff ( a = x1 . i or a = x2 . i ) )

let a be object ; :: thesis: ( a in X . i iff ( a = x1 . i or a = x2 . i ) )
thus ( a in X . i iff ( a = x1 . i or a = x2 . i ) ) :: thesis: verum

proof

thus ( not a in X . i or a = x1 . i or a = x2 . i ) :: thesis: ( ( a = x1 . i or a = x2 . i ) implies a in X . i )

proof

assume that
A5: a in X . i and
A6: a <> x1 . i ; :: thesis: a = x2 . i
A7: dom (i .--> a) = {i} ;
dom (x2 +* (i .--> a)) = I by A4, Th1;
then reconsider k2 = x2 +* (i .--> a) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
i in {i} by TARSKI:def 1;
then A8: k2 . i = (i .--> a) . i by A7, FUNCT_4:13
.= a by FUNCOP_1:72 ;
k2 in X

proof

let q be object ; :: according to PBOOLE:def 1 :: thesis: ( not q in I or k2 . q in X . q )
assume A9: q in I ; :: thesis: k2 . q in X . q

per cases ( i = q or i <> q ) ;

suppose i = q ; :: thesis: k2 . q in X . q

hence k2 . q in X . q by A5, A8; :: thesis: verum

end;

suppose i <> q ; :: thesis: k2 . q in X . q

then not q in dom (i .--> a) by TARSKI:def 1;
then k2 . q = x2 . q by FUNCT_4:11;
hence k2 . q in X . q by A3, A9; :: thesis: verum

end;

end;

end;

hence a = x2 . i by A1, A6, A8; :: thesis: verum

end;

assume A10: ( a = x1 . i or a = x2 . i ) ; :: thesis: a in X . i

per cases ( a = x1 . i or a = x2 . i ) by A10;

suppose a = x1 . i ; :: thesis: a in X . i

hence a in X . i by A2, A4; :: thesis: verum

end;

suppose a = x2 . i ; :: thesis: a in X . i

hence a in X . i by A3, A4; :: thesis: verum

end;

end;

end;

end;

then X . i = {(x1 . i),(x2 . i)} by TARSKI:def 2;
hence X . i = {x1,x2} . i by A4, Def2; :: thesis: verum

end;

hence X = {x1,x2} ; :: thesis: verum