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