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