reconsider T = {{} } as Tree by TREES_1:48;
take T ; :: thesis: T is finite-order
take 0 ; :: according to TREES_2:def 2 :: thesis: for t being Element of T holds not t ^ <*0 *> in T
let t be Element of T; :: thesis: not t ^ <*0 *> in T
thus not t ^ <*0 *> in T by TARSKI:def 1; :: thesis: verum