:: deftheorem defines Mult_ LPSPACE1:def 2 :
for X being non empty RLSStruct
for X1 being non empty multi-closed Subset of X holds Mult_ X1 = the Mult of X | [:REAL,X1:];