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

assume A1: T is binary ; :: thesis: 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

hence
T is finite-order
by TREES_2:def 2; :: thesis: verumlet 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;

end;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 )
;

end;

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

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;

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;assume <*2*> = <*0*> ; :: thesis: contradiction

hence contradiction by A6, FINSEQ_1:40; :: thesis: verum

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

t ^ <*2*> in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in T }
by A2;A8:
<*2*> . 1 = 2
by FINSEQ_1:40;

assume <*2*> = <*1*> ; :: thesis: contradiction

hence contradiction by A8, FINSEQ_1:40; :: thesis: verum

end;assume <*2*> = <*1*> ; :: thesis: contradiction

hence contradiction by A8, FINSEQ_1:40; :: thesis: verum

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