let E be Extension of S; :: thesis: not E is void
consider x being OperSymbol of S;
S is Subsignature of E by Def5;
then ( x in the carrier' of S & the carrier' of S c= the carrier' of E ) by INSTALG1:11;
hence not the carrier' of E is empty ; :: according to STRUCT_0:def 13 :: thesis: verum