:: deftheorem Def1 defines First_Point JORDAN5C:def 1 :
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
for b₅ being Point of (TOP-REAL 2) holds
( b₅ = First_Point (P,p1,p2,Q) iff ( b₅ in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b₅ & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) ) );