defpred S_{1}[ DecoratedTree] means G is binary ;

for tl, tr being Element of TS G st nt ==> <*(root-label tl),(root-label tr)*> & S_{1}[tl] & S_{1}[tr] holds

S_{1}[nt -tree (tl,tr)]
by Th9;

thus for x being Element of TS G holds S_{1}[x]
from BINTREE1:sch 2(A1, A2); :: thesis: verum

A1: now :: thesis: for s being Terminal of G holds S_{1}[ root-tree s]

A2:
for nt being NonTerminal of Glet s be Terminal of G; :: thesis: S_{1}[ root-tree s]

dom (root-tree s) is binary by TREES_4:3;

hence S_{1}[ root-tree s]
by Def3; :: thesis: verum

end;dom (root-tree s) is binary by TREES_4:3;

hence S

for tl, tr being Element of TS G st nt ==> <*(root-label tl),(root-label tr)*> & S

S

thus for x being Element of TS G holds S