let I be set ; :: thesis: for X, x1, x2 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 X, x1, x2 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
let i be set ; :: thesis: ( i in I implies X . i = {x1,x2} . i )
assume A4: i in I ; :: thesis: X . i = {x1,x2} . i
now
let a be set ; :: 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} by FUNCOP_1:19;
dom (x2 +* (i .--> a)) = I by A4, Th1;
then reconsider k2 = x2 +* (i .--> a) as ManySortedSet of I by PARTFUN1:def 4, RELAT_1:def 18;
i in {i} by TARSKI:def 1;
then A8: k2 . i = (i .--> a) . i by A7, FUNCT_4:14
.= a by FUNCOP_1:87 ;
k2 in X
proof
let q be set ; :: according to PBOOLE:def 4 :: 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;
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, PBOOLE:def 4; :: thesis: verum
end;
suppose a = x2 . i ; :: thesis: a in X . i
hence a in X . i by A3, A4, PBOOLE:def 4; :: 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} by PBOOLE:3; :: thesis: verum