let I be set ; :: thesis: for X, x1, x2 being ManySortedSet of st X = {x1,x2} holds
for x being ManySortedSet of st ( x = x1 or x = x2 ) holds
x in X
let X, x1, x2 be ManySortedSet of ; :: thesis: ( X = {x1,x2} implies for x being ManySortedSet of st ( x = x1 or x = x2 ) holds
x in X )
assume A1: X = {x1,x2} ; :: thesis: for x being ManySortedSet of st ( x = x1 or x = x2 ) holds
x in X
let x be ManySortedSet of ; :: thesis: ( ( x = x1 or x = x2 ) implies x in X )
assume A2: ( x = x1 or x = x2 ) ; :: thesis: x in X
let i be set ; :: according to PBOOLE:def 4 :: thesis: ( not i in I or x . i in X . i )
assume i in I ; :: thesis: x . i in X . i
then A3: X . i = {(x1 . i),(x2 . i)} by A1, Def2;

per cases ( x = x1 or x = x2 ) by A2;

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

hence x . i in X . i by A3, TARSKI:def 2; :: thesis: verum

end;

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

hence x . i in X . i by A3, TARSKI:def 2; :: thesis: verum

end;

end;