defpred S₁[ DecoratedTree] means G is binary ;

A1: now :: thesis: for s being Terminal of G holds S₁[ root-tree s]

let s be Terminal of G; :: thesis: S₁[ root-tree s]
dom (root-tree s) is binary by TREES_4:3;
hence S₁[ root-tree s] by Def3; :: thesis: verum

end;

A2: for nt being NonTerminal of G
for tl, tr being Element of TS G st nt ==> <*(root-label tl),(root-label tr)*> & S₁[tl] & S₁[tr] holds
S₁[nt -tree (tl,tr)] by Th9;
thus for x being Element of TS G holds S₁[x] from BINTREE1:sch 2(A1, A2); :: thesis: verum