:: deftheorem defines \~ DICKSON:def 6 :
for R being Relation holds R \~ = R \ (R ~);