:: deftheorem Def5 defines Extension ALGSPEC1:def 5 :
for S, b₂ being Signature holds
( b₂ is Extension of S iff S is Subsignature of b₂ );