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

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