:: deftheorem defines mult-closed REALALG1:def 5 :
for L being non empty multLoopStr
for S being Subset of L holds
( S is mult-closed iff for s1, s2 being Element of L st s1 in S & s2 in S holds
s1 * s2 in S );