let W be Tree; :: thesis: for v, v1, v2 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 v, v1, v2 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 that
A1: ( v1 in C & v2 in C ) and
A2: v is_a_prefix_of v2 ; :: thesis: ( v1 in ProperPrefixes v or v is_a_prefix_of v1 )
( v1 in ProperPrefixes v2 or v2 is_a_prefix_of v1 ) by A1, Th21;
then ( v1 is_a_proper_prefix_of v2 or v is_a_prefix_of v1 ) by A2, TREES_1:12;
then v,v1 are_c=-comparable by A2, Th2;
then ( v is_a_proper_prefix_of v1 or v = v1 or v1 is_a_proper_prefix_of v ) ;
hence ( v1 in ProperPrefixes v or v is_a_prefix_of v1 ) by TREES_1:12; :: thesis: verum