thus ( S <> {} implies |.S.| is ManySortedSet of I ) :: thesis: ( not S <> {} implies EmptyMS I is ManySortedSet of I )
proof
assume S <> {} ; :: thesis: |.S.| is ManySortedSet of I
then dom |.S.| = I by Th13;
hence |.S.| is ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18; :: thesis: verum
end;
thus ( not S <> {} implies EmptyMS I is ManySortedSet of I ) ; :: thesis: verum