theorem Th8: :: AOFA_L00:8
for S, E being non empty Signature st E is S -extension holds
for a being SortSymbol of S holds a is SortSymbol of E