let T be Tree; :: thesis: for t being Element of T holds ProperPrefixes t is finite Chain of T
let t be Element of T; :: thesis: ProperPrefixes t is finite Chain of T
( ProperPrefixes t c= T & ( for p, q being FinSequence of NAT st p in ProperPrefixes t & q in ProperPrefixes t holds
p,q are_c=-comparable ) ) by TREES_1:18, TREES_1:def 3;
hence ProperPrefixes t is finite Chain of T by TREES_2:def 3; :: thesis: verum