let T be Tree; :: thesis: ( T is binary implies T is finite-order )
assume A1: T is binary ; :: thesis: T is finite-order

now :: thesis: for t being Element of T holds not t ^ <*2*> in T

let t be Element of T; :: thesis: not t ^ <*2*> in T
assume A2: t ^ <*2*> in T ; :: thesis: contradiction
then A3: t ^ <*0*> in T by TREES_1:def 3;

per cases ( t in Leaves T or not t in Leaves T ) ;

suppose t in Leaves T ; :: thesis: contradiction

hence contradiction by A3, TREES_1:54; :: thesis: verum

end;

suppose A4: not t in Leaves T ; :: thesis: contradiction

A5: now :: thesis: not <*2*> = <*0*>

A6: <*2*> . 1 = 2 by FINSEQ_1:40;
assume <*2*> = <*0*> ; :: thesis: contradiction
hence contradiction by A6, FINSEQ_1:40; :: thesis: verum

end;

A7: now :: thesis: not <*2*> = <*1*>

A8: <*2*> . 1 = 2 by FINSEQ_1:40;
assume <*2*> = <*1*> ; :: thesis: contradiction
hence contradiction by A8, FINSEQ_1:40; :: thesis: verum

end;

t ^ <*2*> in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in T } by A2;
then A9: t ^ <*2*> in succ t by TREES_2:def 5;
succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A1, A4;
then ( t ^ <*2*> = t ^ <*0*> or t ^ <*2*> = t ^ <*1*> ) by A9, TARSKI:def 2;
hence contradiction by A5, A7, FINSEQ_1:33; :: thesis: verum

end;

end;

end;

hence T is finite-order by TREES_2:def 2; :: thesis: verum