:: deftheorem Def9 defines -extending POLNOT_2:def 8 :
for T, U being Polish-language holds
( U is T -extending iff T c= U );