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 W is finite-order ; :: thesis: succ w is finite
then consider n being Nat such that
A1: for w being Element of W ex B being finite set st
( B = succ w & card B <= n ) by Th17;
ex B being finite set st
( B = succ w & card B <= n ) by A1;
hence succ w is finite ; :: thesis: verum