let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NonTerminals D1 or x in NonTerminals D2 )
assume x in NonTerminals D1 ; :: thesis: x in NonTerminals D2
then ex s being Symbol of D1 st
( x = s & ex n being FinSequence st s ==> n ) ;
then consider s being Symbol of D1, n being FinSequence such that
A3: x = s and
A4: s ==> n ;
A5: [s,n] in the Rules of D1 by A4;
then [s,n] in the Rules of D2 by A1;
then reconsider s9 = s as Symbol of D2 by ZFMISC_1:87;
s9 ==> n by A1, A5;
hence x in NonTerminals D2 by A3; :: thesis: verum

let x be object ; :: thesis: ( x in the carrier of D1 /\ (Terminals D2) implies x in Terminals D1 )
assume A6: x in the carrier of D1 /\ (Terminals D2) ; :: thesis: x in Terminals D1
then A7: x in Terminals D2 by XBOOLE_0:def 4;
reconsider s9 = x as Symbol of D1 by A6, XBOOLE_0:def 4;
reconsider s = x as Symbol of D2 by A6;
assume not x in Terminals D1 ; :: thesis: contradiction
then consider n being FinSequence such that
A8: s9 ==> n ;
[s9,n] in the Rules of D1 by A8;
then s ==> n by A1;
then for s being Symbol of D2 holds
( not x = s or ex n being FinSequence st s ==> n ) ;
hence contradiction by A7; :: thesis: verum