let W be Tree; :: thesis: for w being Element of W st W is finite-order holds
succ w is finite
let w be Element of W; :: thesis: ( W is finite-order implies succ w is finite )
assume A1: W is finite-order ; :: thesis: succ w is finite
consider n being Element of NAT such that
A2: for w being Element of W ex B being finite set st
( B = succ w & card B <= n ) by A1, Th19;
A3: ex B being finite set st
( B = succ w & card B <= n ) by A2;
thus succ w is finite by A3; :: thesis: verum