theorem Th86: :: ORDERS_5:74

for A being transitive RelStr
for B, C being Subset of A
for s1 being FinSequence of A
for x being Element of A st s1 is C -asc_ordering & not x in C & B = C \/ {x} & ( for y being Element of A st y in C holds
y <= x ) holds
ex s2 being FinSequence of A st
( s2 = s1 ^ <*x*> & s2 is B -asc_ordering )