let W be Tree; :: thesis: for B being Branch of W holds {} in B
let B be Branch of W; :: thesis: {} in B
set x = the Element of B;
reconsider x = the Element of B as Element of W ;
<*> NAT is_a_prefix_of x ;
hence {} in B by Th25; :: thesis: verum