theorem :: JORDAN5A:22

for P, Q being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds
ex EX being Point of (TOP-REAL 2) st
( EX in P /\ Q & ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) ) )