:: deftheorem defines \~ DICKSON:def 7 :
for R being RelStr holds R \~ = RelStr(# the carrier of R,( the InternalRel of R \~) #);