:: deftheorem Def12 defines -extending PROOFS_1:def 13 :
for R, R1 being Rule holds
( R1 is R -extending iff R c= R1 );