let I be set ; :: thesis: for x being ManySortedSet of I holds x in {x}
let x be ManySortedSet of I; :: thesis: x in {x}
let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or x . i in {x} . i )
assume A1: i in I ; :: thesis: x . i in {x} . i
x . i in {(x . i)} by TARSKI:def 1;
hence x . i in {x} . i by A1, Def1; :: thesis: verum