:: deftheorem Def3 defines -extending POLNOT_2:def 3 :
for B, C being Polish-arity-function holds
( C is B -extending iff B c= C );