:: deftheorem defines PrefSpace PREFER_1:def 4 :
for X being set holds PrefSpace X = PreferenceStr(# X,({} (X,X)),(nabla X),({} (X,X)) #);