let S be Signature; :: thesis: ( S is J -extension implies ( not S is void & not S is empty ) )
assume J is Subsignature of S ; :: according to AOFA_L00:def 2 :: thesis: ( not S is void & not S is empty )
then ( the carrier of J c= the carrier of S & the carrier' of J c= the carrier' of S ) by INSTALG1:10;
hence ( not the carrier' of S is empty & not the carrier of S is empty ) ; :: according to STRUCT_0:def 1,STRUCT_0:def 13 :: thesis: verum