consider x being 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:11;
x in the carrier of S ;
hence not the carrier of E is empty by A1; :: according to STRUCT_0:def 1 :: thesis: verum