let E be Extension of S; :: thesis: not E is empty
consider x being Element 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 1 :: thesis: verum