:: General {F}ashoda Meet Theorem for Unit Circle and Square :: by Yatsuka Nakamura :: :: Received February 25, 2003 :: Copyright (c) 2003-2012 Association of Mizar Users begin Lm1: for a, b being real number st b <= 0 & a <= b holds a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) proofend; Lm2: for a, b being real number st a <= 0 & a <= b holds a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2))) proofend; Lm3: for a, b being real number st a >= 0 & a >= b holds a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2))) proofend; theorem Th1: :: JGRAPH_6:1 for a, c, d being real number for 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 ) proofend; theorem Th2: :: JGRAPH_6:2 for a, c, d being real number for p being Point of (TOP-REAL 2) st c < d & p `1 = a & c <= p `2 & p `2 <= d holds p in LSeg (|[a,c]|,|[a,d]|) proofend; theorem Th3: :: JGRAPH_6:3 for a, b, d being real number for p being Point of (TOP-REAL 2) st a <= b & p in LSeg (|[a,d]|,|[b,d]|) holds ( p `2 = d & a <= p `1 & p `1 <= b ) proofend; theorem Th4: :: JGRAPH_6:4 for a, b being real number for B being Subset of I[01] st B = [.a,b.] holds B is closed proofend; theorem Th5: :: JGRAPH_6:5 for X being TopStruct for Y, Z being non empty TopStruct for f being Function of X,Y for g being Function of X,Z holds ( dom f = dom g & dom f = the carrier of X & dom f = [#] X ) proofend; theorem Th6: :: JGRAPH_6:6 for X being non empty TopSpace for B being non empty Subset of X ex f being Function of (X | B),X st ( ( for p being Point of (X | B) holds f . p = p ) & f is continuous ) proofend; theorem Th7: :: JGRAPH_6:7 for X being non empty TopSpace for f1 being Function of X,R^1 for a being real number st f1 is continuous holds ex g being Function of X,R^1 st ( ( for p being Point of X for r1 being real number st f1 . p = r1 holds g . p = r1 - a ) & g is continuous ) proofend; theorem Th8: :: JGRAPH_6:8 for X being non empty TopSpace for f1 being Function of X,R^1 for a being real number st f1 is continuous holds ex g being Function of X,R^1 st ( ( for p being Point of X for r1 being real number st f1 . p = r1 holds g . p = a - r1 ) & g is continuous ) proofend; theorem Th9: :: JGRAPH_6:9 for X being non empty TopSpace for n being Element of NAT for p being Point of (TOP-REAL n) for f being Function of X,R^1 st f is continuous holds ex g being Function of X,(TOP-REAL n) st ( ( for r being Point of X holds g . r = (f . r) * p ) & g is continuous ) proofend; theorem Th10: :: JGRAPH_6:10 Sq_Circ . |[(- 1),0]| = |[(- 1),0]| proofend; theorem :: JGRAPH_6:11 for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } holds Sq_Circ . |[(- 1),0]| = W-min P by Th10, JGRAPH_5:29; theorem Th12: :: JGRAPH_6:12 for X being non empty TopSpace for n being Element of NAT for g1, g2 being Function of X,(TOP-REAL n) st g1 is continuous & g2 is continuous holds ex g being Function of X,(TOP-REAL n) st ( ( for r being Point of X holds g . r = (g1 . r) + (g2 . r) ) & g is continuous ) proofend; theorem Th13: :: JGRAPH_6:13 for X being non empty TopSpace for n being Element of NAT for p1, p2 being Point of (TOP-REAL n) for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds ex g being Function of X,(TOP-REAL n) st ( ( for r being Point of X holds g . r = ((f1 . r) * p1) + ((f2 . r) * p2) ) & g is continuous ) proofend; begin Lm4: |[(- 1),0]| `1 = - 1 by EUCLID:52; Lm5: |[(- 1),0]| `2 = 0 by EUCLID:52; Lm6: |[1,0]| `1 = 1 by EUCLID:52; Lm7: |[1,0]| `2 = 0 by EUCLID:52; Lm8: |[0,(- 1)]| `1 = 0 by EUCLID:52; Lm9: |[0,(- 1)]| `2 = - 1 by EUCLID:52; Lm10: |[0,1]| `1 = 0 by EUCLID:52; Lm11: |[0,1]| `2 = 1 by EUCLID:52; Lm12: now__::_thesis:_(_|.|[(-_1),0]|.|_=_1_&_|.|[1,0]|.|_=_1_&_|.|[0,(-_1)]|.|_=_1_&_|.|[0,1]|.|_=_1_) thus |.|[(- 1),0]|.| = sqrt (((- 1) ^2) + (0 ^2)) by Lm4, Lm5, JGRAPH_3:1 .= 1 by SQUARE_1:18 ; ::_thesis: ( |.|[1,0]|.| = 1 & |.|[0,(- 1)]|.| = 1 & |.|[0,1]|.| = 1 ) thus |.|[1,0]|.| = sqrt ((1 ^2) + (0 ^2)) by Lm6, Lm7, JGRAPH_3:1 .= 1 by SQUARE_1:18 ; ::_thesis: ( |.|[0,(- 1)]|.| = 1 & |.|[0,1]|.| = 1 ) thus |.|[0,(- 1)]|.| = sqrt ((0 ^2) + ((- 1) ^2)) by Lm8, Lm9, JGRAPH_3:1 .= 1 by SQUARE_1:18 ; ::_thesis: |.|[0,1]|.| = 1 thus |.|[0,1]|.| = sqrt ((0 ^2) + (1 ^2)) by Lm10, Lm11, JGRAPH_3:1 .= 1 by SQUARE_1:18 ; ::_thesis: verum end; Lm13: 0 in [.0,1.] by XXREAL_1:1; Lm14: 1 in [.0,1.] by XXREAL_1:1; theorem Th14: :: JGRAPH_6:14 for f, g being Function of I[01],(TOP-REAL 2) for C0, KXP, KXN, KYP, KYN being Subset of (TOP-REAL 2) for 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 where p is Point of (TOP-REAL 2) : |.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 KYP & g . I in KYN & rng f c= C0 & rng g c= C0 holds rng f meets rng g proofend; theorem Th15: :: JGRAPH_6:15 for f, g being Function of I[01],(TOP-REAL 2) for C0, KXP, KXN, KYP, KYN being Subset of (TOP-REAL 2) for 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 where p is Point of (TOP-REAL 2) : |.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 proofend; theorem Th16: :: JGRAPH_6:16 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 = { 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 proofend; theorem Th17: :: JGRAPH_6:17 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 = { 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 proofend; theorem Th18: :: JGRAPH_6:18 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 } & 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 proofend; begin notation let a, b, c, d be real number ; synonym rectangle (a,b,c,d) for [.a,b,c,d.]; end; Lm15: for a, b, c, d being real number st a <= b & c <= d holds rectangle (a,b,c,d) = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = a & c <= p `2 & p `2 <= d ) or ( p `2 = d & a <= p `1 & p `1 <= b ) or ( p `1 = b & c <= p `2 & p `2 <= d ) or ( p `2 = c & a <= p `1 & p `1 <= b ) ) } proofend; theorem Th19: :: JGRAPH_6:19 for a, b, c, d being real number for 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 ) proofend; definition let a, b, c, d be real number ; func inside_of_rectangle (a,b,c,d) -> Subset of (TOP-REAL 2) equals :: JGRAPH_6:def 1 { p where p is Point of (TOP-REAL 2) : ( a < p `1 & p `1 < b & c < p `2 & p `2 < d ) } ; coherence { p where p is Point of (TOP-REAL 2) : ( a < p `1 & p `1 < b & c < p `2 & p `2 < d ) } is Subset of (TOP-REAL 2) proofend; end; :: deftheorem defines inside_of_rectangle JGRAPH_6:def_1_:_ for a, b, c, d being real number holds inside_of_rectangle (a,b,c,d) = { p where p is Point of (TOP-REAL 2) : ( a < p `1 & p `1 < b & c < p `2 & p `2 < d ) } ; definition let a, b, c, d be real number ; func closed_inside_of_rectangle (a,b,c,d) -> Subset of (TOP-REAL 2) equals :: JGRAPH_6:def 2 { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) } ; coherence { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) } is Subset of (TOP-REAL 2) proofend; end; :: deftheorem defines closed_inside_of_rectangle JGRAPH_6:def_2_:_ for a, b, c, d being real number holds closed_inside_of_rectangle (a,b,c,d) = { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) } ; definition let a, b, c, d be real number ; func outside_of_rectangle (a,b,c,d) -> Subset of (TOP-REAL 2) equals :: JGRAPH_6:def 3 { p where p is Point of (TOP-REAL 2) : ( not a <= p `1 or not p `1 <= b or not c <= p `2 or not p `2 <= d ) } ; coherence { p where p is Point of (TOP-REAL 2) : ( not a <= p `1 or not p `1 <= b or not c <= p `2 or not p `2 <= d ) } is Subset of (TOP-REAL 2) proofend; end; :: deftheorem defines outside_of_rectangle JGRAPH_6:def_3_:_ for a, b, c, d being real number holds outside_of_rectangle (a,b,c,d) = { p where p is Point of (TOP-REAL 2) : ( not a <= p `1 or not p `1 <= b or not c <= p `2 or not p `2 <= d ) } ; definition let a, b, c, d be real number ; func closed_outside_of_rectangle (a,b,c,d) -> Subset of (TOP-REAL 2) equals :: JGRAPH_6:def 4 { p where p is Point of (TOP-REAL 2) : ( not a < p `1 or not p `1 < b or not c < p `2 or not p `2 < d ) } ; coherence { p where p is Point of (TOP-REAL 2) : ( not a < p `1 or not p `1 < b or not c < p `2 or not p `2 < d ) } is Subset of (TOP-REAL 2) proofend; end; :: deftheorem defines closed_outside_of_rectangle JGRAPH_6:def_4_:_ for a, b, c, d being real number holds closed_outside_of_rectangle (a,b,c,d) = { p where p is Point of (TOP-REAL 2) : ( not a < p `1 or not p `1 < b or not c < p `2 or not p `2 < d ) } ; theorem Th20: :: JGRAPH_6:20 for a, b, r being real number for Kb, Cb being Subset of (TOP-REAL 2) st r >= 0 & Kb = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } & Cb = { p2 where p2 is Point of (TOP-REAL 2) : |.(p2 - |[a,b]|).| = r } holds (AffineMap (r,a,r,b)) .: Kb = Cb proofend; theorem Th21: :: 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 proofend; theorem Th22: :: JGRAPH_6:22 for P being Subset of (TOP-REAL 2) st P is being_simple_closed_curve holds P is compact ; theorem Th23: :: JGRAPH_6:23 for a, b, r being real number for 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 proofend; definition let a, b, r be real number ; 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 } ; coherence { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } is Subset of (TOP-REAL 2) proofend; end; :: deftheorem defines circle JGRAPH_6:def_5_:_ for a, b, r being real number holds circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } ; registration let a, b, r be real number ; cluster circle (a,b,r) -> compact ; coherence circle (a,b,r) is compact proofend; end; registration let a, b be real number ; let r be real non negative number ; cluster circle (a,b,r) -> non empty ; coherence not circle (a,b,r) is empty proofend; end; definition let a, b, r be real number ; 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]|).| < r } ; coherence { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| < r } is Subset of (TOP-REAL 2) proofend; end; :: deftheorem defines inside_of_circle JGRAPH_6:def_6_:_ for a, b, r being real number holds inside_of_circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| < r } ; definition let a, b, r be real number ; func closed_inside_of_circle (a,b,r) -> Subset of (TOP-REAL 2) equals :: JGRAPH_6:def 7 { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| <= r } ; coherence { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| <= r } is Subset of (TOP-REAL 2) proofend; end; :: deftheorem defines closed_inside_of_circle JGRAPH_6:def_7_:_ for a, b, r being real number holds closed_inside_of_circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| <= r } ; definition let a, b, r be real number ; 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 } ; coherence { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| > r } is Subset of (TOP-REAL 2) proofend; end; :: deftheorem defines outside_of_circle JGRAPH_6:def_8_:_ for a, b, r being real number holds outside_of_circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| > r } ; definition let a, b, r be real number ; 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 } ; coherence { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| >= r } is Subset of (TOP-REAL 2) proofend; end; :: deftheorem defines closed_outside_of_circle JGRAPH_6:def_9_:_ for a, b, r being real number holds closed_outside_of_circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| >= r } ; theorem Th24: :: JGRAPH_6:24 for r being real number holds ( inside_of_circle (0,0,r) = { p where p is Point of (TOP-REAL 2) : |.p.| < r } & ( r > 0 implies circle (0,0,r) = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| = r } ) & outside_of_circle (0,0,r) = { p3 where p3 is Point of (TOP-REAL 2) : |.p3.| > r } & closed_inside_of_circle (0,0,r) = { q where q is Point of (TOP-REAL 2) : |.q.| <= r } & closed_outside_of_circle (0,0,r) = { q2 where q2 is Point of (TOP-REAL 2) : |.q2.| >= r } ) proofend; theorem Th25: :: JGRAPH_6:25 for Kb, Cb being Subset of (TOP-REAL 2) st Kb = { p where p is Point of (TOP-REAL 2) : ( - 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 proofend; theorem Th26: :: JGRAPH_6:26 for Kb, Cb being Subset of (TOP-REAL 2) st Kb = { p where p is Point of (TOP-REAL 2) : ( not - 1 <= p `1 or not p `1 <= 1 or not - 1 <= p `2 or not p `2 <= 1 ) } & Cb = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| > 1 } holds Sq_Circ .: Kb = Cb proofend; theorem Th27: :: JGRAPH_6:27 for Kb, Cb being Subset of (TOP-REAL 2) st Kb = { p where p is Point of (TOP-REAL 2) : ( - 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 proofend; theorem Th28: :: JGRAPH_6:28 for Kb, Cb being Subset of (TOP-REAL 2) st Kb = { p where p is Point of (TOP-REAL 2) : ( not - 1 < p `1 or not p `1 < 1 or not - 1 < p `2 or not p `2 < 1 ) } & Cb = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| >= 1 } holds Sq_Circ .: Kb = Cb proofend; theorem :: JGRAPH_6:29 for P0, P1, P01, P11, K0, K1, K01, K11 being Subset of (TOP-REAL 2) for P being non empty compact Subset of (TOP-REAL 2) for 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 ) proofend; begin theorem Th30: :: JGRAPH_6:30 for a, b, c, d being real number st a <= b & c <= d holds ( LSeg (|[a,c]|,|[a,d]|) = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = a & p1 `2 <= d & p1 `2 >= c ) } & LSeg (|[a,d]|,|[b,d]|) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) } & LSeg (|[a,c]|,|[b,c]|) = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= b & q1 `1 >= a & q1 `2 = c ) } & LSeg (|[b,c]|,|[b,d]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = b & q2 `2 <= d & q2 `2 >= c ) } ) proofend; theorem Th31: :: JGRAPH_6:31 for a, b, c, d being real number st a <= b & c <= d holds (LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,c]|,|[b,c]|)) = {|[a,c]|} proofend; theorem Th32: :: JGRAPH_6:32 for a, b, c, d being real number st a <= b & c <= d holds (LSeg (|[a,c]|,|[b,c]|)) /\ (LSeg (|[b,c]|,|[b,d]|)) = {|[b,c]|} proofend; theorem Th33: :: JGRAPH_6:33 for a, b, c, d being real number st a <= b & c <= d holds (LSeg (|[a,d]|,|[b,d]|)) /\ (LSeg (|[b,c]|,|[b,d]|)) = {|[b,d]|} proofend; theorem Th34: :: JGRAPH_6:34 for a, b, c, d being real number st a <= b & c <= d holds (LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,d]|,|[b,d]|)) = {|[a,d]|} proofend; theorem Th35: :: JGRAPH_6:35 { q where q is Point of (TOP-REAL 2) : ( ( - 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 where p is Point of (TOP-REAL 2) : ( ( 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 ) ) } proofend; theorem Th36: :: JGRAPH_6:36 for a, b, c, d being real number st a <= b & c <= d holds W-bound (rectangle (a,b,c,d)) = a proofend; theorem Th37: :: JGRAPH_6:37 for a, b, c, d being real number st a <= b & c <= d holds N-bound (rectangle (a,b,c,d)) = d proofend; theorem Th38: :: JGRAPH_6:38 for a, b, c, d being real number st a <= b & c <= d holds E-bound (rectangle (a,b,c,d)) = b proofend; theorem Th39: :: JGRAPH_6:39 for a, b, c, d being real number st a <= b & c <= d holds S-bound (rectangle (a,b,c,d)) = c proofend; theorem Th40: :: JGRAPH_6:40 for a, b, c, d being real number st a <= b & c <= d holds NW-corner (rectangle (a,b,c,d)) = |[a,d]| proofend; theorem Th41: :: JGRAPH_6:41 for a, b, c, d being real number st a <= b & c <= d holds NE-corner (rectangle (a,b,c,d)) = |[b,d]| proofend; theorem :: JGRAPH_6:42 for a, b, c, d being real number st a <= b & c <= d holds SW-corner (rectangle (a,b,c,d)) = |[a,c]| proofend; theorem :: JGRAPH_6:43 for a, b, c, d being real number st a <= b & c <= d holds SE-corner (rectangle (a,b,c,d)) = |[b,c]| proofend; theorem Th44: :: JGRAPH_6:44 for a, b, c, d being real number st a <= b & c <= d holds W-most (rectangle (a,b,c,d)) = LSeg (|[a,c]|,|[a,d]|) proofend; theorem Th45: :: JGRAPH_6:45 for a, b, c, d being real number st a <= b & c <= d holds E-most (rectangle (a,b,c,d)) = LSeg (|[b,c]|,|[b,d]|) proofend; theorem Th46: :: JGRAPH_6:46 for a, b, c, d being real number st a <= b & c <= d holds ( W-min (rectangle (a,b,c,d)) = |[a,c]| & E-max (rectangle (a,b,c,d)) = |[b,d]| ) proofend; theorem Th47: :: JGRAPH_6:47 for a, b, c, d being real number st a < b & c < d holds ( (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|)) is_an_arc_of W-min (rectangle (a,b,c,d)), E-max (rectangle (a,b,c,d)) & (LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|)) is_an_arc_of E-max (rectangle (a,b,c,d)), W-min (rectangle (a,b,c,d)) ) proofend; theorem Th48: :: JGRAPH_6:48 for a, b, c, d being real number for f1, f2 being FinSequence of (TOP-REAL 2) for p0, p1, p01, p10 being Point of (TOP-REAL 2) st a < b & c < d & p0 = |[a,c]| & p1 = |[b,d]| & p01 = |[a,d]| & p10 = |[b,c]| & f1 = <*p0,p01,p1*> & 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 ) proofend; theorem Th49: :: JGRAPH_6:49 for P1, P2 being Subset of (TOP-REAL 2) for a, b, c, d being real number for f1, f2 being FinSequence of (TOP-REAL 2) for 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 & not P1 is empty & not P2 is empty & rectangle (a,b,c,d) = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) proofend; theorem Th50: :: JGRAPH_6:50 for a, b, c, d being real number st a < b & c < d holds rectangle (a,b,c,d) is being_simple_closed_curve proofend; theorem Th51: :: JGRAPH_6:51 for a, b, c, d being real number st a < b & c < d holds Upper_Arc (rectangle (a,b,c,d)) = (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|)) proofend; theorem Th52: :: JGRAPH_6:52 for a, b, c, d being real number st a < b & c < d holds Lower_Arc (rectangle (a,b,c,d)) = (LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|)) proofend; theorem Th53: :: JGRAPH_6:53 for a, b, c, d being real number st a < b & c < d holds ex f being Function of I[01],((TOP-REAL 2) | (Upper_Arc (rectangle (a,b,c,d)))) st ( f is being_homeomorphism & f . 0 = W-min (rectangle (a,b,c,d)) & f . 1 = E-max (rectangle (a,b,c,d)) & rng f = Upper_Arc (rectangle (a,b,c,d)) & ( for r being Real st r in [.0,(1 / 2).] holds f . r = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) ) & ( for r being Real st r in [.(1 / 2),1.] holds f . r = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) ) & ( for p being Point of (TOP-REAL 2) st p in LSeg (|[a,c]|,|[a,d]|) holds ( 0 <= (((p `2) - c) / (d - c)) / 2 & (((p `2) - c) / (d - c)) / 2 <= 1 & f . ((((p `2) - c) / (d - c)) / 2) = p ) ) & ( for p being Point of (TOP-REAL 2) st p in LSeg (|[a,d]|,|[b,d]|) holds ( 0 <= ((((p `1) - a) / (b - a)) / 2) + (1 / 2) & ((((p `1) - a) / (b - a)) / 2) + (1 / 2) <= 1 & f . (((((p `1) - a) / (b - a)) / 2) + (1 / 2)) = p ) ) ) proofend; theorem Th54: :: JGRAPH_6:54 for a, b, c, d being real number st a < b & c < d holds ex f being Function of I[01],((TOP-REAL 2) | (Lower_Arc (rectangle (a,b,c,d)))) st ( f is being_homeomorphism & f . 0 = E-max (rectangle (a,b,c,d)) & f . 1 = W-min (rectangle (a,b,c,d)) & rng f = Lower_Arc (rectangle (a,b,c,d)) & ( for r being Real st r in [.0,(1 / 2).] holds f . r = ((1 - (2 * r)) * |[b,d]|) + ((2 * r) * |[b,c]|) ) & ( for r being Real st r in [.(1 / 2),1.] holds f . r = ((1 - ((2 * r) - 1)) * |[b,c]|) + (((2 * r) - 1) * |[a,c]|) ) & ( for p being Point of (TOP-REAL 2) st p in LSeg (|[b,d]|,|[b,c]|) holds ( 0 <= (((p `2) - d) / (c - d)) / 2 & (((p `2) - d) / (c - d)) / 2 <= 1 & f . ((((p `2) - d) / (c - d)) / 2) = p ) ) & ( for p being Point of (TOP-REAL 2) st p in LSeg (|[b,c]|,|[a,c]|) holds ( 0 <= ((((p `1) - b) / (a - b)) / 2) + (1 / 2) & ((((p `1) - b) / (a - b)) / 2) + (1 / 2) <= 1 & f . (((((p `1) - b) / (a - b)) / 2) + (1 / 2)) = p ) ) ) proofend; theorem Th55: :: JGRAPH_6:55 for a, b, c, d being real number for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[a,c]|,|[a,d]|) & p2 in LSeg (|[a,c]|,|[a,d]|) holds ( LE p1,p2, rectangle (a,b,c,d) iff p1 `2 <= p2 `2 ) proofend; theorem Th56: :: JGRAPH_6:56 for a, b, c, d being real number for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[a,d]|,|[b,d]|) & p2 in LSeg (|[a,d]|,|[b,d]|) holds ( LE p1,p2, rectangle (a,b,c,d) iff p1 `1 <= p2 `1 ) proofend; theorem Th57: :: JGRAPH_6:57 for a, b, c, d being real number for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[b,c]|,|[b,d]|) & p2 in LSeg (|[b,c]|,|[b,d]|) holds ( LE p1,p2, rectangle (a,b,c,d) iff p1 `2 >= p2 `2 ) proofend; theorem Th58: :: JGRAPH_6:58 for a, b, c, d being real number for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[a,c]|,|[b,c]|) & p2 in LSeg (|[a,c]|,|[b,c]|) holds ( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) iff ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) ) proofend; theorem Th59: :: JGRAPH_6:59 for a, b, c, d being real number for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[a,c]|,|[a,d]|) holds ( LE p1,p2, rectangle (a,b,c,d) iff ( ( p2 in LSeg (|[a,c]|,|[a,d]|) & p1 `2 <= p2 `2 ) or p2 in LSeg (|[a,d]|,|[b,d]|) or p2 in LSeg (|[b,d]|,|[b,c]|) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) ) proofend; theorem Th60: :: JGRAPH_6:60 for a, b, c, d being real number for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[a,d]|,|[b,d]|) holds ( LE p1,p2, rectangle (a,b,c,d) iff ( ( p2 in LSeg (|[a,d]|,|[b,d]|) & p1 `1 <= p2 `1 ) or p2 in LSeg (|[b,d]|,|[b,c]|) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) ) proofend; theorem Th61: :: JGRAPH_6:61 for a, b, c, d being real number for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[b,d]|,|[b,c]|) holds ( LE p1,p2, rectangle (a,b,c,d) iff ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) ) proofend; theorem Th62: :: JGRAPH_6:62 for a, b, c, d being real number for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[b,c]|,|[a,c]|) & p1 <> W-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)) ) ) proofend; theorem Th63: :: JGRAPH_6:63 for x being set for a, b, c, d being real number st x in rectangle (a,b,c,d) & a < b & c < d & not x in LSeg (|[a,c]|,|[a,d]|) & not x in LSeg (|[a,d]|,|[b,d]|) & not x in LSeg (|[b,d]|,|[b,c]|) holds x in LSeg (|[b,c]|,|[a,c]|) proofend; begin theorem Th64: :: JGRAPH_6:64 for p1, p2 being Point of (TOP-REAL 2) st LE p1,p2, rectangle ((- 1),1,(- 1),1) & p1 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & not ( p2 in LSeg (|[(- 1),(- 1)]|,|[(- 1),1]|) & p2 `2 >= p1 `2 ) & not p2 in LSeg (|[(- 1),1]|,|[1,1]|) & not p2 in LSeg (|[1,1]|,|[1,(- 1)]|) holds ( p2 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p2 <> |[(- 1),(- 1)]| ) proofend; theorem Th65: :: JGRAPH_6:65 for p1, p2 being Point of (TOP-REAL 2) for P being non empty compact Subset of (TOP-REAL 2) for 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 proofend; theorem Th66: :: JGRAPH_6:66 for p1, p2, p3 being Point of (TOP-REAL 2) for P being non empty compact Subset of (TOP-REAL 2) for 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 proofend; theorem Th67: :: JGRAPH_6:67 for p being Point of (TOP-REAL 2) for 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 ) proofend; theorem Th68: :: JGRAPH_6:68 for p being Point of (TOP-REAL 2) for P being non empty compact Subset of (TOP-REAL 2) for f being Function of (TOP-REAL 2),(TOP-REAL 2) st f = Sq_Circ holds ( (f . p) `1 >= 0 iff p `1 >= 0 ) proofend; theorem Th69: :: JGRAPH_6:69 for p being Point of (TOP-REAL 2) for P being non empty compact Subset of (TOP-REAL 2) for f being Function of (TOP-REAL 2),(TOP-REAL 2) st f = Sq_Circ holds ( (f . p) `2 >= 0 iff p `2 >= 0 ) proofend; theorem Th70: :: JGRAPH_6:70 for p, q being Point of (TOP-REAL 2) for 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 proofend; theorem Th71: :: JGRAPH_6:71 for p, q being Point of (TOP-REAL 2) for 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 proofend; theorem Th72: :: JGRAPH_6:72 for p1, p2, p3, p4 being Point of (TOP-REAL 2) for P being non empty compact Subset of (TOP-REAL 2) for f being Function of (TOP-REAL 2),(TOP-REAL 2) st P = circle (0,0,1) & f = Sq_Circ & LE p1,p2, rectangle ((- 1),1,(- 1),1) & LE p2,p3, rectangle ((- 1),1,(- 1),1) & LE p3,p4, rectangle ((- 1),1,(- 1),1) holds f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P proofend; theorem Th73: :: JGRAPH_6:73 for p1, p2 being Point of (TOP-REAL 2) for 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 proofend; theorem :: JGRAPH_6:74 for p1, p2, p3 being Point of (TOP-REAL 2) for 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 & not ( LE p1,p2,P & LE p2,p3,P ) & not ( LE p1,p3,P & LE p3,p2,P ) & not ( LE p2,p1,P & LE p1,p3,P ) & not ( LE p2,p3,P & LE p3,p1,P ) & not ( LE p3,p1,P & LE p1,p2,P ) holds ( LE p3,p2,P & LE p2,p1,P ) by Th73; theorem :: JGRAPH_6:75 for p1, p2, p3 being Point of (TOP-REAL 2) for 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 & not LE p1,p2,P & not ( LE p2,p1,P & LE p1,p3,P ) holds LE p3,p1,P by Th73; theorem :: JGRAPH_6:76 for p1, p2, p3, p4 being Point of (TOP-REAL 2) for 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 & not LE p1,p2,P & not ( LE p2,p1,P & LE p1,p3,P ) & not ( LE p3,p1,P & LE p1,p4,P ) holds LE p4,p1,P by Th73; theorem Th77: :: JGRAPH_6:77 for p1, p2, p3, p4 being Point of (TOP-REAL 2) for P being non empty compact Subset of (TOP-REAL 2) for 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) proofend; theorem Th78: :: JGRAPH_6:78 for p1, p2, p3, p4 being Point of (TOP-REAL 2) for P being non empty compact Subset of (TOP-REAL 2) for 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 ) proofend; 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) 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 & 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 proofend;