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
A1: ProperPrefixes t c= T by TREES_1:def 5;
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:42;
hence ProperPrefixes t is finite Chain of T by A1, TREES_2:def 3; :: thesis: verum