let W be Tree; for v1, v2, v being FinSequence
for C being Chain of W st v1 in C & v2 in C & v is_a_prefix_of v2 & not v1 in ProperPrefixes v holds
v is_a_prefix_of v1
let v1, v2, v be FinSequence; for C being Chain of W st v1 in C & v2 in C & v is_a_prefix_of v2 & not v1 in ProperPrefixes v holds
v is_a_prefix_of v1
let C be Chain of W; ( v1 in C & v2 in C & v is_a_prefix_of v2 & not v1 in ProperPrefixes v implies v is_a_prefix_of v1 )
assume that
A1:
( v1 in C & v2 in C )
and
A2:
v is_a_prefix_of v2
; ( v1 in ProperPrefixes v or v is_a_prefix_of v1 )
A3:
( v1 in ProperPrefixes v2 or v2 is_a_prefix_of v1 )
by A1, Th23;
A4:
( v1 is_a_proper_prefix_of v2 or v is_a_prefix_of v1 )
by A2, A3, TREES_1:36, XBOOLE_1:1;
A5:
v,v1 are_c=-comparable
by A2, A4, Th2, XBOOLE_0:def 9;
A6:
( v is_a_proper_prefix_of v1 or v = v1 or v1 is_a_proper_prefix_of v )
by A5, XBOOLE_1:104;
thus
( v1 in ProperPrefixes v or v is_a_prefix_of v1 )
by A6, TREES_1:36, XBOOLE_0:def 8; verum