let T be Tree; :: thesis: for p, q being FinSequence st p in T & q is_a_prefix_of p holds
q in T
let p, q be FinSequence; :: thesis: ( p in T & q is_a_prefix_of p implies q in T )
assume that
A1: p in T and
A2: q is_a_prefix_of p ; :: thesis: q in T
reconsider r = p as Element of T by A1;
A3: ProperPrefixes r c= T by Def3;
( q is_a_proper_prefix_of p or q = p ) by A2;
then ( q in ProperPrefixes p or p = q ) by Th11;
hence q in T by A3; :: thesis: verum