let I be set ; :: thesis: for A, B being ManySortedSet of I st A in B holds
A is Element of B
let A, B be ManySortedSet of I; :: thesis: ( A in B implies A is Element of B )
assume A1: A in B ; :: thesis: A is Element of B
let i be object ; :: according to PBOOLE:def 14 :: thesis: ( not i in I or A . i is Element of B . i )
assume i in I ; :: thesis: A . i is Element of B . i
hence A . i is Element of B . i by A1; :: thesis: verum