:: deftheorem Def1 defines maxPrefix HELLY:def 1 :
for p, q, b₃ being FinSequence holds
( b₃ = maxPrefix (p,q) iff ( b₃ is_a_prefix_of p & b₃ is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds
r is_a_prefix_of b₃ ) ) );