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
consider t being Element of W;
A2: for q being FinSequence of NAT st q in B holds
q is_a_proper_prefix_of t by A1;
thus contradiction by A1, A2, Def7; :: thesis: verum