let m be Element of M; :: thesis: m is total
m is multiset of I by Th2;
hence m is total ; :: thesis: verum