let W be Tree; :: thesis: for v1, v2 being FinSequence
for C being Chain of W st v1 in C & v2 in C & not v1 in ProperPrefixes v2 holds
v2 is_a_prefix_of v1
let v1, v2 be FinSequence; :: thesis: for C being Chain of W st v1 in C & v2 in C & not v1 in ProperPrefixes v2 holds
v2 is_a_prefix_of v1
let C be Chain of W; :: thesis: ( v1 in C & v2 in C & not v1 in ProperPrefixes v2 implies v2 is_a_prefix_of v1 )
assume A1: ( v1 in C & v2 in C ) ; :: thesis: ( v1 in ProperPrefixes v2 or v2 is_a_prefix_of v1 )
then reconsider p = v1, q = v2 as Element of W ;
assume A2: not v1 in ProperPrefixes v2 ; :: thesis: v2 is_a_prefix_of v1
A3: p,q are_c=-comparable by A1, Def3;
A4: not v1 is_a_proper_prefix_of v2 by A2, TREES_1:12;
( v1 is_a_prefix_of v2 or v2 is_a_prefix_of v1 ) by A3;
hence v2 is_a_prefix_of v1 by A4; :: thesis: verum