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 t' being Element of T st
( t' in C & t is_a_proper_prefix_of t' )
let C be Chain of T; :: thesis: for t being Element of T st t in C & not C is finite holds
ex t' being Element of T st
( t' in C & t is_a_proper_prefix_of t' )
let t be Element of T; :: thesis: ( t in C & not C is finite implies ex t' being Element of T st
( t' in C & t is_a_proper_prefix_of t' ) )
assume A1: ( t in C & not C is finite ) ; :: thesis: ex t' being Element of T st
( t' in C & t is_a_proper_prefix_of t' )

now

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

proof

let t' be Element of T; :: thesis: ( t' in C implies t' is_a_prefix_of t )
assume A4: t' in C ; :: thesis: t' is_a_prefix_of t

now

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

end;

hence t' 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 A6: x in C ; :: thesis: x in (ProperPrefixes t) \/ {t}
then reconsider t' = x as Element of T ;
A7: t' is_a_prefix_of t by A3, A6;
t' in (ProperPrefixes t) \/ {t}

proof

per cases ( t' is_a_proper_prefix_of t or t' = t ) by A7, XBOOLE_0:def 8;

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

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

end;

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

then t' in {t} by TARSKI:def 1;
hence t' 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 A1; :: thesis: verum

end;

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