let S1 be OrderSortedSign; :: thesis: for M being ManySortedSet of the carrier of S1 holds M c= OSCl M
let M be ManySortedSet of the carrier of S1; :: thesis: M c= OSCl M
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in the carrier of S1 or M . i c= (OSCl M) . i )
assume i in the carrier of S1 ; :: thesis: M . i c= (OSCl M) . i
then reconsider s = i as SortSymbol of S1 ;
M . s in { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ;
then M . s c= union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } by ZFMISC_1:74;
hence M . i c= (OSCl M) . i by Def4; :: thesis: verum