let p1, p2, p3, p4 be Point of (); :: thesis: for P being non empty compact Subset of ()
for C0 being Subset of () st P = { p where p is Point of () : |.p.| = 1 } & p1,p2,p3,p4 are_in_this_order_on P holds
for f, g being Function of I[01],() st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of () : |.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 (); :: thesis: for C0 being Subset of () st P = { p where p is Point of () : |.p.| = 1 } & p1,p2,p3,p4 are_in_this_order_on P holds
for f, g being Function of I[01],() st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of () : |.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 (); :: thesis: ( P = { p where p is Point of () : |.p.| = 1 } & p1,p2,p3,p4 are_in_this_order_on P implies for f, g being Function of I[01],() st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of () : |.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 () : |.p.| = 1 } and
A2: p1,p2,p3,p4 are_in_this_order_on P ; :: thesis: for f, g being Function of I[01],() st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of () : |.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 ;
suppose ( LE p1,p2,P & LE p2,p3,P & LE p3,p4,P ) ; :: thesis: for f, g being Function of I[01],() st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of () : |.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

hence for f, g being Function of I[01],() st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of () : |.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 ; :: thesis: verum
end;
suppose ( LE p2,p3,P & LE p3,p4,P & LE p4,p1,P ) ; :: thesis: for f, g being Function of I[01],() st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of () : |.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

hence for f, g being Function of I[01],() st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of () : |.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 ; :: thesis: verum
end;
suppose ( LE p3,p4,P & LE p4,p1,P & LE p1,p2,P ) ; :: thesis: for f, g being Function of I[01],() st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of () : |.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

hence for f, g being Function of I[01],() st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of () : |.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 ; :: thesis: verum
end;
suppose ( LE p4,p1,P & LE p1,p2,P & LE p2,p3,P ) ; :: thesis: for f, g being Function of I[01],() st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of () : |.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

hence for f, g being Function of I[01],() st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of () : |.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 ; :: thesis: verum
end;
end;