let S, E be non empty Signature; :: thesis: ( E is S -extension implies for a being SortSymbol of S holds a is SortSymbol of E )
assume S is Subsignature of E ; :: according to AOFA_L00:def 2 :: thesis: for a being SortSymbol of S holds a is SortSymbol of E
then the carrier of S c= the carrier of E by INSTALG1:10;
hence for a being SortSymbol of S holds a is SortSymbol of E ; :: thesis: verum