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