:: deftheorem defines ` ROBBINS1:def 3 :
for L being non empty ComplStr
for x being Element of L holds x ` = the Compl of L . x;