:: deftheorem defines is_postposition_of FINSEQ_8:def 9 :
for f, g being FinSequence holds
( g is_postposition_of f iff Rev g is_preposition_of Rev f );