let W be Tree; :: thesis: for B being Branch of W holds {} in B
let B be Branch of W; :: thesis: {} in B
consider x being Element of B;
reconsider x = x as Element of W ;
A1: <*> NAT is_a_prefix_of x by XBOOLE_1:2;
thus {} in B by A1, Th27; :: thesis: verum