let W be Tree; :: thesis: for p, q being FinSequence of NAT
for B being Branch of W st p is_a_prefix_of q & q in B holds
p in B
let p, q be FinSequence of NAT ; :: thesis: for B being Branch of W st p is_a_prefix_of q & q in B holds
p in B
let B be Branch of W; :: thesis: ( p is_a_prefix_of q & q in B implies p in B )
assume p is_a_prefix_of q ; :: thesis: ( not q in B or p in B )
then ( p is_a_proper_prefix_of q or p = q ) ;
then A1: ( p in ProperPrefixes q or p = q ) by TREES_1:def 2;
assume A2: q in B ; :: thesis: p in B
then ProperPrefixes q c= B by Def7;
hence p in B by A1, A2; :: thesis: verum