let I be set ; :: thesis: for x, X being ManySortedSet of I st {x} (\/) X = X holds
x in X
let x, X be ManySortedSet of I; :: thesis: ( {x} (\/) X = X implies x in X )
assume A1: {x} (\/) X = X ; :: 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 A2: i in I ; :: thesis: x . i in X . i
then {(x . i)} \/ (X . i) = ({x} . i) \/ (X . i) by Def1
.= X . i by A1, A2, PBOOLE:def 4 ;
hence x . i in X . i by ZFMISC_1:39; :: thesis: verum