let I be non empty set ; :: thesis: for i being Element of I
for A being ManySortedSet of I
for x being set st x in A . i holds
i -singleton x is ManySortedSubset of A
let i be Element of I; :: thesis: for A being ManySortedSet of I
for x being set st x in A . i holds
i -singleton x is ManySortedSubset of A
let A be ManySortedSet of I; :: thesis: for x being set st x in A . i holds
i -singleton x is ManySortedSubset of A
let x be set ; :: thesis: ( x in A . i implies i -singleton x is ManySortedSubset of A )
assume A1: x in A . i ; :: thesis: i -singleton x is ManySortedSubset of A
let y be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not y in I or (i -singleton x) . y c= A . y )
assume y in I ; :: thesis: (i -singleton x) . y c= A . y
then ( ( y = i implies (i -singleton x) . y = {x} ) & ( y <> i implies (i -singleton x) . y = {} ) ) by Th6;
hence (i -singleton x) . y c= A . y by A1, ZFMISC_1:31; :: thesis: verum