let I be set ; :: thesis: for A being ManySortedSet of I
for B being non-empty ManySortedSet of I st A is Element of B holds
A in B
let A be ManySortedSet of I; :: thesis: for B being non-empty ManySortedSet of I st A is Element of B holds
A in B
let B be non-empty ManySortedSet of I; :: thesis: ( A is Element of B implies A in B )
assume A1: A is Element of B ; :: thesis: A in B
let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or A . i in B . i )
assume A2: i in I ; :: thesis: A . i in B . i
then A3: B . i <> {} ;
A . i is Element of B . i by A1, A2, PBOOLE:def 14;
hence A . i in B . i by A3; :: thesis: verum