:: deftheorem defines is_a_part_of JORDAN4:def 4 :
for f being V26() standard special_circular_sequence
for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Nat holds
( g is_a_part_of f,i1,i2 iff ( g is_a_part>_of f,i1,i2 or g is_a_part<_of f,i1,i2 ) );