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

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