theorem :: JGRAPH_5:69

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2)
for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds
for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p4 & g . 1 = p2 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g