let G1, G2 be strict GrammarStr ; :: thesis: ( the carrier of G1 = {a} & the Rules of G1 = {[a,{}]} & the carrier of G2 = {a} & the Rules of G2 = {[a,{}]} implies G1 = G2 )
assume that
A1: the carrier of G1 = {a} and
A2: the Rules of G1 = {[a,{}]} and
A3: the carrier of G2 = {a} and
A4: the Rules of G2 = {[a,{}]} ; :: thesis: G1 = G2
the InitialSym of G1 = a by A1, TARSKI:def 1;
hence G1 = G2 by A1, A2, A3, A4, TARSKI:def 1; :: thesis: verum