:: deftheorem Def2 defines -extension AOFA_L00:def 2 :
for S, E being Signature holds
( E is S -extension iff S is Subsignature of E );