set A = the non empty set ;
set P = the Relation of the non empty set ,( the non empty set *);
set I = the Element of the non empty set ;
take GrammarStr(# the non empty set , the Element of the non empty set , the Relation of the non empty set ,( the non empty set *) #) ; :: thesis: not GrammarStr(# the non empty set , the Element of the non empty set , the Relation of the non empty set ,( the non empty set *) #) is empty
thus not the carrier of GrammarStr(# the non empty set , the Element of the non empty set , the Relation of the non empty set ,( the non empty set *) #) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum