let p1, p2, p3, p4 be Point of (TOP-REAL 2); :: thesis: 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 } & p1,p2,p3,p4 are_in_this_order_on 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 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

let P be non empty compact Subset of (TOP-REAL 2); :: thesis: for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1,p2,p3,p4 are_in_this_order_on 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 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

let C0 be Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1,p2,p3,p4 are_in_this_order_on P implies 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 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g )

assume that

A1: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } and

A2: p1,p2,p3,p4 are_in_this_order_on P ; :: thesis: 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 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1,p2,p3,p4 are_in_this_order_on 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 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

let P be non empty compact Subset of (TOP-REAL 2); :: thesis: for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1,p2,p3,p4 are_in_this_order_on 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 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

let C0 be Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1,p2,p3,p4 are_in_this_order_on P implies 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 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g )

assume that

A1: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } and

A2: p1,p2,p3,p4 are_in_this_order_on P ; :: thesis: 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 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

per cases
( ( LE p1,p2,P & LE p2,p3,P & LE p3,p4,P ) or ( LE p2,p3,P & LE p3,p4,P & LE p4,p1,P ) or ( LE p3,p4,P & LE p4,p1,P & LE p1,p2,P ) or ( LE p4,p1,P & LE p1,p2,P & LE p2,p3,P ) )
by A2, JORDAN17:def 1;

end;

suppose
( LE p1,p2,P & LE p2,p3,P & LE p3,p4,P )
; :: thesis: 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 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

rng f meets rng g

hence
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 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g by A1, JGRAPH_5:68; :: thesis: verum

end;rng f meets rng g by A1, JGRAPH_5:68; :: thesis: verum

suppose
( LE p2,p3,P & LE p3,p4,P & LE p4,p1,P )
; :: thesis: 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 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

rng f meets rng g

hence
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 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g by A1, JGRAPH_5:69; :: thesis: verum

end;rng f meets rng g by A1, JGRAPH_5:69; :: thesis: verum

suppose
( LE p3,p4,P & LE p4,p1,P & LE p1,p2,P )
; :: thesis: 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 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

rng f meets rng g

hence
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 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g by A1, Th17; :: thesis: verum

end;rng f meets rng g by A1, Th17; :: thesis: verum

suppose
( LE p4,p1,P & LE p1,p2,P & LE p2,p3,P )
; :: thesis: 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 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g

rng f meets rng g

hence
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 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds

rng f meets rng g by A1, Th16; :: thesis: verum

end;rng f meets rng g by A1, Th16; :: thesis: verum