let e be Element of S; :: thesis: e is ManySortedSubset of M
thus e is ManySortedSubset of M by Def1; :: thesis: verum