reconsider E = the non empty non void Signature +* J as non empty non void Signature ;
take E ; :: thesis: E is J -extension
E is Extension of J by ALGSPEC1:48;
hence J is Subsignature of E by ALGSPEC1:def 5; :: according to AOFA_L00:def 2 :: thesis: verum