let I be set ; :: thesis: for x, A, B being ManySortedSet of I st ( x = A or x = B ) holds
x in {A,B}
let x, A, B be ManySortedSet of I; :: thesis: ( ( x = A or x = B ) implies x in {A,B} )
assume A1: ( x = A or x = B ) ; :: thesis: x in {A,B}

per cases ( x = A or x = B ) by A1;

suppose A2: x = A ; :: thesis: x in {A,B}

let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or x . i in {A,B} . i )
assume A3: i in I ; :: thesis: x . i in {A,B} . i
x . i in {(A . i),(B . i)} by A2, TARSKI:def 2;
hence x . i in {A,B} . i by A3, Def2; :: thesis: verum

end;

suppose A4: x = B ; :: thesis: x in {A,B}

let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or x . i in {A,B} . i )
assume A5: i in I ; :: thesis: x . i in {A,B} . i
x . i in {(A . i),(B . i)} by A4, TARSKI:def 2;
hence x . i in {A,B} . i by A5, Def2; :: thesis: verum

end;

end;