thus the Sorts of MSClosureStr(# M,F #) is non-empty ; :: according to MSUALG_1:def 8 :: thesis: verum