:: deftheorem defines is_S-Seq_joining JORDAN3:def 2 :
for g being FinSequence of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) holds
( g is_S-Seq_joining p1,p2 iff ( g is being_S-Seq & g . 1 = p1 & g . (len g) = p2 ) );