:: deftheorem defines op0 CLASSES5:def 19 :
for x being object holds op0 x = x;