:: deftheorem defines corestr WAYBEL18:def 7 :
for X being 1-sorted
for Y being non empty TopStruct
for f being Function of X,Y holds corestr f = f;