let W be Tree; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 A1: ( v1 in C & v2 in C & v is_a_prefix_of v2 ) ; :: thesis: ( v1 in ProperPrefixes v or v is_a_prefix_of v1 )
then ( v1 in ProperPrefixes v2 or v2 is_a_prefix_of v1 ) by Th23;
then ( v1 is_a_proper_prefix_of v2 or v is_a_prefix_of v1 ) by A1, TREES_1:36, XBOOLE_1:1;
then v,v1 are_c=-comparable by A1, Th2, XBOOLE_0:def 9;
then ( v is_a_proper_prefix_of v1 or v = v1 or v1 is_a_proper_prefix_of v ) by XBOOLE_1:104;
hence ( v1 in ProperPrefixes v or v is_a_prefix_of v1 ) by TREES_1:36, XBOOLE_0:def 8; :: thesis: verum