let G, G9 be non empty DTConstrStr ; :: thesis: ( Terminals G c= Terminals G9 & the Rules of G c= the Rules of G9 implies TS G c= TS G9 )
assume that
A1: Terminals G c= Terminals G9 and
A2: the Rules of G c= the Rules of G9 ; :: thesis: TS G c= TS G9
A3: the carrier of G9 = (Terminals G9) \/ (NonTerminals G9) by LANG1:1;
A4: the carrier of G c= the carrier of G9 by A1, A2, Th115;
defpred S₁[ set ] means $1 in TS G9;
A5: for s being Symbol of G st s in Terminals G holds
S₁[ root-tree s]

proof

let s be Symbol of G; :: thesis: ( s in Terminals G implies S₁[ root-tree s] )
assume A6: s in Terminals G ; :: thesis: S₁[ root-tree s]
then reconsider s9 = s as Symbol of G9 by A1, A3, XBOOLE_0:def 3;
root-tree s = root-tree s9 ;
hence S₁[ root-tree s] by A1, A6, DTCONSTR:def 1; :: thesis: verum

end;

A7: for nt being Symbol of G
for ts being FinSequence of TS G st nt ==> roots ts & ( for t being DecoratedTree of the carrier of G st t in rng ts holds
S₁[t] ) holds
S₁[nt -tree ts]

proof

let n be Symbol of G; :: thesis: for ts being FinSequence of TS G st n ==> roots ts & ( for t being DecoratedTree of the carrier of G st t in rng ts holds
S₁[t] ) holds
S₁[n -tree ts]
let s be FinSequence of TS G; :: thesis: ( n ==> roots s & ( for t being DecoratedTree of the carrier of G st t in rng s holds
S₁[t] ) implies S₁[n -tree s] )
assume that
A8: [n,(roots s)] in the Rules of G and
A9: for t being DecoratedTree of the carrier of G st t in rng s holds
S₁[t] ; :: according to LANG1:def 1 :: thesis: S₁[n -tree s]
rng s c= TS G9 by A9;
then reconsider s9 = s as FinSequence of TS G9 by FINSEQ_1:def 4;
reconsider n9 = n as Symbol of G9 by A4;
n9 ==> roots s9 by A2, A8;
hence S₁[n -tree s] by DTCONSTR:def 1; :: thesis: verum

end;

A10: for t being DecoratedTree of the carrier of G st t in TS G holds
S₁[t] from DTCONSTR:sch 7(A5, A7);
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in TS G or x in TS G9 )
assume A11: x in TS G ; :: thesis: x in TS G9
then reconsider t = x as Element of FinTrees the carrier of G ;
S₁[t] by A10, A11;
hence x in TS G9 ; :: thesis: verum