let T be Tree; :: thesis: for C being Chain of T
for t being Element of T st t in C & not C is finite holds
ex t9 being Element of T st
( t9 in C & t is_a_proper_prefix_of t9 )
let C be Chain of T; :: thesis: for t being Element of T st t in C & not C is finite holds
ex t9 being Element of T st
( t9 in C & t is_a_proper_prefix_of t9 )
let t be Element of T; :: thesis: ( t in C & not C is finite implies ex t9 being Element of T st
( t9 in C & t is_a_proper_prefix_of t9 ) )
assume that
A1: t in C and
A2: not C is finite ; :: thesis: ex t9 being Element of T st
( t9 in C & t is_a_proper_prefix_of t9 )

now

assume A3: for t9 being Element of T holds
( not t9 in C or not t is_a_proper_prefix_of t9 ) ; :: thesis: contradiction
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: ( t9 in C implies t9 is_a_prefix_of t )
assume A5: t9 in C ; :: thesis: t9 is_a_prefix_of t

now

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

end;

hence t9 is_a_prefix_of t ; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in C or x in (ProperPrefixes t) \/ {t} )
assume A7: x in C ; :: thesis: x in (ProperPrefixes t) \/ {t}
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 ( t9 is_a_proper_prefix_of t or t9 = t ) by A8, XBOOLE_0:def 8;

suppose t9 is_a_proper_prefix_of t ; :: thesis: t9 in (ProperPrefixes t) \/ {t}

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

end;

suppose t9 = t ; :: thesis: t9 in (ProperPrefixes t) \/ {t}

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

end;

end;

end;

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

end;

hence contradiction by A2; :: thesis: verum

end;

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