theorem :: TREES_1:49

for w, s, t being FinSequence st w ^ t is_a_proper_prefix_of w ^ s holds
t is_a_proper_prefix_of s