let T be Tree; :: thesis:
let C be Chain of T; :: thesis:
let t be Element of T; :: thesis:
assume that
A1: t in C and
A2: not C is finite ; :: thesis:

now :: thesis:

assume A3: for t9 being Element of T holds
( not t9 in C or not t is_a_proper_prefix_of t9 ) ; :: thesis:
A4: for t9 being Element of T st t9 in C holds
t9 is_a_prefix_of t

proof

let t9 be Element of T; :: thesis:
assume A5: t9 in C ; :: thesis:

now :: thesis:

assume A6: not t9 is_a_prefix_of t ; :: thesis:
t,t9 are_c=-comparable by A1, A5, TREES_2:def 3;
then t is_a_prefix_of t9 by A6;
then t is_a_proper_prefix_of t9 by A6;
hence contradiction by A3, A5; :: thesis:

end;

hence t9 is_a_prefix_of t ; :: thesis:

end;

C c= (ProperPrefixes t) \/ {t}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A7: x in C ; :: thesis:
then reconsider t9 = x as Element of T ;
A8: t9 is_a_prefix_of t by A4, A7;
t9 in (ProperPrefixes t) \/ {t}

proof

per cases by A8;

suppose t9 is_a_proper_prefix_of t ; :: thesis:

then t9 in ProperPrefixes t by TREES_1:12;
hence t9 in (ProperPrefixes t) \/ {t} by XBOOLE_0:def 3; :: thesis:

end;

suppose t9 = t ; :: thesis:

then t9 in {t} by TARSKI:def 1;
hence t9 in (ProperPrefixes t) \/ {t} by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

hence x in (ProperPrefixes t) \/ {t} ; :: thesis:

end;

hence contradiction by A2; :: thesis:

end;

hence ex t9 being Element of T st
( t9 in C & t is_a_proper_prefix_of t9 ) ; :: thesis: