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

proof

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

end;

A7: for nt being Symbol of
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 ; :: 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 G'

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng s or x in TS G' )
assume A10: x in rng s ; :: thesis: x in TS G'
then x is DecoratedTree of the carrier of G by TREES_3:def 6;
hence x in TS G' by A9, A10; :: thesis: verum

end;

then reconsider s' = s as FinSequence of TS G' by FINSEQ_1:def 4;
n in the carrier of G ;
then reconsider n' = n as Symbol of by A4;
n' ==> roots s' by A2, A8, LANG1:def 1;
hence S₁[n -tree s] by DTCONSTR:def 4; :: thesis: verum

end;

A11: 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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in TS G or x in TS G' )
assume A12: x in TS G ; :: thesis: x in TS G'
then reconsider t = x as Element of FinTrees the carrier of G ;
S₁[t] by A11, A12;
hence x in TS G' ; :: thesis: verum