set x = the OperSymbol of S;
let E be Extension of S; :: thesis: not E is void
S is Subsignature of E by Def5;
then A1: the carrier' of S c= the carrier' of E by INSTALG1:10;
the OperSymbol of S in the carrier' of S ;
hence not the carrier' of E is empty by A1; :: according to STRUCT_0:def 13 :: thesis: verum