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 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 Th19;
ex B being finite set st
( B = succ w & card B <= n ) by A2;
hence succ w is finite ; :: thesis: verum