let W be Tree; :: thesis: for p, q being FinSequence of NAT
for C being Chain of W st p in C & q in C & len p <= len q holds
p is_a_prefix_of q
let p, q be FinSequence of NAT ; :: thesis: for C being Chain of W st p in C & q in C & len p <= len q holds
p is_a_prefix_of q
let C be Chain of W; :: thesis: ( p in C & q in C & len p <= len q implies p is_a_prefix_of q )
assume ( p in C & q in C & len p <= len q & not p is_a_prefix_of q ) ; :: thesis: contradiction
then ( q in ProperPrefixes p & not q is_a_proper_prefix_of p ) by Th21, TREES_1:6;
hence contradiction by TREES_1:12; :: thesis: verum