:: deftheorem defines - RLTOPSP1:def 4 :
for X being non empty RLSStruct
for A being Subset of X holds - A = (- 1) * A;