let B be Chain of W; :: thesis: ( B is Branch-like implies not B is empty )
assume A1: ( B is Branch-like & B is empty ) ; :: thesis: contradiction
set t = the Element of W;
for q being FinSequence of NAT st q in B holds
q is_a_proper_prefix_of the Element of W by A1;
hence contradiction by A1; :: thesis: verum