:: deftheorem defines op1 CLASSES5:def 20 :
for x being object holds op1 x = x .--> x;