:: General {F}ashoda Meet Theorem for Unit Circle and Square :: by Yatsuka Nakamura :: :: Received February 25, 2003 :: Copyright (c) 2003-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XXREAL_0, CARD_1, RELAT_1, SQUARE_1, ARYTM_3, ARYTM_1, PRE_TOPC, EUCLID, RLTOPSP1, MCART_1, REAL_1, SUBSET_1, BORSUK_1, XXREAL_1, RCOMP_1, TOPMETR, STRUCT_0, XBOOLE_0, FUNCT_1, ORDINAL2, TARSKI, TOPS_1, METRIC_1, SUPINF_2, COMPLEX1, JGRAPH_3, PSCOMP_1, PCOMPS_1, JORDAN3, TOPS_2, JORDAN17, JGRAPH_2, TOPREAL2, TOPREAL1, SEQ_4, FINSEQ_1, PARTFUN1, NAT_1, JORDAN6, JORDAN5C, FUNCT_4, RELAT_2, JGRAPH_6; notations XBOOLE_0, ORDINAL1, XCMPLX_0, COMPLEX1, TARSKI, RELAT_1, TOPS_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, SUBSET_1, FINSEQ_1, FINSEQ_4, SEQ_4, STRUCT_0, TOPMETR, COMPTS_1, METRIC_1, SQUARE_1, RCOMP_1, PRE_TOPC, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID, FUNCT_4, JGRAPH_3, JORDAN5C, JORDAN6, TOPREAL2, CONNSP_1, TOPS_1, JORDAN17, JGRAPH_2, NUMBERS, XREAL_0, TOPREAL1, PSCOMP_1, REAL_1, NAT_1, SPPOL_2, XXREAL_0; constructors FUNCT_4, REAL_1, SQUARE_1, COMPLEX1, RCOMP_1, FINSEQ_4, TOPS_1, CONNSP_1, TOPS_2, COMPTS_1, TOPMETR, TOPREAL1, SPPOL_2, PSCOMP_1, JORDAN5C, JORDAN6, JGRAPH_2, JGRAPH_3, JORDAN17, PCOMPS_1, SEQ_4, FUNCSDOM, CONVEX1, BINOP_2; registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, MEMBERED, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, EUCLID, TOPMETR, TOPREAL1, TOPREAL2, SPPOL_2, PSCOMP_1, JGRAPH_2, JGRAPH_3, XXREAL_2, COMPTS_1, RLTOPSP1, MEASURE6, FUNCT_1, VALUED_0, ORDINAL1; requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM; begin theorem :: JGRAPH_6:1 for a,c,d being Real,p being Point of TOP-REAL 2 st c <=d & p in LSeg(|[a,c]|,|[a,d]|) holds p`1=a & c <=p`2 & p`2<=d; theorem :: JGRAPH_6:2 for a,c,d being Real,p being Point of TOP-REAL 2 st c =-q1`1} & KXN={q2 where q2 is Point of TOP-REAL 2: |.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} & KYP={q3 where q3 is Point of TOP-REAL 2: |.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} & KYN={q4 where q4 is Point of TOP-REAL 2: |.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} & f.O in KXP & f.I in KXN & g.O in KYP & g.I in KYN & rng f c= C0 & rng g c= C0 holds rng f meets rng g; theorem :: JGRAPH_6:15 for f,g being Function of I[01],TOP-REAL 2, C0,KXP,KXN,KYP,KYN being Subset of TOP-REAL 2, O,I being Point of I[01] st O=0 & I=1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0={p: |.p.|<=1}& KXP={q1 where q1 is Point of TOP-REAL 2: |.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} & KXN={q2 where q2 is Point of TOP-REAL 2: |.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} & KYP={q3 where q3 is Point of TOP-REAL 2: |.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} & KYN={q4 where q4 is Point of TOP-REAL 2: |.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} & f.O in KXP & f.I in KXN & g.O in KYN & g.I in KYP & rng f c= C0 & rng g c= C0 holds rng f meets rng g; theorem :: JGRAPH_6:16 for p1,p2,p3,p4 being Point of TOP-REAL 2, P being compact non empty Subset of TOP-REAL 2,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 one-to-one & g is continuous one-to-one & C0={p8 where p8 is Point of TOP-REAL 2: |.p8.|<=1}& f.0=p3 & f.1=p1 & g.0=p2 & g.1=p4 & rng f c= C0 & rng g c= C0 holds rng f meets rng g; theorem :: JGRAPH_6:17 for p1,p2,p3,p4 being Point of TOP-REAL 2, P being compact non empty Subset of TOP-REAL 2,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 one-to-one & g is continuous one-to-one & C0={p8 where p8 is Point of TOP-REAL 2: |.p8.|<=1}& f.0=p3 & f.1=p1 & g.0=p4 & g.1=p2 & rng f c= C0 & rng g c= C0 holds rng f meets rng g; theorem :: JGRAPH_6:18 for p1,p2,p3,p4 being Point of TOP-REAL 2, P being compact non empty Subset of TOP-REAL 2, 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 one-to-one & g is continuous 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; begin :: General Rectangles and Circles notation let a,b,c,d be Real; synonym rectangle(a,b,c,d) for [.a,b,c,d.]; end; theorem :: JGRAPH_6:19 for a,b,c,d being Real, p being Point of TOP-REAL 2 st a<=b & c <=d & p in rectangle(a,b,c,d) holds a<=p`1 & p`1<=b & c <=p`2 & p`2<=d; definition let a,b,c,d be Real; func inside_of_rectangle(a,b,c,d) -> Subset of TOP-REAL 2 equals :: JGRAPH_6:def 1 {p: a Subset of TOP-REAL 2 equals :: JGRAPH_6:def 2 {p: a <=p`1 & p`1<= b & c <=p`2 & p`2<= d}; end; definition let a,b,c,d be Real; func outside_of_rectangle(a,b,c,d) -> Subset of TOP-REAL 2 equals :: JGRAPH_6:def 3 {p: not(a <=p`1 & p`1<= b & c <=p`2 & p`2<= d)}; end; definition let a,b,c,d be Real; func closed_outside_of_rectangle(a,b,c,d) -> Subset of TOP-REAL 2 equals :: JGRAPH_6:def 4 {p: not(a =0 & Kb={q: |.q.|=1}& Cb={p2 where p2 is Point of TOP-REAL 2: |.(p2- |[a,b]|).|=r} holds AffineMap(r,a,r,b).:Kb=Cb; theorem :: JGRAPH_6:21 for P,Q being Subset of TOP-REAL 2 st (ex f being Function of (TOP-REAL 2)|P,(TOP-REAL 2)|Q st f is being_homeomorphism) & P is being_simple_closed_curve holds Q is being_simple_closed_curve; theorem :: JGRAPH_6:22 for P being Subset of TOP-REAL 2 st P is being_simple_closed_curve holds P is compact; theorem :: JGRAPH_6:23 for a,b,r be Real, Cb being Subset of TOP-REAL 2 st r>0 & Cb={p where p is Point of TOP-REAL 2: |.(p- |[a,b]|).|=r} holds Cb is being_simple_closed_curve; definition let a,b,r be Real; func circle(a,b,r) -> Subset of TOP-REAL 2 equals :: JGRAPH_6:def 5 {p where p is Point of TOP-REAL 2: |.p- |[a,b]| .|=r}; end; registration let a,b,r be Real; cluster circle(a,b,r) -> compact; end; registration let a,b be Real; let r be non negative Real; cluster circle(a,b,r) -> non empty; end; definition let a,b,r be Real; func inside_of_circle(a,b,r) -> Subset of TOP-REAL 2 equals :: JGRAPH_6:def 6 {p where p is Point of TOP-REAL 2: |.p- |[a,b]| .| Subset of TOP-REAL 2 equals :: JGRAPH_6:def 7 {p where p is Point of TOP-REAL 2: |.p- |[a,b]| .|<=r}; end; definition let a,b,r be Real; func outside_of_circle(a,b,r) -> Subset of TOP-REAL 2 equals :: JGRAPH_6:def 8 {p where p is Point of TOP-REAL 2: |.p- |[a,b]| .|>r}; end; definition let a,b,r be Real; func closed_outside_of_circle(a,b,r) -> Subset of TOP-REAL 2 equals :: JGRAPH_6:def 9 {p where p is Point of TOP-REAL 2: |.p- |[a,b]| .|>=r}; end; theorem :: JGRAPH_6:24 for r being Real holds inside_of_circle(0,0,r)={p : |.p.|0 implies circle(0,0,r)={p2 : |.p2.|=r}) & outside_of_circle(0,0,r)={p3 : |.p3.|>r} & closed_inside_of_circle(0,0,r)={q : |.q.|<=r} & closed_outside_of_circle(0,0,r)={q2 : |.q2.|>=r}; theorem :: JGRAPH_6:25 for Kb,Cb being Subset of TOP-REAL 2 st Kb={p: -1 1} holds Sq_Circ.:Kb=Cb; theorem :: JGRAPH_6:27 for Kb,Cb being Subset of TOP-REAL 2 st Kb={p: -1 <=p`1 & p`1<= 1 & -1 <=p`2 & p`2<= 1}& Cb={p2 where p2 is Point of TOP-REAL 2: |.p2.|<=1} holds Sq_Circ.:Kb=Cb; theorem :: JGRAPH_6:28 for Kb,Cb being Subset of TOP-REAL 2 st Kb={p: not(-1 =1} holds Sq_Circ.:Kb=Cb; theorem :: JGRAPH_6:29 for P0,P1,P01,P11,K0,K1,K01,K11 being Subset of TOP-REAL 2, P being non empty compact Subset of TOP-REAL 2, f being Function of TOP-REAL 2,TOP-REAL 2 st P= circle(0,0,1) & P0= inside_of_circle(0,0,1) & P1= outside_of_circle(0,0,1) & P01= closed_inside_of_circle(0,0,1) & P11= closed_outside_of_circle(0,0,1) & K0=inside_of_rectangle(-1,1,-1,1) & K1=outside_of_rectangle(-1,1,-1,1) & K01=closed_inside_of_rectangle(-1,1,-1,1) & K11=closed_outside_of_rectangle(-1,1,-1,1) & f=Sq_Circ holds f.:rectangle(-1,1,-1,1)=P & f".:P=rectangle(-1,1,-1,1) & f.:K0=P0 & f".:P0=K0 & f.:K1=P1 & f".:P1=K1 & f.:K01=P01 & f.:K11=P11 & f".:P01=K01 & f".:P11=K11; begin :: Order of Points on Rectangle theorem :: JGRAPH_6:30 for a,b,c,d being Real st a <= b & c <= d holds LSeg(|[ a,c ]|, |[ a,d ]|) = { p1 : p1`1 = a & p1`2 <= d & p1`2 >= c} & LSeg(|[ a,d ]|, |[ b,d ]|) = { p2 : p2`1 <= b & p2`1 >= a & p2`2 = d} & LSeg(|[ a,c ]|, |[ b,c ]|) = { q1 : q1`1 <= b & q1`1 >= a & q1`2 = c} & LSeg(|[ b,c ]|, |[ b,d ]|) = { q2 : q2`1 = b & q2`2 <= d & q2`2 >= c}; theorem :: JGRAPH_6:31 for a,b,c,d being Real st a <= b & c <= d holds LSeg(|[a,c]|,|[a,d]|) /\ LSeg(|[a,c]|,|[b,c]|) = {|[a,c]|}; theorem :: JGRAPH_6:32 for a,b,c,d being Real st a <= b & c <= d holds LSeg(|[a,c]|,|[b,c]|) /\ LSeg(|[b,c]|,|[b,d]|) = {|[b,c]|}; theorem :: JGRAPH_6:33 for a,b,c,d being Real st a <= b & c <= d holds LSeg(|[a,d]|,|[b,d]|) /\ LSeg(|[b,c]|,|[b,d]|) = {|[b,d]|}; theorem :: JGRAPH_6:34 for a,b,c,d being Real st a <= b & c <= d holds LSeg(|[a,c]|,|[a,d]|) /\ LSeg(|[a,d]|,|[b,d]|) = {|[a,d]|}; theorem :: JGRAPH_6:35 {q: -1=q`1 & -1<=q`2 & q`2<=1 or q`1=1 & -1<=q`2 & q`2<=1 or -1=q`2 & -1<=q`1 & q`1<=1 or 1=q`2 & -1<=q`1 & q`1<=1} = {p: p`1=-1 & -1 <=p`2 & p`2<=1 or p`2=1 & -1<=p`1 & p`1<=1 or p`1=1 & -1 <=p`2 & p`2<=1 or p`2=-1 & -1<=p`1 & p`1<=1}; theorem :: JGRAPH_6:36 for a,b,c,d being Real st a<=b & c <=d holds W-bound rectangle(a,b,c,d) = a; theorem :: JGRAPH_6:37 for a,b,c,d being Real st a<=b & c <=d holds N-bound rectangle(a,b,c,d) = d; theorem :: JGRAPH_6:38 for a,b,c,d being Real st a<=b & c <=d holds E-bound rectangle(a,b,c,d) = b; theorem :: JGRAPH_6:39 for a,b,c,d being Real st a<=b & c <=d holds S-bound rectangle(a,b,c,d) = c; theorem :: JGRAPH_6:40 for a,b,c,d being Real st a<=b & c <=d holds NW-corner rectangle(a,b,c,d) = |[a,d]|; theorem :: JGRAPH_6:41 for a,b,c,d being Real st a<=b & c <=d holds NE-corner rectangle(a,b,c,d) = |[b,d]|; theorem :: JGRAPH_6:42 for a,b,c,d being Real st a<=b & c <=d holds SW-corner rectangle(a,b,c,d) = |[a,c]|; theorem :: JGRAPH_6:43 for a,b,c,d being Real st a<=b & c <=d holds SE-corner rectangle(a,b,c,d) = |[b,c]|; theorem :: JGRAPH_6:44 for a,b,c,d being Real st a<=b & c <=d holds W-most rectangle(a,b,c,d) = LSeg(|[a,c]|,|[a,d]|); theorem :: JGRAPH_6:45 for a,b,c,d being Real st a<=b & c <=d holds E-most rectangle(a,b,c,d) = LSeg(|[b,c]|,|[b,d]|); theorem :: JGRAPH_6:46 for a,b,c,d being Real st a<=b & c <=d holds W-min rectangle(a,b,c,d)=|[a,c]| & E-max rectangle(a,b,c,d)=|[b,d]|; theorem :: JGRAPH_6:47 for a,b,c,d being Real st a & f2=<*p0,p10,p1*> holds f1 is being_S-Seq & L~f1 = LSeg(p0,p01) \/ LSeg(p01,p1) & f2 is being_S-Seq & L~f2 = LSeg(p0,p10) \/ LSeg(p10,p1) & rectangle(a,b,c,d) = L~f1 \/ L~f2 & L~f1 /\ L~f2 = {p0,p1} & f1/.1 = p0 & f1/.len f1=p1 & f2/.1 = p0 & f2/.len f2 = p1; theorem :: JGRAPH_6:49 for P1,P2 being Subset of TOP-REAL 2, a,b,c,d being Real, f1,f2 being FinSequence of TOP-REAL 2,p1,p2 being Point of TOP-REAL 2 st a < b & c < d & p1=|[a,c]| & p2=|[b,d]| & f1=<*|[a,c]|,|[a,d]|,|[b,d]|*> & f2=<*|[a,c]|,|[b,c]|,|[b,d]|*> & P1=L~f1 & P2=L~f2 holds P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 is non empty & P2 is non empty & rectangle(a,b,c,d) = P1 \/ P2 & P1 /\ P2 = {p1,p2}; theorem :: JGRAPH_6:50 for a,b,c,d being Real st a < b & c < d holds rectangle(a,b,c,d) is being_simple_closed_curve; theorem :: JGRAPH_6:51 for a,b,c,d being Real st a=p2`2; theorem :: JGRAPH_6:58 for a,b,c,d being Real,p1,p2 being Point of TOP-REAL 2 st aW-min rectangle(a,b,c,d) iff p1`1>=p2`1 & p2<>W-min rectangle(a,b,c,d); theorem :: JGRAPH_6:59 for a,b,c,d being Real,p1,p2 being Point of TOP-REAL 2 st aW-min rectangle(a,b,c,d); theorem :: JGRAPH_6:60 for a,b,c,d being Real,p1,p2 being Point of TOP-REAL 2 st aW-min rectangle(a,b,c,d); theorem :: JGRAPH_6:61 for a,b,c,d being Real,p1,p2 being Point of TOP-REAL 2 st a=p2`2 or p2 in LSeg(|[b,c]|,|[a,c]|) & p2<>W-min rectangle(a,b,c,d); theorem :: JGRAPH_6:62 for a,b,c,d being Real,p1,p2 being Point of TOP-REAL 2 st aW-min rectangle(a,b,c,d) holds LE p1,p2,rectangle(a,b,c,d) iff p2 in LSeg(|[b,c]|,|[a,c]|) & p1`1>=p2`1 & p2<>W-min rectangle(a,b,c,d); theorem :: JGRAPH_6:63 for x being set,a,b,c,d being Real st x in rectangle(a,b,c,d) & a=p1`2 or p2 in LSeg(|[-1,1]|,|[1,1]|) or p2 in LSeg(|[1,1]|,|[1,-1]|) or p2 in LSeg(|[1,-1]|,|[-1,-1]|)& p2<>|[-1,-1]|; theorem :: JGRAPH_6:65 for p1,p2 being Point of TOP-REAL 2, P being non empty compact Subset of TOP-REAL 2, f being Function of TOP-REAL 2,TOP-REAL 2 st P= circle(0,0,1) & f=Sq_Circ & p1 in LSeg(|[-1,-1]|,|[-1,1]|)& p1`2>=0 & LE p1,p2,rectangle(-1,1,-1,1) holds LE f.p1,f.p2,P; theorem :: JGRAPH_6:66 for p1,p2,p3 being Point of TOP-REAL 2, P being non empty compact Subset of TOP-REAL 2, f being Function of TOP-REAL 2,TOP-REAL 2 st P= circle(0,0,1) & f=Sq_Circ & p1 in LSeg(|[-1,-1]|,|[-1,1]|)& p1`2>=0 & LE p1,p2,rectangle(-1,1,-1,1) & LE p2,p3,rectangle(-1,1,-1,1) holds LE f.p2,f.p3,P; theorem :: JGRAPH_6:67 for p being Point of TOP-REAL 2, f being Function of TOP-REAL 2,TOP-REAL 2 st f=Sq_Circ & p`1=-1 & p`2<0 holds (f.p)`1<0 & (f.p)`2<0; theorem :: JGRAPH_6:68 for p being Point of TOP-REAL 2, P being non empty compact Subset of TOP-REAL 2, f being Function of TOP-REAL 2,TOP-REAL 2 st f=Sq_Circ holds (f.p)`1>=0 iff p`1>=0; theorem :: JGRAPH_6:69 for p being Point of TOP-REAL 2, P being non empty compact Subset of TOP-REAL 2, f being Function of TOP-REAL 2,TOP-REAL 2 st f=Sq_Circ holds (f.p)`2>=0 iff p`2>=0; theorem :: JGRAPH_6:70 for p,q being Point of TOP-REAL 2, f being Function of TOP-REAL 2,TOP-REAL 2 st f=Sq_Circ & p in LSeg(|[-1,-1]|,|[-1,1]|) & q in LSeg(|[1,-1]|,|[-1,-1]|) holds (f.p)`1<=(f.q)`1; theorem :: JGRAPH_6:71 for p,q being Point of TOP-REAL 2, f being Function of TOP-REAL 2,TOP-REAL 2 st f=Sq_Circ & p in LSeg(|[-1,-1]|,|[-1,1]|) & q in LSeg(|[-1,-1]|,|[-1,1]|) & p`2>=q`2 & p`2<0 holds (f.p)`2>=(f.q)`2; theorem :: JGRAPH_6:72 for p1,p2,p3,p4 being Point of TOP-REAL 2, P being non empty compact Subset of TOP-REAL 2, f being Function of TOP-REAL 2,TOP-REAL 2 st P= circle(0,0,1) & f=Sq_Circ holds LE p1,p2,rectangle(-1,1,-1,1) & LE p2,p3,rectangle(-1,1,-1,1) & LE p3,p4,rectangle(-1,1,-1,1) implies f.p1,f.p2,f.p3,f.p4 are_in_this_order_on P; theorem :: JGRAPH_6:73 for p1,p2 being Point of TOP-REAL 2, P being non empty compact Subset of TOP-REAL 2 st P is being_simple_closed_curve & p1 in P & p2 in P & not LE p1,p2,P holds LE p2,p1,P; theorem :: JGRAPH_6:74 for p1,p2,p3 being Point of TOP-REAL 2, P being non empty compact Subset of TOP-REAL 2 st P is being_simple_closed_curve & p1 in P & p2 in P & p3 in P holds LE p1,p2,P & LE p2,p3,P or LE p1,p3,P & LE p3,p2,P or LE p2,p1,P & LE p1,p3,P or LE p2,p3,P & LE p3,p1,P or LE p3,p1,P & LE p1,p2,P or LE p3,p2,P & LE p2,p1,P; theorem :: JGRAPH_6:75 for p1,p2,p3 being Point of TOP-REAL 2, P being non empty compact Subset of TOP-REAL 2 st P is being_simple_closed_curve & p1 in P & p2 in P & p3 in P & LE p2,p3,P holds LE p1,p2,P or LE p2,p1,P & LE p1,p3,P or LE p3,p1,P; theorem :: JGRAPH_6:76 for p1,p2,p3,p4 being Point of TOP-REAL 2, P being non empty compact Subset of TOP-REAL 2 st P is being_simple_closed_curve & p1 in P & p2 in P & p3 in P & p4 in P & LE p2,p3,P & LE p3,p4,P holds LE p1,p2,P or LE p2,p1,P & LE p1,p3,P or LE p3,p1,P & LE p1,p4,P or LE p4,p1,P; theorem :: JGRAPH_6:77 for p1,p2,p3,p4 being Point of TOP-REAL 2, P being non empty compact Subset of TOP-REAL 2, f being Function of TOP-REAL 2,TOP-REAL 2 st P= circle(0,0,1) & f=Sq_Circ & LE f.p1,f.p2,P & LE f.p2,f.p3,P & LE f.p3,f.p4,P holds p1,p2,p3,p4 are_in_this_order_on rectangle(-1,1,-1,1); theorem :: JGRAPH_6:78 for p1,p2,p3,p4 being Point of TOP-REAL 2, P being non empty compact Subset of TOP-REAL 2, f being Function of TOP-REAL 2,TOP-REAL 2 st P= circle(0,0,1) & f=Sq_Circ holds p1,p2,p3,p4 are_in_this_order_on rectangle(-1,1,-1,1) iff f.p1,f.p2,f.p3,f.p4 are_in_this_order_on P; theorem :: JGRAPH_6:79 for p1,p2,p3,p4 being Point of TOP-REAL 2 st p1,p2,p3,p4 are_in_this_order_on rectangle(-1,1,-1,1) for f,g being Function of I[01],TOP-REAL 2 st f is continuous one-to-one & g is continuous one-to-one & f.0=p1 & f.1=p3 & g.0=p2 & g.1=p4 & rng f c= closed_inside_of_rectangle(-1,1,-1,1) & rng g c= closed_inside_of_rectangle(-1,1,-1,1) holds rng f meets rng g;