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

now

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 5;

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:91; :: thesis: verum

end;

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

then A4: succ t = {(t ^ <*0 *>),(t ^ <*1*>)} by A1, Def2;
t ^ <*2*> in { (t ^ <*n*>) where n is Element of NAT : t ^ <*n*> in T } by A2;
then t ^ <*2*> in succ t by TREES_2:def 5;
then A5: ( t ^ <*2*> = t ^ <*0 *> or t ^ <*2*> = t ^ <*1*> ) by A4, TARSKI:def 2;

A6: now

assume <*2*> = <*0 *> ; :: thesis: contradiction
then ( <*2*> . 1 = 2 & <*2*> . 1 = 0 ) by FINSEQ_1:57;
hence contradiction ; :: thesis: verum

end;

now

assume <*2*> = <*1*> ; :: thesis: contradiction
then ( <*2*> . 1 = 2 & <*2*> . 1 = 1 ) by FINSEQ_1:57;
hence contradiction ; :: thesis: verum

end;

hence contradiction by A5, A6, FINSEQ_1:46; :: thesis: verum

end;

end;

end;

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