gtarski2.miz



    begin

    theorem :: GTARSKI2:1

    

     Th1: for r,s,t,u be Real st s <> 0 & t <> 0 & (r ^2 ) = (((s ^2 ) + (t ^2 )) - (((2 * s) * t) * u)) holds u = ((((r ^2 ) - (s ^2 )) - (t ^2 )) / ( - ((2 * s) * t)))

    proof

      let r,s,t,u be Real;

      assume that

       A1: s <> 0 and

       A2: t <> 0 and

       A3: (r ^2 ) = (((s ^2 ) + (t ^2 )) - (((2 * s) * t) * u));

      (((r ^2 ) - (s ^2 )) - (t ^2 )) = (u * ( - ((2 * s) * t))) by A3;

      hence thesis by A1, A2, XCMPLX_1: 89;

    end;

    theorem :: GTARSKI2:2

    

     THJE: for n be Nat holds for u,v be Element of ( TOP-REAL n) holds (u + ( 0 * v)) = u

    proof

      let n be Nat;

      let u,v be Element of ( TOP-REAL n);

      ( 0. ( TOP-REAL n)) = ( 0 * v) by RLVECT_1: 10;

      hence thesis;

    end;

    theorem :: GTARSKI2:3

    

     THJC: for n be Nat holds for r,s be Real, u,v,w be Element of ( TOP-REAL n) st ((r * u) - (r * v)) = ((s * w) - (s * u)) holds ((r + s) * u) = ((r * v) + (s * w))

    proof

      let n be Nat;

      let r,s be Real, u,v,w be Element of ( TOP-REAL n);

      assume ((r * u) - (r * v)) = ((s * w) - (s * u));

      

      then (((r * u) - (r * v)) + (s * u)) = ((s * w) + (( - (s * u)) + (s * u))) by RVSUM_1: 15

      .= ((s * w) + (((( - 1) * s) * u) + (s * u))) by RVSUM_1: 49

      .= ((s * w) + ((( - s) + s) * u)) by RVSUM_1: 50

      .= (s * w) by THJE;

      

      then ((s * w) + (r * v)) = ((((r * u) + ((( - 1) * r) * v)) + (s * u)) + (r * v)) by RVSUM_1: 49

      .= ((((r * u) + (s * u)) + ((( - 1) * r) * v)) + (r * v)) by RVSUM_1: 15

      .= (((r * u) + (s * u)) + (((( - 1) * r) * v) + (r * v))) by RVSUM_1: 15

      .= (((r * u) + (s * u)) + ((( - r) + r) * v)) by RVSUM_1: 50

      .= ((r * u) + (s * u)) by THJE;

      hence thesis by RVSUM_1: 50;

    end;

    theorem :: GTARSKI2:4

    

     THJD: for r,s be Real st 0 < r & 0 < s holds 0 <= (r / (r + s)) <= 1

    proof

      let r,s be Real;

      assume that

       A1: 0 < r and

       A2: 0 < s;

      thus 0 <= (r / (r + s)) by A1, A2;

      ( 0 + r) <= (s + r) by A2, XREAL_1: 6;

      then (r / (r + s)) <= ((r + s) / (r + s)) by A1, XREAL_1: 72;

      hence (r / (r + s)) <= 1 by A1, A2, XCMPLX_1: 60;

    end;

    theorem :: GTARSKI2:5

    

     Th2: for a be Real holds ( cos ((3 * PI ) - a)) = ( - ( cos a))

    proof

      let a be Real;

      ( cos ((3 * PI ) - a)) = ( cos ((2 * PI ) + ( PI - a)))

      .= ( cos ( PI - a)) by SIN_COS: 79

      .= ( - ( cos a)) by EUCLID10: 2;

      hence thesis;

    end;

    theorem :: GTARSKI2:6

    

     THSD2: for n be Nat holds for a,b,c be Element of ( TOP-REAL n) st (a - c) = (b - c) holds a = b

    proof

      let n be Nat;

      let a,b,c be Element of ( TOP-REAL n);

      assume (a - c) = (b - c);

      then (a + (( - c) + c)) = ((b - c) + c) by RLVECT_1:def 3;

      then (a + ( 0. ( TOP-REAL n))) = ((b - c) + c) by RLVECT_1: 5;

      then a = (b + (( - c) + c)) by RLVECT_1:def 3;

      then a = (b + ( 0. ( TOP-REAL n))) by RLVECT_1: 5;

      hence thesis;

    end;

    theorem :: GTARSKI2:7

    

     ThWW: for n be Nat holds for a,b,c be Element of ( TOP-REAL n) holds ((c - a) - (b - a)) = (c - b)

    proof

      let n be Nat;

      let a,b,c be Element of ( TOP-REAL n);

      

      thus ((c - a) - (b - a)) = (((c - a) - b) + a) by RLVECT_1: 29

      .= (((c - a) + a) + ( - b)) by RLVECT_1:def 3

      .= ((c + (( - a) + a)) + ( - b)) by RLVECT_1:def 3

      .= ((c + ( 0. ( TOP-REAL n))) + ( - b)) by RLVECT_1: 5

      .= (c - b);

    end;

    theorem :: GTARSKI2:8

    

     THYQ: for a,b,c,d be Real holds ( dist ( |[a, b]|, |[c, d]|)) = ( sqrt (((a - c) ^2 ) + ((b - d) ^2 )))

    proof

      let a,b,c,d be Real;

      

       A1: ( |[a, b]| `1 ) = a & ( |[a, b]| `2 ) = b & ( |[c, d]| `1 ) = c & ( |[c, d]| `2 ) = d by EUCLID: 52;

      reconsider P = |[a, b]|, Q = |[c, d]| as Point of ( Euclid 2) by EUCLID: 22;

      ( dist ( |[a, b]|, |[c, d]|)) = ( dist (P,Q)) by TOPREAL6:def 1

      .= (( Pitag_dist 2) . (P,Q)) by METRIC_1:def 1

      .= ( sqrt (((a - c) ^2 ) + ((b - d) ^2 ))) by A1, TOPREAL3: 7;

      hence thesis;

    end;

    theorem :: GTARSKI2:9

    

     THY1: ( dist ( |[ 0 , 0 ]|, |[1, 0 ]|)) = 1

    proof

      ( dist ( |[ 0 , 0 ]|, |[1, 0 ]|)) = ( sqrt ((( 0 - 1) ^2 ) + (( 0 - 0 ) ^2 ))) by THYQ

      .= ( sqrt ((( - 1) * ( - 1)) + ( 0 ^2 ))) by SQUARE_1:def 1

      .= ( sqrt (1 + ( 0 * 0 ))) by SQUARE_1:def 1

      .= 1 by SQUARE_1: 18;

      hence thesis;

    end;

    theorem :: GTARSKI2:10

    

     THY2: ( dist ( |[ 0 , 0 ]|, |[ 0 , 1]|)) = 1

    proof

      ( dist ( |[ 0 , 0 ]|, |[ 0 , 1]|)) = ( sqrt ((( 0 - 0 ) ^2 ) + (( 0 - 1) ^2 ))) by THYQ

      .= ( sqrt (( 0 * 0 ) + (( - 1) ^2 ))) by SQUARE_1:def 1

      .= ( sqrt ( 0 + (( - 1) * ( - 1)))) by SQUARE_1:def 1

      .= 1 by SQUARE_1: 18;

      hence thesis;

    end;

    theorem :: GTARSKI2:11

    

     THY3: ( dist ( |[1, 0 ]|, |[ 0 , 1]|)) = ( sqrt 2)

    proof

      ( dist ( |[1, 0 ]|, |[ 0 , 1]|)) = ( sqrt (((1 - 0 ) ^2 ) + (( 0 - 1) ^2 ))) by THYQ

      .= ( sqrt ((1 ^2 ) + (1 ^2 ))) by SQUARE_1: 3

      .= ( sqrt ((1 * 1) + (1 ^2 ))) by SQUARE_1:def 1

      .= ( sqrt ((1 * 1) + (1 * 1))) by SQUARE_1:def 1

      .= ( sqrt 2);

      hence thesis;

    end;

    definition

      let n be Nat;

      :: GTARSKI2:def1

      func TarskiEuclidSpace n -> MetrTarskiStr equals the naturally_generated TarskiExtension of ( Euclid n);

      coherence ;

    end

    definition

      :: GTARSKI2:def2

      func TarskiEuclid2Space -> MetrTarskiStr equals ( TarskiEuclidSpace 2);

      coherence ;

    end

    begin

    registration

      let n be Nat;

      cluster ( TarskiEuclidSpace n) -> non empty;

      coherence ;

    end

    registration

      cluster TarskiEuclid2Space -> Reflexive symmetric discerning;

      coherence ;

    end

    registration

      let n be Nat;

      cluster ( TarskiEuclidSpace n) -> Reflexive symmetric discerning;

      coherence ;

    end

    definition

      let n be Nat;

      let P be POINT of ( TarskiEuclidSpace n);

      :: GTARSKI2:def3

      func Tn2TR P -> Element of ( TOP-REAL n) equals P;

      coherence

      proof

         the MetrStruct of ( TarskiEuclidSpace n) = the MetrStruct of ( Euclid n) by GTARSKI1:def 13;

        hence thesis by EUCLID: 22;

      end;

    end

    definition

      let P be POINT of TarskiEuclid2Space ;

      :: GTARSKI2:def4

      func Tn2TR P -> Element of ( TOP-REAL 2) equals P;

      coherence

      proof

         the MetrStruct of TarskiEuclid2Space = the MetrStruct of ( Euclid 2) by GTARSKI1:def 13;

        hence thesis by EUCLID: 22;

      end;

    end

    definition

      let P be POINT of TarskiEuclid2Space ;

      :: GTARSKI2:def5

      func Tn2E P -> Point of ( Euclid 2) equals P;

      coherence

      proof

         the MetrStruct of TarskiEuclid2Space = the MetrStruct of ( Euclid 2) by GTARSKI1:def 13;

        hence thesis;

      end;

    end

    definition

      let P be POINT of TarskiEuclid2Space ;

      :: GTARSKI2:def6

      func Tn2R P -> Element of ( REAL 2) equals P;

      coherence

      proof

         the MetrStruct of TarskiEuclid2Space = the MetrStruct of ( Euclid 2) by GTARSKI1:def 13;

        hence thesis;

      end;

    end

    theorem :: GTARSKI2:12

    

     ThEquiv: for n be Nat holds for p,q be POINT of ( TarskiEuclidSpace n), p1,q1 be Element of ( TOP-REAL n) st p = p1 & q = q1 holds ( dist (p,q)) = (( Pitag_dist n) . (p1,q1)) & ( dist (p,q)) = |.(p1 - q1).|

    proof

      let n be Nat;

      let p,q be POINT of ( TarskiEuclidSpace n), p1,q1 be Element of ( TOP-REAL n);

      assume

       A0: p = p1 & q = q1;

      

       A1: the MetrStruct of ( TarskiEuclidSpace n) = the MetrStruct of ( Euclid n) by GTARSKI1:def 13;

      then (( Pitag_dist n) . (p1,q1)) = |.(p1 - q1).| by A0, EUCLID:def 6;

      hence thesis by A1, METRIC_1:def 1, A0;

    end;

    theorem :: GTARSKI2:13

    

     ThLawOfCosines: for a,b,c be POINT of TarskiEuclid2Space holds (( dist (c,a)) ^2 ) = (((( dist (a,b)) ^2 ) + (( dist (b,c)) ^2 )) - (((2 * ( dist (a,b))) * ( dist (b,c))) * ( cos ( angle (( Tn2TR a),( Tn2TR b),( Tn2TR c))))))

    proof

      let a,b,c be POINT of TarskiEuclid2Space ;

      set ta = |.(( Tn2TR a) - ( Tn2TR b)).|, tb = |.(( Tn2TR c) - ( Tn2TR b)).|, tc = |.(( Tn2TR c) - ( Tn2TR a)).|;

       |.(( Tn2TR a) - ( Tn2TR b)).| = ( dist (a,b)) & |.(( Tn2TR c) - ( Tn2TR b)).| = ( dist (c,b)) & |.(( Tn2TR c) - ( Tn2TR a)).| = ( dist (c,a)) by ThEquiv;

      hence thesis by EUCLID_6: 7;

    end;

    theorem :: GTARSKI2:14

    for a,b,c,e,f,g be POINT of TarskiEuclid2Space st (( Tn2TR a),( Tn2TR b),( Tn2TR c)) is_a_triangle & ( angle (( Tn2TR a),( Tn2TR b),( Tn2TR c))) < PI & ( angle (( Tn2TR e),( Tn2TR c),( Tn2TR a))) = (( angle (( Tn2TR b),( Tn2TR c),( Tn2TR a))) / 3) & ( angle (( Tn2TR c),( Tn2TR a),( Tn2TR e))) = (( angle (( Tn2TR c),( Tn2TR a),( Tn2TR b))) / 3) & ( angle (( Tn2TR a),( Tn2TR b),( Tn2TR f))) = (( angle (( Tn2TR a),( Tn2TR b),( Tn2TR c))) / 3) & ( angle (( Tn2TR f),( Tn2TR a),( Tn2TR b))) = (( angle (( Tn2TR c),( Tn2TR a),( Tn2TR b))) / 3) & ( angle (( Tn2TR b),( Tn2TR c),( Tn2TR g))) = (( angle (( Tn2TR b),( Tn2TR c),( Tn2TR a))) / 3) & ( angle (( Tn2TR g),( Tn2TR b),( Tn2TR c))) = (( angle (( Tn2TR a),( Tn2TR b),( Tn2TR c))) / 3) holds ( dist (f,e)) = ( dist (g,f)) & ( dist (f,e)) = ( dist (e,g)) & ( dist (g,f)) = ( dist (e,g))

    proof

      let a,b,c,e,f,g be POINT of TarskiEuclid2Space ;

      assume

       A1: (( Tn2TR a),( Tn2TR b),( Tn2TR c)) is_a_triangle & ( angle (( Tn2TR a),( Tn2TR b),( Tn2TR c))) < PI & ( angle (( Tn2TR e),( Tn2TR c),( Tn2TR a))) = (( angle (( Tn2TR b),( Tn2TR c),( Tn2TR a))) / 3) & ( angle (( Tn2TR c),( Tn2TR a),( Tn2TR e))) = (( angle (( Tn2TR c),( Tn2TR a),( Tn2TR b))) / 3) & ( angle (( Tn2TR a),( Tn2TR b),( Tn2TR f))) = (( angle (( Tn2TR a),( Tn2TR b),( Tn2TR c))) / 3) & ( angle (( Tn2TR f),( Tn2TR a),( Tn2TR b))) = (( angle (( Tn2TR c),( Tn2TR a),( Tn2TR b))) / 3) & ( angle (( Tn2TR b),( Tn2TR c),( Tn2TR g))) = (( angle (( Tn2TR b),( Tn2TR c),( Tn2TR a))) / 3) & ( angle (( Tn2TR g),( Tn2TR b),( Tn2TR c))) = (( angle (( Tn2TR a),( Tn2TR b),( Tn2TR c))) / 3);

       |.(( Tn2TR f) - ( Tn2TR e)).| = ( dist (f,e)) & |.(( Tn2TR g) - ( Tn2TR f)).| = ( dist (g,f)) & |.(( Tn2TR e) - ( Tn2TR g)).| = ( dist (e,g)) by ThEquiv;

      hence thesis by A1, EUCLID11: 23;

    end;

    theorem :: GTARSKI2:15

    

     ThConv: for n be Nat holds for p,q be Element of ( TarskiEuclidSpace n), p1,q1 be Element of ( Euclid n) st p = p1 & q = q1 holds ( dist (p,q)) = ( dist (p1,q1))

    proof

      let n be Nat;

      let p,q be Element of ( TarskiEuclidSpace n);

      let p1,q1 be Element of ( Euclid n);

      assume

       A1: p = p1 & q = q1;

      

      thus ( dist (p,q)) = (the distance of the MetrStruct of ( TarskiEuclidSpace n) . (p,q)) by METRIC_1:def 1

      .= (the distance of the MetrStruct of ( Euclid n) . (p,q)) by GTARSKI1:def 13

      .= ( dist (p1,q1)) by METRIC_1:def 1, A1;

    end;

    theorem :: GTARSKI2:16

    

     ThConv2: for p,q be POINT of TarskiEuclid2Space holds ( dist (p,q)) = ( sqrt ((((( Tn2TR p) `1 ) - (( Tn2TR q) `1 )) ^2 ) + (((( Tn2TR p) `2 ) - (( Tn2TR q) `2 )) ^2 )))

    proof

      let p,q be POINT of TarskiEuclid2Space ;

      

       A1: the MetrStruct of TarskiEuclid2Space = the MetrStruct of ( Euclid 2) by GTARSKI1:def 13;

      (( Pitag_dist 2) . (( Tn2E p),( Tn2E q))) = ( sqrt ((((( Tn2TR p) `1 ) - (( Tn2TR q) `1 )) ^2 ) + (((( Tn2TR p) `2 ) - (( Tn2TR q) `2 )) ^2 ))) by TOPREAL3: 7;

      hence thesis by A1, METRIC_1:def 1;

    end;

    theorem :: GTARSKI2:17

    

     ThConv3: for A,B be POINT of TarskiEuclid2Space holds ( dist (A,B)) = |.(( Tn2TR A) - ( Tn2TR B)).| & ( dist (A,B)) = |.(( Tn2R A) - ( Tn2R B)).|

    proof

      let A,B be POINT of TarskiEuclid2Space ;

       the MetrStruct of TarskiEuclid2Space = the MetrStruct of ( Euclid 2) by GTARSKI1:def 13;

      

      then ( dist (A,B)) = (( Pitag_dist 2) . (( Tn2TR A),( Tn2TR B))) by METRIC_1:def 1

      .= |.(( Tn2R A) - ( Tn2R B)).| by EUCLID:def 6;

      hence thesis;

    end;

    theorem :: GTARSKI2:18

    

     ThConv4: for a,b,c,d be POINT of TarskiEuclid2Space holds |.(( Tn2TR a) - ( Tn2TR b)).| = |.(( Tn2TR c) - ( Tn2TR d)).| iff (a,b) equiv (c,d)

    proof

      let a,b,c,d be POINT of TarskiEuclid2Space ;

      

       A1: ( dist (a,b)) = |.(( Tn2TR a) - ( Tn2TR b)).| & ( dist (c,d)) = |.(( Tn2TR c) - ( Tn2TR d)).| by ThConv3;

      thus |.(( Tn2TR a) - ( Tn2TR b)).| = |.(( Tn2TR c) - ( Tn2TR d)).| implies (a,b) equiv (c,d) by A1, GTARSKI1:def 15;

      assume (a,b) equiv (c,d);

      hence thesis by A1, GTARSKI1:def 15;

    end;

    theorem :: GTARSKI2:19

    

     ThConv5: for p,q,r be POINT of TarskiEuclid2Space holds p is_Between (q,r) iff ( Tn2TR p) in ( LSeg (( Tn2TR q),( Tn2TR r)))

    proof

      let p,q,r be POINT of TarskiEuclid2Space ;

      

       A1: ( dist (( Tn2TR q),( Tn2TR p))) = ( dist (( Tn2E q),( Tn2E p))) & ( dist (( Tn2TR p),( Tn2TR r))) = ( dist (( Tn2E p),( Tn2E r))) & ( dist (( Tn2TR q),( Tn2TR r))) = ( dist (( Tn2E q),( Tn2E r))) by TOPREAL6:def 1;

      ( dist (q,p)) = ( dist (( Tn2E q),( Tn2E p))) & ( dist (p,r)) = ( dist (( Tn2E p),( Tn2E r))) & ( dist (q,r)) = ( dist (( Tn2E q),( Tn2E r))) by ThConv;

      hence thesis by A1, EUCLID12: 12;

    end;

    reserve n for Nat;

    theorem :: GTARSKI2:20

    

     ThConv6: for p,q,r be POINT of TarskiEuclid2Space holds between (p,q,r) iff ( Tn2TR q) in ( LSeg (( Tn2TR p),( Tn2TR r)))

    proof

      let p,q,r be POINT of TarskiEuclid2Space ;

      hereby

        assume between (p,q,r);

        then q is_Between (p,r) by GTARSKI1:def 15;

        hence ( Tn2TR q) in ( LSeg (( Tn2TR p),( Tn2TR r))) by ThConv5;

      end;

      assume ( Tn2TR q) in ( LSeg (( Tn2TR p),( Tn2TR r)));

      then q is_Between (p,r) by ThConv5;

      hence thesis by GTARSKI1:def 15;

    end;

    theorem :: GTARSKI2:21

    

     ThConv7: for a,b be Point of TarskiEuclid2Space holds between (a,a,b) & between (a,b,b)

    proof

      let a,b be Point of TarskiEuclid2Space ;

      ( Tn2TR a) in ( LSeg (( Tn2TR a),( Tn2TR b))) by RLTOPSP1: 68;

      hence between (a,a,b) by ThConv6;

      ( Tn2TR b) in ( LSeg (( Tn2TR a),( Tn2TR b))) by RLTOPSP1: 68;

      hence between (a,b,b) by ThConv6;

    end;

    theorem :: GTARSKI2:22

    

     ThConv7bis: for a,b,c be Point of TarskiEuclid2Space st between (a,b,c) holds between (c,b,a)

    proof

      let a,b,c be Point of TarskiEuclid2Space ;

      assume between (a,b,c);

      then ( Tn2TR b) in ( LSeg (( Tn2TR a),( Tn2TR c))) by ThConv6;

      hence thesis by ThConv6;

    end;

    theorem :: GTARSKI2:23

    

     ThConv7ter: for a,b be Point of TarskiEuclid2Space st between (a,b,a) holds a = b

    proof

      let a,b be Point of TarskiEuclid2Space ;

      assume between (a,b,a);

      then ( Tn2TR b) in ( LSeg (( Tn2TR a),( Tn2TR a))) by ThConv6;

      then ( Tn2TR b) in {( Tn2TR a)} by RLTOPSP1: 70;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: GTARSKI2:24

    

     ThEgal: for a,b be POINT of TarskiEuclid2Space holds a = b iff ( dist (a,b)) = 0

    proof

      let a,b be POINT of TarskiEuclid2Space ;

      hereby

        assume a = b;

        then ( Tn2R a) = ( Tn2R b);

        then 0 = |.(( Tn2TR a) - ( Tn2TR b)).|;

        hence ( dist (a,b)) = 0 by ThEquiv;

      end;

      assume ( dist (a,b)) = 0 ;

      hence thesis by METRIC_1: 2;

    end;

    theorem :: GTARSKI2:25

    

     ThNull: for a,b,c,d be POINT of TarskiEuclid2Space st (( dist (a,b)) + ( dist (c,d))) = 0 holds a = b & c = d

    proof

      let a,b,c,d be POINT of TarskiEuclid2Space ;

      assume

       A1: (( dist (a,b)) + ( dist (c,d))) = 0 ;

       0 <= ( dist (a,b)) & 0 <= ( dist (c,d)) by METRIC_1: 5;

      then ( dist (a,b)) = 0 & ( dist (c,d)) = 0 by A1;

      hence thesis by ThEgal;

    end;

    theorem :: GTARSKI2:26

    for a,b,c,a1,b1,c1 be POINT of TarskiEuclid2Space holds (a,b,c) cong (a1,b1,c1) iff (( dist (a,b)) = ( dist (a1,b1)) & ( dist (a,c)) = ( dist (a1,c1)) & ( dist (b,c)) = ( dist (b1,c1))) by GTARSKI1:def 15;

    theorem :: GTARSKI2:27

    

     ThConv8: for a,b,c be POINT of TarskiEuclid2Space holds between (a,b,c) iff ( dist (a,c)) = (( dist (a,b)) + ( dist (b,c)))

    proof

      let a,b,c be POINT of TarskiEuclid2Space ;

      hereby

        assume between (a,b,c);

        then b is_Between (a,c) by GTARSKI1:def 15;

        hence ( dist (a,c)) = (( dist (a,b)) + ( dist (b,c)));

      end;

      assume ( dist (a,c)) = (( dist (a,b)) + ( dist (b,c)));

      then b is_Between (a,c);

      hence thesis by GTARSKI1:def 15;

    end;

    theorem :: GTARSKI2:28

    

     ThConv9: for a,b,c,d be POINT of TarskiEuclid2Space holds (( dist (a,b)) ^2 ) = (( dist (c,d)) ^2 ) iff (a,b) equiv (c,d)

    proof

      let a,b,c,d be POINT of TarskiEuclid2Space ;

      hereby

        assume

         A1: (( dist (a,b)) ^2 ) = (( dist (c,d)) ^2 );

        ( sqrt (( dist (a,b)) ^2 )) = ( dist (a,b)) & ( sqrt (( dist (c,d)) ^2 )) = ( dist (c,d)) by METRIC_1: 5, SQUARE_1: 22;

        hence (a,b) equiv (c,d) by A1, GTARSKI1:def 15;

      end;

      assume (a,b) equiv (c,d);

      hence thesis by GTARSKI1:def 15;

    end;

    theorem :: GTARSKI2:29

    for a be Point of TarskiEuclid2Space holds between (a,a,a) by ThConv7;

    

     ThCongruenceSymmetry: TarskiEuclid2Space is satisfying_CongruenceSymmetry

    proof

      for a,b be POINT of TarskiEuclid2Space holds (a,b) equiv (b,a)

      proof

        let a,b be POINT of TarskiEuclid2Space ;

        ( dist (a,b)) = ( dist (b,a));

        hence thesis by GTARSKI1:def 15;

      end;

      hence thesis;

    end;

    

     ThCongruenceEquivalenceRelation: TarskiEuclid2Space is satisfying_CongruenceEquivalenceRelation

    proof

      let a,b,p,q,r,s be POINT of TarskiEuclid2Space ;

      assume (a,b) equiv (p,q) & (a,b) equiv (r,s);

      then ( dist (a,b)) = ( dist (p,q)) & ( dist (a,b)) = ( dist (r,s)) by GTARSKI1:def 15;

      hence thesis by GTARSKI1:def 15;

    end;

    

     ThCongruenceIdentity: TarskiEuclid2Space is satisfying_CongruenceIdentity

    proof

      let a,b,c be POINT of TarskiEuclid2Space ;

      assume (a,b) equiv (c,c);

      then ( dist (a,b)) = ( dist (c,c)) by GTARSKI1:def 15;

      hence thesis by METRIC_1: 2, METRIC_1: 1;

    end;

    

     ThSegmentConstruction: TarskiEuclid2Space is satisfying_SegmentConstruction

    proof

      

       A1: the MetrStruct of TarskiEuclid2Space = the MetrStruct of ( Euclid 2) by GTARSKI1:def 13;

      let a,q,b,c be POINT of TarskiEuclid2Space ;

      per cases ;

        suppose

         A1bis: a = q;

        now

          set alpha = |.(( Tn2TR b) - ( Tn2TR c)).|;

          reconsider P = |[alpha, 0 ]| as Element of ( TOP-REAL 2);

          reconsider x = |[((( Tn2TR a) `1 ) + alpha), (( Tn2TR a) `2 )]| as POINT of TarskiEuclid2Space by A1, EUCLID: 67;

          

           A2: (( Tn2TR x) `1 ) = ((( Tn2TR a) `1 ) + alpha) & (( Tn2TR x) `2 ) = (( Tn2TR a) `2 ) by EUCLID: 52;

          

           A3: |.(( Tn2TR a) - ( Tn2TR x)).| = ( dist (a,x)) by ThEquiv

          .= ( sqrt ((((( Tn2TR a) `1 ) - ((( Tn2TR a) `1 ) + alpha)) ^2 ) + (((( Tn2TR a) `2 ) - (( Tn2TR a) `2 )) ^2 ))) by A2, ThConv2

          .= ( sqrt ((( 0 - alpha) ^2 ) + ( 0 * 0 ))) by SQUARE_1:def 1

          .= ( sqrt (alpha ^2 )) by SQUARE_1: 3

          .= alpha by SQUARE_1: 22;

          take x;

          thus between (q,a,x) by A1bis, ThConv7;

          thus (a,x) equiv (b,c) by A3, ThConv4;

        end;

        hence thesis;

      end;

        suppose

         A4: a <> q;

        

         A5: b = c implies thesis

        proof

          assume

           A6: b = c;

          set x = a;

          thus ex x be POINT of TarskiEuclid2Space st between (q,a,x) & (a,x) equiv (b,c)

          proof

            take x;

            

             A7: ( Tn2R a) = ( Tn2R x);

            ( Tn2R b) = ( Tn2R c) by A6;

            then |.(( Tn2TR b) - ( Tn2TR c)).| = 0 ;

            then |.(( Tn2TR a) - ( Tn2TR x)).| = |.(( Tn2TR b) - ( Tn2TR c)).| by A7;

            hence thesis by ThConv7, ThConv4;

          end;

        end;

        b <> c implies thesis

        proof

          assume b <> c;

          then ( Tn2R b) <> ( Tn2R c);

          then

          reconsider alpha = |.(( Tn2TR b) - ( Tn2TR c)).| as positive Real by EUCLID: 17;

          ( Tn2R a) <> ( Tn2R q) by A4;

          then

          reconsider mu = |.(( Tn2TR a) - ( Tn2TR q)).| as positive Real by EUCLID: 17;

          reconsider nu = (alpha / mu) as positive Real;

          reconsider y = |[((( Tn2TR a) `1 ) + (nu * ((( Tn2TR a) `1 ) - (( Tn2TR q) `1 )))), ((( Tn2TR a) `2 ) + (nu * ((( Tn2TR a) `2 ) - (( Tn2TR q) `2 ))))]| as POINT of TarskiEuclid2Space by A1, EUCLID: 67;

          reconsider x = (( Tn2TR a) + (nu * (( Tn2TR a) - ( Tn2TR q)))) as POINT of TarskiEuclid2Space by A1, EUCLID: 67;

          ex x be POINT of TarskiEuclid2Space st between (q,a,x) & (a,x) equiv (b,c)

          proof

            take x;

            reconsider t1 = ( - (nu * (( Tn2TR a) - ( Tn2TR q)))), t2 = ( Tn2TR a) as Element of (2 -tuples_on REAL ) by EUCLID: 22;

            (( Tn2TR a) - ( Tn2TR x)) = (( Tn2TR a) + (( - ( Tn2TR a)) + ( - (nu * (( Tn2TR a) - ( Tn2TR q)))))) by RVSUM_1: 26

            .= ((t1 + t2) - t2) by RVSUM_1: 15

            .= ( - (nu * (( Tn2TR a) - ( Tn2TR q)))) by RVSUM_1: 42;

            

            then

             A8: |.(( Tn2TR a) - ( Tn2TR x)).| = |.(nu * (( Tn2TR a) - ( Tn2TR q))).| by EUCLID: 10

            .= ( |.nu.| * |.(( Tn2TR a) - ( Tn2TR q)).|) by EUCLID: 11

            .= ((alpha / mu) * mu) by COMPLEX1: 43

            .= alpha by XCMPLX_1: 87;

            reconsider aq = (( Tn2TR a) - ( Tn2TR q)), qa = (( Tn2TR q) - ( Tn2TR a)) as Element of (2 -tuples_on REAL ) by EUCLID: 22;

            

             A9: (( Tn2TR q) - ( Tn2TR x)) = (( Tn2TR q) + (( - ( Tn2TR a)) + ( - (nu * (( Tn2TR a) - ( Tn2TR q)))))) by RVSUM_1: 26

            .= (( - (nu * (( Tn2TR a) - ( Tn2TR q)))) + (( - ( - ( Tn2TR q))) + ( - ( Tn2TR a)))) by RVSUM_1: 15

            .= (( - (nu * (( Tn2TR a) - ( Tn2TR q)))) - (( - ( Tn2TR q)) + ( Tn2TR a))) by RVSUM_1: 26

            .= (((( - 1) * nu) * aq) + (( - 1) * aq)) by RVSUM_1: 49

            .= ((( - 1) - nu) * (( Tn2TR a) - ( Tn2TR q))) by RVSUM_1: 50;

             |.(( Tn2TR q) - ( Tn2TR x)).| = ( |.( - (1 + nu)).| * |.(( Tn2TR a) - ( Tn2TR q)).|) by A9, EUCLID: 11

            .= ( |.(1 + nu).| * |.(( Tn2TR a) - ( Tn2TR q)).|) by COMPLEX1: 52

            .= ((1 + nu) * |.(( Tn2TR a) - ( Tn2TR q)).|) by COMPLEX1: 43

            .= (mu + ((alpha / mu) * mu))

            .= (mu + alpha) by XCMPLX_1: 87;

            

            then |.(( Tn2TR q) - ( Tn2TR x)).| = ( |.(( Tn2R q) - ( Tn2R a)).| + |.(( Tn2TR a) - ( Tn2TR x)).|) by A8, EUCLID: 18

            .= ( |.(( Tn2TR q) - ( Tn2TR a)).| + |.(( Tn2TR a) - ( Tn2TR x)).|);

            then ( Tn2TR a) in ( LSeg (( Tn2TR q),( Tn2TR x))) by EUCLID12: 11;

            hence thesis by ThConv6, A8, ThConv4;

          end;

          hence thesis;

        end;

        hence thesis by A5;

      end;

    end;

    

     ThSAS: TarskiEuclid2Space is satisfying_SAS

    proof

      set TP = TarskiEuclid2Space ;

      let a,b,c,x,a1,b1,c1,x1 be POINT of TP;

      assume that

       A1: a <> b and

       A2: (a,b,c) cong (a1,b1,c1) and

       A3: between (a,b,x) and

       A4: between (a1,b1,x1) and

       A5: (b,x) equiv (b1,x1);

      

       A6: (( dist (a,b)) = ( dist (a1,b1)) & ( dist (a,c)) = ( dist (a1,c1)) & ( dist (b,c)) = ( dist (b1,c1))) by A2, GTARSKI1:def 15;

      

       A7: ( dist (a,x)) = (( dist (a,b)) + ( dist (b,x))) by A3, ThConv8;

      

       A8: ( dist (a1,x1)) = (( dist (a1,b1)) + ( dist (b1,x1))) by A4, ThConv8;

      

       A9: ( dist (b,x)) = ( dist (b1,x1)) by A5, GTARSKI1:def 15;

      

       A10: (( dist (c1,x1)) ^2 ) = (((( dist (x1,b1)) ^2 ) + (( dist (c1,b1)) ^2 )) - (((2 * ( dist (x1,b1))) * ( dist (c1,b1))) * ( cos ( angle (( Tn2TR x1),( Tn2TR b1),( Tn2TR c1)))))) by ThLawOfCosines;

      (( dist (c,x)) ^2 ) = (( dist (c1,x1)) ^2 )

      proof

        per cases ;

          suppose x = b;

          then

           A11: 0 = ( dist (x,b)) by ThEgal;

          then

           A12: ( dist (x1,b1)) = 0 by A5, GTARSKI1:def 15;

          

           A12bis: (( dist (c,x)) ^2 ) = ((( 0 ^2 ) + (( dist (c,b)) ^2 )) - (((2 * 0 ) * ( dist (c,b))) * ( cos ( angle (( Tn2TR x),( Tn2TR b),( Tn2TR c)))))) by A11, ThLawOfCosines

          .= (( 0 * 0 ) + (( dist (c,b)) ^2 )) by SQUARE_1:def 1;

          (( dist (c1,x1)) ^2 ) = ((( 0 ^2 ) + (( dist (c1,b1)) ^2 )) - (((2 * 0 ) * ( dist (c1,b1))) * ( cos ( angle (( Tn2TR x1),( Tn2TR b1),( Tn2TR c1)))))) by ThLawOfCosines, A12

          .= (( 0 * 0 ) + (( dist (c1,b1)) ^2 )) by SQUARE_1:def 1;

          hence thesis by A12bis, A2, GTARSKI1:def 15;

        end;

          suppose

           A13: c = b;

          then 0 = ( dist (c,b)) by ThEgal;

          then ( dist (c1,b1)) = 0 by A2, GTARSKI1:def 15;

          then (( dist (c1,x1)) ^2 ) = (( 0 * 0 ) + (( dist (x1,b1)) ^2 )) by A10, SQUARE_1:def 1;

          hence thesis by A13, A5, GTARSKI1:def 15;

        end;

          suppose

           A14: x <> b & c <> b;

          

           A15: a <> x

          proof

            assume a = x;

            then (( dist (a,b)) + ( dist (b,x))) = 0 by A7, ThEgal;

            hence contradiction by A1, ThNull;

          end;

          ( dist (a,b)) <> 0 & ( dist (a,x)) <> 0 & ( dist (b,x)) <> 0 by A1, A14, A15, ThEgal;

          then

           A16: ( Tn2TR a1) <> ( Tn2TR b1) & ( Tn2TR a1) <> ( Tn2TR x1) & ( Tn2TR b1) <> ( Tn2TR x1) by ThEgal, A6, A7, A8, A9;

          ( Tn2TR b) in ( LSeg (( Tn2TR a),( Tn2TR x))) by A3, ThConv6;

          then (( angle (( Tn2TR a),( Tn2TR b),( Tn2TR c))) + ( angle (( Tn2TR c),( Tn2TR b),( Tn2TR x)))) = PI or (( angle (( Tn2TR a),( Tn2TR b),( Tn2TR c))) + ( angle (( Tn2TR c),( Tn2TR b),( Tn2TR x)))) = (3 * PI ) by A1, A14, EUCLID_6: 13;

          then ( cos ( angle (( Tn2TR a),( Tn2TR b),( Tn2TR c)))) = ( cos ( PI - ( angle (( Tn2TR c),( Tn2TR b),( Tn2TR x))))) or ( cos ( angle (( Tn2TR a),( Tn2TR b),( Tn2TR c)))) = ( cos ((3 * PI ) - ( angle (( Tn2TR c),( Tn2TR b),( Tn2TR x)))));

          then

           A17: ( cos ( angle (( Tn2TR a),( Tn2TR b),( Tn2TR c)))) = ( - ( cos ( angle (( Tn2TR c),( Tn2TR b),( Tn2TR x))))) by Th2, EUCLID10: 2;

          ( Tn2TR b1) in ( LSeg (( Tn2TR a1),( Tn2TR x1))) by A4, ThConv6;

          then (( angle (( Tn2TR a1),( Tn2TR b1),( Tn2TR c1))) + ( angle (( Tn2TR c1),( Tn2TR b1),( Tn2TR x1)))) = PI or (( angle (( Tn2TR a1),( Tn2TR b1),( Tn2TR c1))) + ( angle (( Tn2TR c1),( Tn2TR b1),( Tn2TR x1)))) = (3 * PI ) by A16, EUCLID_6: 13;

          then ( cos ( angle (( Tn2TR a1),( Tn2TR b1),( Tn2TR c1)))) = ( cos ( PI - ( angle (( Tn2TR c1),( Tn2TR b1),( Tn2TR x1))))) or ( cos ( angle (( Tn2TR a1),( Tn2TR b1),( Tn2TR c1)))) = ( cos ((3 * PI ) - ( angle (( Tn2TR c1),( Tn2TR b1),( Tn2TR x1)))));

          then

           A18: ( cos ( angle (( Tn2TR a1),( Tn2TR b1),( Tn2TR c1)))) = ( - ( cos ( angle (( Tn2TR c1),( Tn2TR b1),( Tn2TR x1))))) by Th2, EUCLID10: 2;

          

           A19: ( dist (a,b)) <> 0 & ( dist (c,b)) <> 0 by A1, A14, ThEgal;

          

           A20: (( dist (c,a)) ^2 ) = (((( dist (a,b)) ^2 ) + (( dist (c,b)) ^2 )) - (((2 * ( dist (a,b))) * ( dist (c,b))) * ( cos ( angle (( Tn2TR a),( Tn2TR b),( Tn2TR c)))))) by ThLawOfCosines;

          

           A21: ( dist (a1,b1)) <> 0 & ( dist (c1,b1)) <> 0 by A1, A6, A14, ThEgal;

          (( dist (c1,a1)) ^2 ) = (((( dist (a1,b1)) ^2 ) + (( dist (c1,b1)) ^2 )) - (((2 * ( dist (a1,b1))) * ( dist (c1,b1))) * ( cos ( angle (( Tn2TR a1),( Tn2TR b1),( Tn2TR c1)))))) by ThLawOfCosines;

          

          then

           A22: ( cos ( angle (( Tn2TR a1),( Tn2TR b1),( Tn2TR c1)))) = ((((( dist (c,a)) ^2 ) - (( dist (a,b)) ^2 )) - (( dist (c,b)) ^2 )) / ( - ((2 * ( dist (a,b))) * ( dist (c,b))))) by A6, Th1, A21

          .= ( cos ( angle (( Tn2TR a),( Tn2TR b),( Tn2TR c)))) by A20, A19, Th1;

          (( dist (c,x)) ^2 ) = (((( dist (x,b)) ^2 ) + (( dist (c,b)) ^2 )) - (((2 * ( dist (x,b))) * ( dist (c,b))) * ( cos ( angle (( Tn2TR x),( Tn2TR b),( Tn2TR c)))))) by ThLawOfCosines

          .= (((( dist (x1,b1)) ^2 ) + (( dist (c1,b1)) ^2 )) - (((2 * ( dist (x1,b1))) * ( dist (c1,b1))) * ( - ( cos ( angle (( Tn2TR a1),( Tn2TR b1),( Tn2TR c1))))))) by A17, EUCLID_6: 3, A6, A9, A22

          .= (((( dist (x1,b1)) ^2 ) + (( dist (c1,b1)) ^2 )) - (((2 * ( dist (x1,b1))) * ( dist (c1,b1))) * ( cos ( angle (( Tn2TR x1),( Tn2TR b1),( Tn2TR c1)))))) by A18, EUCLID_6: 3

          .= (( dist (c1,x1)) ^2 ) by ThLawOfCosines;

          hence thesis;

        end;

      end;

      hence thesis by ThConv9;

    end;

    

     ThBetweennessIdentity: TarskiEuclid2Space is satisfying_BetweennessIdentity

    proof

      let a,b be POINT of TarskiEuclid2Space ;

      assume between (a,b,a);

      then ( Tn2TR b) in ( LSeg (( Tn2TR a),( Tn2TR a))) by ThConv6;

      then ( Tn2TR b) in {( Tn2TR a)} by RLTOPSP1: 70;

      hence thesis by TARSKI:def 1;

    end;

    begin

    theorem :: GTARSKI2:30

    

     THQQ: ( OASpace ( TOP-REAL 2)) is OAffinSpace

    proof

      (ex u,v be VECTOR of ( TOP-REAL 2) st for a,b be Real st ((a * u) + (b * v)) = ( 0. ( TOP-REAL 2)) holds a = 0 & b = 0 )

      proof

        reconsider u = |[1, 0 ]|, v = |[ 0 , 1]| as VECTOR of ( TOP-REAL 2);

        now

          let a,b be Real;

          assume

           A1: ((a * u) + (b * v)) = ( 0. ( TOP-REAL 2));

          

           A2: ((a * u) + (b * v)) = ( |[(a * 1), (a * 0 )]| + (b * v)) by EUCLID: 58

          .= ( |[(a * 1), (a * 0 )]| + |[(b * 0 ), (b * 1)]|) by EUCLID: 58

          .= |[(a + 0 ), ( 0 + b)]| by EUCLID: 56

          .= |[a, b]|;

          ( |[a, b]| `1 ) = a & ( |[a, b]| `2 ) = b & ( |[ 0 , 0 ]| `1 ) = 0 & ( |[ 0 , 0 ]| `2 ) = 0 by EUCLID: 52;

          hence a = 0 & b = 0 by A1, A2, EUCLID: 54;

        end;

        hence thesis;

      end;

      hence thesis by ANALOAF: 26;

    end;

    theorem :: GTARSKI2:31

    

     THSS: for a,b,c be Element of ( OASpace ( TOP-REAL 2)) holds Mid (a,b,c) iff a = b or b = c or (ex u,v be Point of ( TOP-REAL 2) st u = a & v = c & b in ( LSeg (u,v)))

    proof

      let a,b,c be Element of ( OASpace ( TOP-REAL 2));

       A1:

      now

        assume Mid (a,b,c);

        then (a,b) // (b,c);

        then

        consider u,v,w,y be VECTOR of ( TOP-REAL 2) such that

         A2: [a, b] = [u, v] and

         A3: [b, c] = [w, y] and

         A4: (u,v) // (w,y) by ANALOAF:def 3;

        

         A5: a = u & b = v & b = w & c = y by A2, A3, XTUPLE_0: 1;

        per cases by A4;

          suppose u = v;

          hence a = b or b = c or (ex u,v be Point of ( TOP-REAL 2) st u = a & v = c & b in ( LSeg (u,v))) by A5;

        end;

          suppose w = y;

          hence a = b or b = c or (ex u,v be Point of ( TOP-REAL 2) st u = a & v = c & b in ( LSeg (u,v))) by A5;

        end;

          suppose ex r,s be Real st 0 < r & 0 < s & (r * (v - u)) = (s * (y - w));

          then

          consider r,s be Real such that

           A6: 0 < r and

           A7: 0 < s and

           A8: (r * (v - u)) = (s * (y - w));

          ((r * v) - (r * u)) = (r * (v - u)) by RLVECT_1: 34

          .= ((s * y) - (s * v)) by A5, A8, RLVECT_1: 34;

          then

           A9: ((r + s) * v) = ((r * u) + (s * y)) by THJC;

          reconsider t = (1 / (r + s)) as Real;

          

           A10: (1 - (s / (r + s))) = (((r + s) / (r + s)) - (s / (r + s))) by A6, A7, XCMPLX_1: 60

          .= (r / (r + s));

          

           A11: ((1 / (r + s)) * (r + s)) = ((r + s) / (r + s))

          .= 1 by A6, A7, XCMPLX_1: 60;

          

           A12: v = (1 * v) by RVSUM_1: 52

          .= (t * ((r + s) * v)) by A11, RVSUM_1: 49

          .= ((t * (r * u)) + (t * (s * y))) by RVSUM_1: 51, A9

          .= (((t * r) * u) + (t * (s * y))) by RVSUM_1: 49

          .= (((1 - (s / (r + s))) * u) + ((s / (r + s)) * y)) by A10, RVSUM_1: 49;

          reconsider l = (s / (r + s)) as Real;

           0 <= l <= 1 & v = (((1 - l) * u) + (l * y)) by A12, A6, A7, THJD;

          then v in { (((1 - l) * u) + (l * y)) where l be Real : 0 <= l & l <= 1 };

          then b in ( LSeg (u,y)) by A5, RLTOPSP1:def 2;

          hence a = b or b = c or (ex u,v be Point of ( TOP-REAL 2) st u = a & v = c & b in ( LSeg (u,v))) by A5;

        end;

      end;

      now

        assume

         A13: a = b or b = c or (ex u,v be Point of ( TOP-REAL 2) st u = a & v = c & b in ( LSeg (u,v)));

        reconsider OAS = ( OASpace ( TOP-REAL 2)) as OAffinSpace by THQQ;

        per cases by A13;

          suppose

           A14: a = b;

          a is Element of OAS & b is Element of OAS;

          hence Mid (a,b,c) by A14, DIRAF: 10;

        end;

          suppose

           A15: b = c;

          b is Element of OAS & c is Element of OAS;

          hence Mid (a,b,c) by A15, DIRAF: 10;

        end;

          suppose ex u,v be Point of ( TOP-REAL 2) st u = a & v = c & b in ( LSeg (u,v));

          then

          consider u,v be Point of ( TOP-REAL 2) such that

           A16: u = a and

           A17: v = c and

           A18: b in ( LSeg (u,v));

          b in { (((1 - l) * u) + (l * v)) where l be Real : 0 <= l & l <= 1 } by RLTOPSP1:def 2, A18;

          then

          consider l be Real such that

           A19: b = (((1 - l) * u) + (l * v)) and

           A20: 0 <= l and

           A21: l <= 1;

          reconsider w = b, y = b as Point of ( TOP-REAL 2);

          now

            take u, w, y, v;

            thus [a, b] = [u, w] & [b, c] = [y, v] by A16, A17;

            

             A22: (w - ((1 - l) * u)) = (((l * v) + ((1 - l) * u)) + ((( - 1) * (1 - l)) * u)) by A19, RVSUM_1: 49

            .= ((l * v) + (((1 - l) * u) + (( - (1 - l)) * u))) by RVSUM_1: 15

            .= ((l * v) + (((1 - l) + ( - (1 - l))) * u)) by RVSUM_1: 50

            .= (l * v) by THJE;

             |[(l * (v `1 )), (l * (v `2 ))]| = (l * v) by EUCLID: 57

            .= ( |[(w `1 ), (w `2 )]| - ((1 - l) * u)) by A22, EUCLID: 53

            .= ( |[(w `1 ), (w `2 )]| - |[((1 - l) * (u `1 )), ((1 - l) * (u `2 ))]|) by EUCLID: 57

            .= |[((w `1 ) - ((1 - l) * (u `1 ))), ((w `2 ) - ((1 - l) * (u `2 )))]| by EUCLID: 62;

            then

             A23: (l * (v `1 )) = ((w `1 ) - ((1 - l) * (u `1 ))) & (l * (v `2 )) = ((w `2 ) - ((1 - l) * (u `2 ))) by FINSEQ_1: 77;

            

             A24: (((1 - l) * w) - ((1 - l) * u)) = ((l * v) - (l * w))

            proof

              

               A25: (((1 - l) * w) - ((1 - l) * u)) = (((1 - l) * |[(w `1 ), (w `2 )]|) - ((1 - l) * u)) by EUCLID: 53

              .= (((1 - l) * |[(w `1 ), (w `2 )]|) - ((1 - l) * |[(u `1 ), (u `2 )]|)) by EUCLID: 53

              .= ( |[((1 - l) * (w `1 )), ((1 - l) * (w `2 ))]| - ((1 - l) * |[(u `1 ), (u `2 )]|)) by EUCLID: 58

              .= ( |[((1 - l) * (w `1 )), ((1 - l) * (w `2 ))]| - |[((1 - l) * (u `1 )), ((1 - l) * (u `2 ))]|) by EUCLID: 58

              .= |[(((1 - l) * (w `1 )) - ((1 - l) * (u `1 ))), (((1 - l) * (w `2 )) - ((1 - l) * (u `2 )))]| by EUCLID: 62

              .= |[((l * (v `1 )) - (l * (w `1 ))), ((l * (v `2 )) - (l * (w `2 )))]| by A23;

              ((l * v) - (l * w)) = ((l * |[(v `1 ), (v `2 )]|) - (l * w)) by EUCLID: 53

              .= ((l * |[(v `1 ), (v `2 )]|) - (l * |[(w `1 ), (w `2 )]|)) by EUCLID: 53

              .= ( |[(l * (v `1 )), (l * (v `2 ))]| - (l * |[(w `1 ), (w `2 )]|)) by EUCLID: 58

              .= ( |[(l * (v `1 )), (l * (v `2 ))]| - |[(l * (w `1 )), (l * (w `2 ))]|) by EUCLID: 58

              .= |[((l * (v `1 )) - (l * (w `1 ))), ((l * (v `2 )) - (l * (w `2 )))]| by EUCLID: 62;

              hence thesis by A25;

            end;

            

             A26: ((1 - l) * (w - u)) = (((1 - l) * w) + ((1 - l) * ( - u))) by RVSUM_1: 51

            .= (((1 - l) * w) + (((1 - l) * ( - 1)) * u)) by RVSUM_1: 49

            .= (((1 - l) * w) - ((1 - l) * u)) by RVSUM_1: 49

            .= ((l * v) + ((( - 1) * l) * w)) by A24, RVSUM_1: 49

            .= ((l * v) + (l * (( - 1) * w))) by RVSUM_1: 49

            .= (l * (v - w)) by RVSUM_1: 51;

            per cases by A20, A21, XXREAL_0: 1;

              suppose l = 1;

              

              then w = (v + ( 0 * u)) by A19, RVSUM_1: 52

              .= v by THJE;

              hence (u,w) // (y,v);

            end;

              suppose l = 0 ;

              

              then w = (u + ( 0 * v)) by A19, RVSUM_1: 52

              .= u by THJE;

              hence (u,w) // (y,v);

            end;

              suppose

               A27: 0 < l < 1;

              then (l - l) < (1 - l) by XREAL_1: 9;

              hence (u,w) // (y,v) by A27, A26;

            end;

          end;

          then (a,b) // (b,c) by ANALOAF:def 3;

          hence Mid (a,b,c);

        end;

      end;

      hence thesis by A1;

    end;

    theorem :: GTARSKI2:32

    

     THSS2: for a,b,c be Element of ( OASpace ( TOP-REAL 2)) holds Mid (a,b,c) iff (ex u,v be Point of ( TOP-REAL 2) st u = a & v = c & b in ( LSeg (u,v)))

    proof

      let a,b,c be Element of ( OASpace ( TOP-REAL 2));

      hereby

        assume Mid (a,b,c);

        per cases by THSS;

          suppose

           A1: a = b;

          reconsider u = a, v = c as Point of ( TOP-REAL 2);

          u in ( LSeg (u,v)) by RLTOPSP1: 68;

          hence ex u,v be Point of ( TOP-REAL 2) st u = a & v = c & b in ( LSeg (u,v)) by A1;

        end;

          suppose

           A2: b = c;

          reconsider u = a, v = c as Point of ( TOP-REAL 2);

          v in ( LSeg (u,v)) by RLTOPSP1: 68;

          hence ex u,v be Point of ( TOP-REAL 2) st u = a & v = c & b in ( LSeg (u,v)) by A2;

        end;

          suppose ex u,v be Point of ( TOP-REAL 2) st u = a & v = c & b in ( LSeg (u,v));

          hence ex u,v be Point of ( TOP-REAL 2) st u = a & v = c & b in ( LSeg (u,v));

        end;

      end;

      assume ex u,v be Point of ( TOP-REAL 2) st u = a & v = c & b in ( LSeg (u,v));

      hence Mid (a,b,c) by THSS;

    end;

    theorem :: GTARSKI2:33

    

     THSS3: for a,b,c be Element of ( OASpace ( TOP-REAL 2)), ap,bp,cp be POINT of TarskiEuclid2Space st a = ap & b = bp & c = cp holds Mid (a,b,c) iff between (ap,bp,cp)

    proof

      let a,b,c be Element of ( OASpace ( TOP-REAL 2)), ap,bp,cp be POINT of TarskiEuclid2Space ;

      assume that

       A1: a = ap and

       A2: b = bp and

       A3: c = cp;

      hereby

        assume Mid (a,b,c);

        then ex u,v be Point of ( TOP-REAL 2) st u = a & v = c & b in ( LSeg (u,v)) by THSS2;

        then ( Tn2TR bp) in ( LSeg (( Tn2TR ap),( Tn2TR cp))) by A1, A2, A3;

        hence between (ap,bp,cp) by ThConv6;

      end;

      assume between (ap,bp,cp);

      then ( Tn2TR bp) in ( LSeg (( Tn2TR ap),( Tn2TR cp))) by ThConv6;

      hence Mid (a,b,c) by A1, A2, A3, THSS2;

    end;

    begin

    theorem :: GTARSKI2:34

    

     THORANGE: for A,B,C,D be Element of ( TOP-REAL 2) st B in ( LSeg (A,C)) & C in ( LSeg (A,D)) holds B in ( LSeg (A,D))

    proof

      let A,B,C,D be Element of ( TOP-REAL 2);

      assume that

       A1: B in ( LSeg (A,C)) and

       A2: C in ( LSeg (A,D));

      B in { (((1 - r) * A) + (r * C)) where r be Real : 0 <= r & r <= 1 } by A1, RLTOPSP1:def 2;

      then

      consider r be Real such that

       A3: B = (((1 - r) * A) + (r * C)) and

       A4: 0 <= r and

       A5: r <= 1;

      C in { (((1 - r) * A) + (r * D)) where r be Real : 0 <= r & r <= 1 } by A2, RLTOPSP1:def 2;

      then

      consider s be Real such that

       A6: C = (((1 - s) * A) + (s * D)) and

       A7: 0 <= s and

       A8: s <= 1;

      reconsider t = (r * s) as Real;

      

       A9: (r * s) <= (1 * 1) by A4, A5, A7, A8, XREAL_1: 66;

      (s * D) = |[(s * (D `1 )), (s * (D `2 ))]| by EUCLID: 57;

      

      then

       A10: (r * (((1 - s) * A) + (s * D))) = (r * ( |[((1 - s) * (A `1 )), ((1 - s) * (A `2 ))]| + |[(s * (D `1 )), (s * (D `2 ))]|)) by EUCLID: 57

      .= (r * |[(((1 - s) * (A `1 )) + (s * (D `1 ))), (((1 - s) * (A `2 )) + (s * (D `2 )))]|) by EUCLID: 56

      .= |[(r * (((1 - s) * (A `1 )) + (s * (D `1 )))), (r * (((1 - s) * (A `2 )) + (s * (D `2 ))))]| by EUCLID: 58;

      B = ( |[((1 - r) * (A `1 )), ((1 - r) * (A `2 ))]| + |[(r * (((1 - s) * (A `1 )) + (s * (D `1 )))), (r * (((1 - s) * (A `2 )) + (s * (D `2 ))))]|) by A3, A6, A10, EUCLID: 57

      .= |[(((1 - r) * (A `1 )) + (r * (((1 - s) * (A `1 )) + (s * (D `1 ))))), (((1 - r) * (A `2 )) + (r * (((1 - s) * (A `2 )) + (s * (D `2 )))))]| by EUCLID: 56

      .= |[(((1 - (r * s)) * (A `1 )) + ((r * s) * (D `1 ))), (((1 - (r * s)) * (A `2 )) + ((r * s) * (D `2 )))]|

      .= ( |[((1 - (r * s)) * (A `1 )), ((1 - (r * s)) * (A `2 ))]| + |[((r * s) * (D `1 )), ((r * s) * (D `2 ))]|) by EUCLID: 56

      .= (((1 - (r * s)) * A) + |[((r * s) * (D `1 )), ((r * s) * (D `2 ))]|) by EUCLID: 57

      .= (((1 - t) * A) + (t * D)) by EUCLID: 57;

      then B in { (((1 - r) * A) + (r * D)) where r be Real : 0 <= r & r <= 1 } by A9, A4, A7;

      hence thesis by RLTOPSP1:def 2;

    end;

    theorem :: GTARSKI2:35

    

     THORANGE2: for A,B,C,D be Element of ( TOP-REAL 2) st B <> C & B in ( LSeg (A,C)) & C in ( LSeg (B,D)) holds C in ( LSeg (A,D))

    proof

      let A,B,C,D be Element of ( TOP-REAL 2);

      assume that

       A1: B <> C and

       A2: B in ( LSeg (A,C)) and

       A3: C in ( LSeg (B,D));

      reconsider OAS = ( OASpace ( TOP-REAL 2)) as OAffinSpace by THQQ;

      reconsider ta = A, tb = B, tc = C, td = D as Element of OAS;

       Mid (ta,tb,tc) & Mid (tb,tc,td) by A2, A3, THSS2;

      then ex u,v be Point of ( TOP-REAL 2) st u = ta & v = td & tc in ( LSeg (u,v)) by A1, DIRAF: 12, THSS2;

      hence thesis;

    end;

    theorem :: GTARSKI2:36

    

     THPOIRE: for p,q,r,s be Point of TarskiEuclid2Space st between (p,q,r) & between (p,r,s) holds between (p,q,s)

    proof

      let p,q,r,s be Point of TarskiEuclid2Space ;

      assume that

       A1: between (p,q,r) and

       A2: between (p,r,s);

      ( Tn2TR q) in ( LSeg (( Tn2TR p),( Tn2TR r))) & ( Tn2TR r) in ( LSeg (( Tn2TR p),( Tn2TR s))) by A1, A2, ThConv6;

      hence thesis by ThConv6, THORANGE;

    end;

    theorem :: GTARSKI2:37

    

     THNOIX: for A,B,C,D be Point of ( TOP-REAL 2) st B in ( LSeg (A,C)) & D in ( LSeg (A,B)) holds B in ( LSeg (D,C))

    proof

      let A,B,C,D be Point of ( TOP-REAL 2);

      assume that

       A1: B in ( LSeg (A,C)) and

       A2: D in ( LSeg (A,B));

      

       A3: (( dist (A,D)) + ( dist (D,C))) = ( dist (A,C)) by A1, A2, THORANGE, EUCLID12: 12;

      

       A4: (( dist (A,B)) + ( dist (B,C))) = ( dist (A,C)) by A1, EUCLID12: 12;

      (( dist (A,D)) + ( dist (D,B))) = ( dist (A,B)) by A2, EUCLID12: 12;

      then (( dist (D,B)) + ( dist (B,C))) = ( dist (D,C)) by A3, A4;

      hence thesis by EUCLID12: 12;

    end;

    theorem :: GTARSKI2:38

    

     THNOIX2: for p,q,r,s be Point of TarskiEuclid2Space st between (p,q,r) & between (p,s,q) holds between (s,q,r)

    proof

      let p,q,r,s be Point of TarskiEuclid2Space ;

      assume that

       A1: between (p,q,r) and

       A2: between (p,s,q);

      

       A3: ( Tn2TR q) in ( LSeg (( Tn2TR p),( Tn2TR r))) by A1, ThConv6;

      ( Tn2TR s) in ( LSeg (( Tn2TR p),( Tn2TR q))) by A2, ThConv6;

      then ( Tn2TR q) in ( LSeg (( Tn2TR s),( Tn2TR r))) by A3, THNOIX;

      hence thesis by ThConv6;

    end;

    theorem :: GTARSKI2:39

    

     THNOIX3: for p,q,r,s be Point of TarskiEuclid2Space st q <> r & between (p,q,r) & between (q,r,s) holds between (p,q,s)

    proof

      let p,q,r,s be Point of TarskiEuclid2Space ;

      assume that

       A1: q <> r and

       A2: between (p,q,r) and

       A3: between (q,r,s);

      

       A4: ( Tn2TR q) in ( LSeg (( Tn2TR p),( Tn2TR r))) by A2, ThConv6;

      then

       A5: (( dist (( Tn2TR p),( Tn2TR q))) + ( dist (( Tn2TR q),( Tn2TR r)))) = ( dist (( Tn2TR p),( Tn2TR r))) by EUCLID12: 12;

      

       A6: ( Tn2TR r) in ( LSeg (( Tn2TR q),( Tn2TR s))) by A3, ThConv6;

      

       A7: ( Tn2TR r) in ( LSeg (( Tn2TR p),( Tn2TR s))) by A1, A4, A6, THORANGE2;

      (( dist (( Tn2TR p),( Tn2TR q))) + ( dist (( Tn2TR q),( Tn2TR s)))) = ((( dist (( Tn2TR p),( Tn2TR r))) - ( dist (( Tn2TR q),( Tn2TR r)))) + (( dist (( Tn2TR q),( Tn2TR r))) + ( dist (( Tn2TR r),( Tn2TR s))))) by A5, A6, EUCLID12: 12

      .= (( dist (( Tn2TR p),( Tn2TR r))) + ( dist (( Tn2TR r),( Tn2TR s))))

      .= ( dist (( Tn2TR p),( Tn2TR s))) by A7, EUCLID12: 12;

      then ( Tn2TR q) in ( LSeg (( Tn2TR p),( Tn2TR s))) by EUCLID12: 12;

      hence thesis by ThConv6;

    end;

    theorem :: GTARSKI2:40

    for p,q,r,s be Point of TarskiEuclid2Space st q <> r & between (p,q,r) & between (q,r,s) holds between (p,r,s)

    proof

      let p,q,r,s be Point of TarskiEuclid2Space ;

      assume that

       A1: q <> r and

       A2: between (p,q,r) and

       A3: between (q,r,s);

      

       A4: ( Tn2TR q) in ( LSeg (( Tn2TR p),( Tn2TR r))) by A2, ThConv6;

      

       A6: ( Tn2TR r) in ( LSeg (( Tn2TR q),( Tn2TR s))) by A3, ThConv6;

      ( Tn2TR r) in ( LSeg (( Tn2TR p),( Tn2TR s))) by A1, A4, A6, THORANGE2;

      hence thesis by ThConv6;

    end;

    

     ThPasch: TarskiEuclid2Space is satisfying_Pasch

    proof

      set S = TarskiEuclid2Space ;

      now

        let a,b,p,q,z be POINT of S;

        assume that

         A1: between (a,p,z) and

         A2: between (b,q,z);

        reconsider OAS = ( OASpace ( TOP-REAL 2)) as OAffinSpace by THQQ;

        

         A3: OAS is satisfying_Int_Bet_Pasch by PASCH: 30;

        ( Tn2TR a) is Element of ( REAL 2) & ( Tn2TR b) is Element of ( REAL 2) & ( Tn2TR p) is Element of ( REAL 2) & ( Tn2TR z) is Element of ( REAL 2) & ( Tn2TR q) is Element of ( REAL 2) by EUCLID: 22;

        then

        reconsider a1 = a, b1 = b, p1 = p, z1 = z, q1 = q as Element of OAS;

         Mid (a1,p1,z1) by A1, THSS3;

        then

         A4: Mid (z1,p1,a1) by DIRAF: 9;

         Mid (b1,q1,z1) by A2, THSS3;

        then

         A5: Mid (z1,q1,b1) by DIRAF: 9;

        per cases ;

          suppose (z1,p1,b1) are_collinear ;

          then (z1,p1) '||' (z1,b1);

          per cases by DIRAF: 2;

            suppose (z1,p1) // (z1,b1);

            then

            consider u,v,w,y be VECTOR of ( TOP-REAL 2) such that

             A6: [z1, p1] = [u, v] and

             A7: [z1, b1] = [w, y] and

             A8: (u,v) // (w,y) by ANALOAF:def 3;

            

             A9: u = z1 & p1 = v & z1 = w & b1 = y by A6, A7, XTUPLE_0: 1;

            per cases by A8;

              suppose u = v;

              then

               A10: between (p,q,b) by A9, A2, ThConv7bis;

               between (q,q,a) by ThConv7;

              hence ex x be POINT of S st between (p,x,b) & between (q,x,a) by A10;

            end;

              suppose u = y;

              then

               A11: b = q by A2, A9, ThConv7ter;

              

               A12: between (p,b,b) by ThConv7;

               between (q,b,a) by A11, ThConv7;

              hence ex x be POINT of S st between (p,x,b) & between (q,x,a) by A12;

            end;

              suppose ex a,b be Real st 0 < a & 0 < b & (a * (v - u)) = (b * (y - u));

              then

              consider r,s be Real such that

               A13: 0 < r and

               A14: 0 < s and

               A15: (r * (v - u)) = (s * (y - u));

              per cases by XXREAL_0: 1;

                suppose r = s;

                then (v - u) = (y - u) by A13, A15, RLVECT_1: 36;

                then

                 A16: v = y by THSD2;

                

                 A17: between (p,p,b) by ThConv7;

                ( Tn2TR p) in ( LSeg (( Tn2TR z),( Tn2TR a))) by A1, ThConv6;

                then

                 A18: between (z,b,a) by A16, A9, ThConv6;

                ( Tn2TR q) in ( LSeg (( Tn2TR b),( Tn2TR z))) by A2, ThConv6;

                then

                 A19: between (z,q,b) by ThConv6;

                 between (q,p,a) by A16, A9, A18, A19, THNOIX2;

                hence ex x be POINT of S st between (p,x,b) & between (q,x,a) by A17;

              end;

                suppose

                 A20: r < s;

                reconsider t = (r / s) as Real;

                

                 A21: (r / s) < (s / s) by A13, A20, XREAL_1: 74;

                

                 A22: ((t * v) - (t * u)) = ( |[(t * (v `1 )), (t * (v `2 ))]| - (t * u)) by EUCLID: 57

                .= ( |[(t * (v `1 )), (t * (v `2 ))]| - |[(t * (u `1 )), (t * (u `2 ))]|) by EUCLID: 57

                .= |[((((1 / s) * r) * (v `1 )) - (((1 / s) * r) * (u `1 ))), ((t * (v `2 )) - (t * (u `2 )))]| by EUCLID: 62

                .= |[((1 / s) * ((r * (v `1 )) - (r * (u `1 )))), ((1 / s) * ((r * (v `2 )) - (r * (u `2 ))))]|

                .= ((1 / s) * |[((r * (v `1 )) - (r * (u `1 ))), ((r * (v `2 )) - (r * (u `2 )))]|) by EUCLID: 58;

                

                 A23: |[((r * (v `1 )) - (r * (u `1 ))), ((r * (v `2 )) - (r * (u `2 )))]| = |[(r * ((v `1 ) - (u `1 ))), (r * ((v `2 ) - (u `2 )))]|

                .= (r * |[((v `1 ) - (u `1 )), ((v `2 ) - (u `2 ))]|) by EUCLID: 58

                .= (s * (y - u)) by A15, EUCLID: 61;

                

                 A24: ((t * v) - (t * u)) = ((1 / s) * |[(s * ((y - u) `1 )), (s * ((y - u) `2 ))]|) by A23, A22, EUCLID: 57

                .= |[((1 / s) * (s * ((y - u) `1 ))), ((1 / s) * (s * ((y - u) `2 )))]| by EUCLID: 58

                .= |[((s * (1 / s)) * ((y - u) `1 )), ((s * (1 / s)) * ((y - u) `2 ))]|

                .= |[(1 * ((y - u) `1 )), ((s * (1 / s)) * ((y - u) `2 ))]| by XCMPLX_1: 106, A14

                .= |[((y - u) `1 ), (1 * ((y - u) `2 ))]| by XCMPLX_1: 106, A14

                .= (y - u) by EUCLID: 53;

                y = |[(((y `1 ) - (u `1 )) + (u `1 )), (((y `2 ) - (u `2 )) + (u `2 ))]| by EUCLID: 53

                .= ( |[((y `1 ) - (u `1 )), ((y `2 ) - (u `2 ))]| + |[(u `1 ), (u `2 )]|) by EUCLID: 56

                .= (( |[(y `1 ), (y `2 )]| - |[(u `1 ), (u `2 )]|) + |[(u `1 ), (u `2 )]|) by EUCLID: 62

                .= ((y - |[(u `1 ), (u `2 )]|) + |[(u `1 ), (u `2 )]|) by EUCLID: 53

                .= ((y - u) + |[(u `1 ), (u `2 )]|) by EUCLID: 53

                .= ((y - u) + u) by EUCLID: 53

                .= (( |[(t * (v `1 )), (t * (v `2 ))]| - (t * u)) + u) by A24, EUCLID: 57

                .= (( |[(t * (v `1 )), (t * (v `2 ))]| - |[(t * (u `1 )), (t * (u `2 ))]|) + u) by EUCLID: 57

                .= (( |[(t * (v `1 )), (t * (v `2 ))]| - |[(t * (u `1 )), (t * (u `2 ))]|) + |[(u `1 ), (u `2 )]|) by EUCLID: 53

                .= ( |[((t * (v `1 )) - (t * (u `1 ))), ((t * (v `2 )) - (t * (u `2 )))]| + |[(u `1 ), (u `2 )]|) by EUCLID: 62

                .= |[(((t * (v `1 )) - (t * (u `1 ))) + (u `1 )), (((t * (v `2 )) - (t * (u `2 ))) + (u `2 ))]| by EUCLID: 56

                .= |[((t * (v `1 )) + ((1 - t) * (u `1 ))), ((t * (v `2 )) + ((1 - t) * (u `2 )))]|

                .= ( |[((1 - t) * (u `1 )), ((1 - t) * (u `2 ))]| + |[(t * (v `1 )), (t * (v `2 ))]|) by EUCLID: 56

                .= (((1 - t) * u) + |[(t * (v `1 )), (t * (v `2 ))]|) by EUCLID: 57

                .= (((1 - t) * u) + (t * v)) by EUCLID: 57;

                then (((1 - t) * u) + (t * v)) = y & 0 < t & t < 1 by A21, A13, A14, XCMPLX_1: 60;

                then y in { (((1 - t) * u) + (t * v)) where t be Real : 0 <= t & t <= 1 };

                then ( Tn2TR b) in ( LSeg (( Tn2TR z),( Tn2TR p))) by A9, RLTOPSP1:def 2;

                then

                 A25: between (z,b,p) by ThConv6;

                

                 A26: between (z,p,a) by A1, ThConv7bis;

                

                 A27: between (z,q,b) by A2, ThConv7bis;

                then

                 A28: between (z,q,p) by A25, THPOIRE;

                ( Tn2TR p) in ( LSeg (( Tn2TR z),( Tn2TR a))) by A1, ThConv6;

                then

                 A29: (( dist (( Tn2TR z),( Tn2TR p))) + ( dist (( Tn2TR p),( Tn2TR a)))) = ( dist (( Tn2TR z),( Tn2TR a))) by EUCLID12: 12;

                ( Tn2TR q) in ( LSeg (( Tn2TR z),( Tn2TR p))) by A27, A25, THPOIRE, ThConv6;

                then

                 A30: (( dist (( Tn2TR z),( Tn2TR q))) + ( dist (( Tn2TR q),( Tn2TR p)))) = ( dist (( Tn2TR z),( Tn2TR p))) by EUCLID12: 12;

                ( Tn2TR q) in ( LSeg (( Tn2TR z),( Tn2TR a))) by A28, A26, THPOIRE, ThConv6;

                then (( dist (( Tn2TR z),( Tn2TR q))) + ( dist (( Tn2TR q),( Tn2TR a)))) = ( dist (( Tn2TR z),( Tn2TR a))) by EUCLID12: 12;

                then (( dist (( Tn2TR q),( Tn2TR p))) + ( dist (( Tn2TR p),( Tn2TR a)))) = ( dist (( Tn2TR q),( Tn2TR a))) by A29, A30;

                then

                 A31: ( Tn2TR p) in ( LSeg (( Tn2TR q),( Tn2TR a))) by EUCLID12: 12;

                

                 A32: between (p,p,b) by ThConv7;

                 between (q,p,a) by A31, ThConv6;

                hence ex x be POINT of S st between (p,x,b) & between (q,x,a) by A32;

              end;

                suppose

                 A33: s < r;

                set t = (s / r);

                t < (r / r) by A33, A13, XREAL_1: 74;

                then

                 A34: t < 1 by A13, XCMPLX_1: 60;

                

                 A35: ((t * y) - (t * u)) = ( |[(t * (y `1 )), (t * (y `2 ))]| - (t * u)) by EUCLID: 57

                .= ( |[(t * (y `1 )), (t * (y `2 ))]| - |[(t * (u `1 )), (t * (u `2 ))]|) by EUCLID: 57

                .= |[((((1 / r) * s) * (y `1 )) - (((1 / r) * s) * (u `1 ))), ((((1 / r) * s) * (y `2 )) - (((1 / r) * s) * (u `2 )))]| by EUCLID: 62

                .= |[((1 / r) * ((s * (y `1 )) - (s * (u `1 )))), ((1 / r) * ((s * (y `2 )) - (s * (u `2 ))))]|

                .= ((1 / r) * |[((s * (y `1 )) - (s * (u `1 ))), ((s * (y `2 )) - (s * (u `2 )))]|) by EUCLID: 58;

                

                 A36: |[((s * (y `1 )) - (s * (u `1 ))), ((s * (y `2 )) - (s * (u `2 )))]| = |[(s * ((y `1 ) - (u `1 ))), (s * ((y `2 ) - (u `2 )))]|

                .= (s * |[((y `1 ) - (u `1 )), ((y `2 ) - (u `2 ))]|) by EUCLID: 58

                .= (r * (v - u)) by A15, EUCLID: 61;

                

                 A37: ((t * y) - (t * u)) = ((1 / r) * |[(r * ((v - u) `1 )), (r * ((v - u) `2 ))]|) by A36, A35, EUCLID: 57

                .= |[((1 / r) * (r * ((v - u) `1 ))), ((1 / r) * (r * ((v - u) `2 )))]| by EUCLID: 58

                .= |[((r * (1 / r)) * ((v - u) `1 )), ((r * (1 / r)) * ((v - u) `2 ))]|

                .= |[(1 * ((v - u) `1 )), ((r * (1 / r)) * ((v - u) `2 ))]| by XCMPLX_1: 106, A13

                .= |[((v - u) `1 ), (1 * ((v - u) `2 ))]| by XCMPLX_1: 106, A13

                .= (v - u) by EUCLID: 53;

                v = |[(((v `1 ) - (u `1 )) + (u `1 )), (((v `2 ) - (u `2 )) + (u `2 ))]| by EUCLID: 53

                .= ( |[((v `1 ) - (u `1 )), ((v `2 ) - (u `2 ))]| + |[(u `1 ), (u `2 )]|) by EUCLID: 56

                .= (( |[(v `1 ), (v `2 )]| - |[(u `1 ), (u `2 )]|) + |[(u `1 ), (u `2 )]|) by EUCLID: 62

                .= ((v - |[(u `1 ), (u `2 )]|) + |[(u `1 ), (u `2 )]|) by EUCLID: 53

                .= ((v - u) + |[(u `1 ), (u `2 )]|) by EUCLID: 53

                .= (((t * y) - (t * u)) + u) by A37, EUCLID: 53

                .= (( |[(t * (y `1 )), (t * (y `2 ))]| - (t * u)) + u) by EUCLID: 57

                .= (( |[(t * (y `1 )), (t * (y `2 ))]| - |[(t * (u `1 )), (t * (u `2 ))]|) + u) by EUCLID: 57

                .= (( |[(t * (y `1 )), (t * (y `2 ))]| - |[(t * (u `1 )), (t * (u `2 ))]|) + |[(u `1 ), (u `2 )]|) by EUCLID: 53

                .= ( |[((t * (y `1 )) - (t * (u `1 ))), ((t * (y `2 )) - (t * (u `2 )))]| + |[(u `1 ), (u `2 )]|) by EUCLID: 62

                .= |[(((t * (y `1 )) - (t * (u `1 ))) + (u `1 )), (((t * (y `2 )) - (t * (u `2 ))) + (u `2 ))]| by EUCLID: 56

                .= |[((t * (y `1 )) + ((1 - t) * (u `1 ))), ((t * (y `2 )) + ((1 - t) * (u `2 )))]|

                .= ( |[((1 - t) * (u `1 )), ((1 - t) * (u `2 ))]| + |[(t * (y `1 )), (t * (y `2 ))]|) by EUCLID: 56

                .= (((1 - t) * u) + |[(t * (y `1 )), (t * (y `2 ))]|) by EUCLID: 57

                .= (((1 - t) * u) + (t * y)) by EUCLID: 57;

                then v in { (((1 - t) * u) + (t * y)) where t be Real : 0 <= t & t <= 1 } by A13, A14, A34;

                then ( Tn2TR p) in ( LSeg (( Tn2TR z),( Tn2TR b))) by A9, RLTOPSP1:def 2;

                then

                 A38: between (z,p,b) by ThConv6;

                

                 A39: between (z,p,a) by A1, ThConv7bis;

                

                 A40: between (z,q,b) by A2, ThConv7bis;

                

                 A41: Mid (z1,p1,b1) & Mid (z1,q1,b1) by A38, A40, THSS3;

                per cases ;

                  suppose

                   A42: z <> p;

                   Mid (z1,p1,b1) & Mid (z1,p1,a1) by A38, A39, THSS3;

                  per cases by A42, DIRAF: 15;

                    suppose Mid (p1,b1,a1);

                    per cases by A41, DIRAF: 17;

                      suppose Mid (z1,p1,q1);

                      then between (z,p,q) by THSS3;

                      then

                       A43: between (p,q,b) by A40, THNOIX2;

                       between (q,q,a) by ThConv7;

                      hence ex x be POINT of S st between (p,x,b) & between (q,x,a) by A43;

                    end;

                      suppose Mid (z1,q1,p1);

                      then between (z,q,p) by THSS3;

                      then

                       A44: between (q,p,a) by A39, THNOIX2;

                       between (p,p,b) by ThConv7;

                      hence ex x be POINT of S st between (p,x,b) & between (q,x,a) by A44;

                    end;

                  end;

                    suppose Mid (p1,a1,b1);

                    per cases by A41, DIRAF: 17;

                      suppose Mid (z1,p1,q1);

                      then between (z,p,q) by THSS3;

                      then

                       A45: between (p,q,b) by A40, THNOIX2;

                       between (q,q,a) by ThConv7;

                      hence ex x be POINT of S st between (p,x,b) & between (q,x,a) by A45;

                    end;

                      suppose Mid (z1,q1,p1);

                      then between (z,q,p) by THSS3;

                      then

                       A46: between (q,p,a) by A39, THNOIX2;

                       between (p,p,b) by ThConv7;

                      hence ex x be POINT of S st between (p,x,b) & between (q,x,a) by A46;

                    end;

                  end;

                end;

                  suppose

                   A47: z = p;

                   between (q,q,a) by ThConv7;

                  hence ex x be POINT of S st between (p,x,b) & between (q,x,a) by A47, A40;

                end;

              end;

            end;

          end;

            suppose (b1,z1) // (z1,p1);

            then Mid (b1,z1,p1);

            then Mid (p1,z1,b1) by DIRAF: 9;

            then

             A48: between (p,z,b) by THSS3;

            then

             A49: between (b,z,p) by ThConv7bis;

            

             A50: between (q,z,p) by A2, A49, THNOIX2;

            

             A51: between (z,p,a) by A1, ThConv7bis;

            per cases ;

              suppose z = p;

              then

               A52: between (p,q,b) by A2, ThConv7bis;

               between (q,q,a) by ThConv7;

              hence ex x be POINT of S st between (p,x,b) & between (q,x,a) by A52;

            end;

              suppose z <> p;

              then between (q,z,a) by A50, A51, THNOIX3;

              hence ex x be POINT of S st between (p,x,b) & between (q,x,a) by A48;

            end;

          end;

        end;

          suppose

           A53: not (z1,p1,b1) are_collinear ;

          consider y be Element of OAS such that

           A54: Mid (p1,y,b1) and

           A55: Mid (q1,y,a1) by A3, A53, A4, A5;

           the MetrStruct of TarskiEuclid2Space = the MetrStruct of ( Euclid 2) by GTARSKI1:def 13;

          then

          reconsider yt = y as POINT of S by EUCLID: 22;

          

           A56: between (p,yt,b) by A54, THSS3;

           between (q,yt,a) by A55, THSS3;

          hence ex x be POINT of S st between (p,x,b) & between (q,x,a) by A56;

        end;

      end;

      hence thesis;

    end;

    registration

      cluster TarskiEuclid2Space -> satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch;

      coherence by ThCongruenceSymmetry, ThCongruenceEquivalenceRelation, ThCongruenceIdentity, ThSegmentConstruction, ThSAS, ThBetweennessIdentity, ThPasch;

    end

    registration

      cluster TarskiEuclid2Space -> satisfying_Tarski-model;

      coherence ;

    end

    begin

    theorem :: GTARSKI2:41

    

     ThAZ9: for P,Q,R be Point of ( TOP-REAL 2), L be Element of ( line_of_REAL 2) st P in L & Q in L & R in L holds P in ( LSeg (Q,R)) or Q in ( LSeg (R,P)) or R in ( LSeg (P,Q))

    proof

      let P,Q,R be Point of ( TOP-REAL 2), L be Element of ( line_of_REAL 2);

      assume that

       A1: P in L and

       A2: Q in L and

       A3: R in L;

      L in ( line_of_REAL 2);

      then L in the set of all ( Line (x1,x2)) where x1,x2 be Element of ( REAL 2) by EUCLIDLP:def 4;

      then

      consider x1,x2 be Element of ( REAL 2) such that

       A4: L = ( Line (x1,x2));

      reconsider tx1 = x1, tx2 = x2 as Element of ( TOP-REAL 2) by EUCLID: 22;

      P in ( Line (tx1,tx2)) & Q in ( Line (tx1,tx2)) & R in ( Line (tx1,tx2)) by A1, A2, A3, A4, EUCLID12: 4;

      hence thesis by RLTOPSP1:def 16, TOPREAL9: 67;

    end;

    theorem :: GTARSKI2:42

    

     ThConvAG: for a,b,c be Element of TarskiEuclid2Space holds ( Tn2TR b) in ( LSeg (( Tn2TR a),( Tn2TR c))) implies ex jj be Real st 0 <= jj & jj <= 1 & (( Tn2TR b) - ( Tn2TR a)) = (jj * (( Tn2TR c) - ( Tn2TR a)))

    proof

      let a,b,c be Element of TarskiEuclid2Space ;

      assume ( Tn2TR b) in ( LSeg (( Tn2TR a),( Tn2TR c)));

      then

      consider jj be Real such that

       G2: 0 <= jj & jj <= 1 & ( Tn2TR b) = (((1 - jj) * ( Tn2TR a)) + (jj * ( Tn2TR c))) by RLTOPSP1: 76;

      set v = ( Tn2TR a), w = ( Tn2TR c);

      (( Tn2TR b) - ( Tn2TR a)) = ((((1 - jj) * v) - v) + (jj * w)) by RVSUM_1: 15, G2

      .= ((((1 - jj) + ( - 1)) * v) + (jj * w)) by RVSUM_1: 50

      .= ((jj * w) + ((jj * ( - 1)) * v))

      .= ((jj * w) + (jj * (( - 1) * v))) by RVSUM_1: 49

      .= (jj * (w - v)) by RVSUM_1: 51;

      hence thesis by G2;

    end;

    theorem :: GTARSKI2:43

    for n be Nat holds for a,b,c be Element of ( TarskiEuclidSpace n) holds ( Tn2TR b) in ( LSeg (( Tn2TR a),( Tn2TR c))) implies ex jj be Real st 0 <= jj <= 1 & (( Tn2TR b) - ( Tn2TR a)) = (jj * (( Tn2TR c) - ( Tn2TR a)))

    proof

      let n be Nat;

      let a,b,c be Element of ( TarskiEuclidSpace n);

      assume ( Tn2TR b) in ( LSeg (( Tn2TR a),( Tn2TR c)));

      then

      consider jj be Real such that

       G2: 0 <= jj <= 1 & ( Tn2TR b) = (((1 - jj) * ( Tn2TR a)) + (jj * ( Tn2TR c))) by RLTOPSP1: 76;

      set v = ( Tn2TR a), w = ( Tn2TR c);

      (( Tn2TR b) - ( Tn2TR a)) = ((((1 - jj) * v) - v) + (jj * w)) by RVSUM_1: 15, G2

      .= ((((1 - jj) + ( - 1)) * v) + (jj * w)) by RVSUM_1: 50

      .= ((jj * w) + ((jj * ( - 1)) * v))

      .= ((jj * w) + (jj * (( - 1) * v))) by RVSUM_1: 49

      .= (jj * (w - v)) by RVSUM_1: 51;

      hence thesis by G2;

    end;

    theorem :: GTARSKI2:44

    

     ThConvAGI: for a,b,c be Element of TarskiEuclid2Space holds (ex jj be Real st 0 <= jj & jj <= 1 & (( Tn2TR b) - ( Tn2TR a)) = (jj * (( Tn2TR c) - ( Tn2TR a)))) implies ( Tn2TR b) in ( LSeg (( Tn2TR a),( Tn2TR c)))

    proof

      let a,b,c be Element of TarskiEuclid2Space ;

      given jj be Real such that

       G2: 0 <= jj <= 1 & (( Tn2TR b) - ( Tn2TR a)) = (jj * (( Tn2TR c) - ( Tn2TR a)));

      set v = ( Tn2TR a), w = ( Tn2TR c);

      

       SS: (( Tn2TR b) + (v - v)) = (( Tn2TR b) + ( 0. ( TOP-REAL 2))) by RLVECT_1: 5

      .= ( Tn2TR b);

      

       G3: v = (1 * v) by RVSUM_1: 52;

      (( Tn2TR b) + (( - v) + v)) = ((jj * (( Tn2TR c) - ( Tn2TR a))) + v) by G2, RVSUM_1: 15;

      

      then ( Tn2TR b) = (((jj * w) + (jj * ( - v))) + v) by RVSUM_1: 51, SS

      .= (((jj * w) + ((jj * ( - 1)) * v)) + v) by RVSUM_1: 49

      .= (((jj * w) + (( - 1) * (jj * v))) + v) by RVSUM_1: 49

      .= ((jj * w) + (( - (jj * v)) + (1 * v))) by RVSUM_1: 15, G3

      .= ((jj * w) + (((( - 1) * jj) * v) + (1 * v))) by RVSUM_1: 49

      .= (((1 - jj) * v) + (jj * w)) by RVSUM_1: 50;

      then ( Tn2TR b) in { (((1 - r) * v) + (r * w)) where r be Real : 0 <= r & r <= 1 } by G2;

      hence thesis by RLTOPSP1:def 2;

    end;

    begin

    definition

      let S be TarskiGeometryStruct;

      :: GTARSKI2:def7

      attr S is satisfying_A8 means ex a,b,c be POINT of S st not between (a,b,c) & not between (b,c,a) & not between (c,a,b);

      :: GTARSKI2:def8

      attr S is satisfying_A9 means for a,b,c,p,q be POINT of S st p <> q & (a,p) equiv (a,q) & (b,p) equiv (b,q) & (c,p) equiv (c,q) holds between (a,b,c) or between (b,c,a) or between (c,a,b);

      :: GTARSKI2:def9

      attr S is satisfying_A10 means for a,b,c,d,t be POINT of S st between (a,d,t) & between (b,d,c) & a <> d holds ex x,y be POINT of S st between (a,b,x) & between (a,c,y) & between (x,t,y);

      :: GTARSKI2:def10

      attr S is satisfying_A11 means for X,Y be Subset of S st (ex a be POINT of S st for x,y be POINT of S st x in X & y in Y holds between (a,x,y)) holds (ex b be POINT of S st for x,y be POINT of S st x in X & y in Y holds between (x,b,y));

    end

    notation

      let S be TarskiGeometryStruct;

      synonym S is satisfying_Lower_Dimension_Axiom for S is satisfying_A8;

      synonym S is satisfying_Upper_Dimension_Axiom for S is satisfying_A9;

      synonym S is satisfying_Euclid_Axiom for S is satisfying_A10;

      synonym S is satisfying_Continuity_Axiom for S is satisfying_A11;

    end

    ::$Notion-Name

    theorem :: GTARSKI2:45

    

     AxiomA8: ex a,b,c be Point of TarskiEuclid2Space st not between (a,b,c) & not between (b,c,a) & not between (c,a,b)

    proof

       the MetrStruct of TarskiEuclid2Space = the MetrStruct of ( Euclid 2) by GTARSKI1:def 13;

      then

      reconsider a = |[ 0 , 0 ]|, b = |[1, 0 ]|, c = |[ 0 , 1]| as Point of TarskiEuclid2Space by EUCLID: 22;

      take a, b, c;

      thus not between (a,b,c)

      proof

        assume between (a,b,c);

        then ( Tn2TR b) in ( LSeg (( Tn2TR a),( Tn2TR c))) by ThConv6;

        then (( dist (( Tn2TR a),( Tn2TR b))) + ( dist (( Tn2TR b),( Tn2TR c)))) = ( dist (( Tn2TR a),( Tn2TR c))) by EUCLID12: 12;

        hence thesis by SQUARE_1: 19, THY1, THY2, THY3;

      end;

      thus not between (b,c,a)

      proof

        assume between (b,c,a);

        then ( Tn2TR c) in ( LSeg (( Tn2TR b),( Tn2TR a))) by ThConv6;

        then (( dist (( Tn2TR b),( Tn2TR c))) + ( dist (( Tn2TR c),( Tn2TR a)))) = ( dist (( Tn2TR b),( Tn2TR a))) by EUCLID12: 12;

        hence thesis by SQUARE_1: 19, THY1, THY2, THY3;

      end;

      assume between (c,a,b);

      then ( Tn2TR a) in ( LSeg (( Tn2TR c),( Tn2TR b))) by ThConv6;

      then (( dist (( Tn2TR c),( Tn2TR a))) + ( dist (( Tn2TR a),( Tn2TR b)))) = ( dist (( Tn2TR c),( Tn2TR b))) by EUCLID12: 12;

      hence thesis by SQUARE_1: 21, THY1, THY2, THY3;

    end;

    ::$Notion-Name

    theorem :: GTARSKI2:46

    

     AxiomA9: for a,b,c,p,q be Point of TarskiEuclid2Space st p <> q & (a,p) equiv (a,q) & (b,p) equiv (b,q) & (c,p) equiv (c,q) holds between (a,b,c) or between (b,c,a) or between (c,a,b)

    proof

      let a,b,c,p,q be Point of TarskiEuclid2Space ;

      assume that

       A1: p <> q and

       A2: (a,p) equiv (a,q) and

       A3: (b,p) equiv (b,q) and

       A4: (c,p) equiv (c,q);

       |.(( Tn2TR a) - ( Tn2TR p)).| = |.(( Tn2TR a) - ( Tn2TR q)).| by A2, ThConv4;

      then

       A5: ( Tn2TR a) in ( the_perpendicular_bisector (( Tn2TR p),( Tn2TR q))) by A1, EUCLID12: 60;

       |.(( Tn2TR b) - ( Tn2TR p)).| = |.(( Tn2TR b) - ( Tn2TR q)).| by A3, ThConv4;

      then

       A6: ( Tn2TR b) in ( the_perpendicular_bisector (( Tn2TR p),( Tn2TR q))) by A1, EUCLID12: 60;

       |.(( Tn2TR c) - ( Tn2TR p)).| = |.(( Tn2TR c) - ( Tn2TR q)).| by A4, ThConv4;

      then ( Tn2TR c) in ( the_perpendicular_bisector (( Tn2TR p),( Tn2TR q))) by A1, EUCLID12: 60;

      then ( Tn2TR a) in ( LSeg (( Tn2TR b),( Tn2TR c))) or ( Tn2TR b) in ( LSeg (( Tn2TR c),( Tn2TR a))) or ( Tn2TR c) in ( LSeg (( Tn2TR a),( Tn2TR b))) by A5, A6, ThAZ9;

      hence thesis by ThConv6;

    end;

    ::$Notion-Name

    theorem :: GTARSKI2:47

    

     AxiomA10: for a,b,c,d,t be Element of TarskiEuclid2Space st between (a,d,t) & between (b,d,c) & a <> d holds ex x,y be Element of TarskiEuclid2Space st between (a,b,x) & between (a,c,y) & between (x,t,y)

    proof

      let a,b,c,d,t be Element of TarskiEuclid2Space ;

      assume that

       A1: between (a,d,t) and

       A2: between (b,d,c) and

       A3: a <> d;

      

       G0: ( Tn2TR d) in ( LSeg (( Tn2TR a),( Tn2TR t))) by A1, ThConv6;

      set v = ( Tn2TR a), w = ( Tn2TR t);

      consider jj be Real such that

       G2: 0 <= jj & jj <= 1 & ( Tn2TR d) = (((1 - jj) * v) + (jj * w)) by RLTOPSP1: 76, G0;

      

       g1: (( Tn2TR d) - ( Tn2TR a)) = ((((1 - jj) * v) - v) + (jj * w)) by RVSUM_1: 15, G2

      .= ((((1 - jj) + ( - 1)) * v) + (jj * w)) by RVSUM_1: 50

      .= ((jj * w) + ((jj * ( - 1)) * v))

      .= ((jj * w) + (jj * (( - 1) * v))) by RVSUM_1: 49

      .= (jj * (w - v)) by RVSUM_1: 51;

      set jt = (1 / jj);

      

       JJ: jj <> 0

      proof

        assume jj = 0 ;

        then (( Tn2TR d) - ( Tn2TR a)) = ( 0. ( TOP-REAL 2)) by g1, RLVECT_1: 10;

        hence thesis by A3, RLVECT_1: 21;

      end;

      set xxx = ((jt * (( Tn2TR b) - ( Tn2TR a))) + ( Tn2TR a));

      

       ww: the MetrStruct of TarskiEuclid2Space = the MetrStruct of ( Euclid 2) by GTARSKI1:def 13;

      then

      reconsider xx = xxx as Element of TarskiEuclid2Space by EUCLID: 22;

      (jj * (xxx - ( Tn2TR a))) = (jj * ((jt * (( Tn2TR b) - ( Tn2TR a))) + (( Tn2TR a) - ( Tn2TR a)))) by RLVECT_1: 28

      .= (jj * (((1 / jj) * (( Tn2TR b) - ( Tn2TR a))) + ( 0. ( TOP-REAL 2)))) by RLVECT_1: 15

      .= ((jj * (1 / jj)) * (( Tn2TR b) - ( Tn2TR a))) by RLVECT_1:def 7

      .= (1 * (( Tn2TR b) - ( Tn2TR a))) by XCMPLX_0:def 7, JJ

      .= (( Tn2TR b) - ( Tn2TR a)) by RVSUM_1: 52;

      then ( Tn2TR b) in ( LSeg (( Tn2TR a),( Tn2TR xx))) by G2, ThConvAGI;

      then

       T1: between (a,b,xx) by ThConv6;

      set yyy = ((jt * (( Tn2TR c) - ( Tn2TR a))) + ( Tn2TR a));

      reconsider yy = yyy as Element of TarskiEuclid2Space by ww, EUCLID: 22;

      (jj * (yyy - ( Tn2TR a))) = (jj * ((jt * (( Tn2TR c) - ( Tn2TR a))) + (( Tn2TR a) - ( Tn2TR a)))) by RLVECT_1: 28

      .= (jj * ((jt * (( Tn2TR c) - ( Tn2TR a))) + ( 0. ( TOP-REAL 2)))) by RLVECT_1: 15

      .= ((jj * jt) * (( Tn2TR c) - ( Tn2TR a))) by RLVECT_1:def 7

      .= (1 * (( Tn2TR c) - ( Tn2TR a))) by XCMPLX_0:def 7, JJ

      .= (( Tn2TR c) - ( Tn2TR a)) by RVSUM_1: 52;

      then ( Tn2TR c) in ( LSeg (( Tn2TR a),( Tn2TR yy))) by G2, ThConvAGI;

      then

       T2: between (a,c,yy) by ThConv6;

      ( Tn2TR d) in ( LSeg (( Tn2TR b),( Tn2TR c))) by A2, ThConv6;

      then

      consider kk be Real such that

       Y1: 0 <= kk & kk <= 1 & (( Tn2TR d) - ( Tn2TR b)) = (kk * (( Tn2TR c) - ( Tn2TR b))) by ThConvAG;

      (jt * (( Tn2TR d) - ( Tn2TR a))) = (((1 / jj) * jj) * (( Tn2TR t) - ( Tn2TR a))) by g1, RLVECT_1:def 7

      .= (1 * (( Tn2TR t) - ( Tn2TR a))) by JJ, XCMPLX_0:def 7

      .= (( Tn2TR t) - ( Tn2TR a)) by RVSUM_1: 52;

      

      then

       w1: ((jt * (( Tn2TR d) - ( Tn2TR a))) + ( Tn2TR a)) = (( Tn2TR t) + (( - ( Tn2TR a)) + ( Tn2TR a))) by RLVECT_1:def 3

      .= (( Tn2TR t) + ( 0. ( TOP-REAL 2))) by RLVECT_1: 5;

      

       W2: (( Tn2TR yy) - ( Tn2TR xx)) = (((((1 / jj) * (( Tn2TR c) - ( Tn2TR a))) + ( Tn2TR a)) - ( Tn2TR a)) - ((1 / jj) * (( Tn2TR b) - ( Tn2TR a)))) by RLVECT_1: 27

      .= (((jt * (( Tn2TR c) - ( Tn2TR a))) + (( Tn2TR a) - ( Tn2TR a))) - ((1 / jj) * (( Tn2TR b) - ( Tn2TR a)))) by RLVECT_1: 28

      .= (((jt * (( Tn2TR c) - ( Tn2TR a))) + ( 0. ( TOP-REAL 2))) - ((1 / jj) * (( Tn2TR b) - ( Tn2TR a)))) by RLVECT_1: 15

      .= (jt * ((( Tn2TR c) - ( Tn2TR a)) - (( Tn2TR b) - ( Tn2TR a)))) by RLVECT_1: 34

      .= (jt * (( Tn2TR c) - ( Tn2TR b))) by ThWW;

      (( Tn2TR t) - ( Tn2TR xx)) = ((((jt * (( Tn2TR d) - ( Tn2TR a))) + ( Tn2TR a)) - ( Tn2TR a)) - ((1 / jj) * (( Tn2TR b) - ( Tn2TR a)))) by RLVECT_1: 27, w1

      .= (((jt * (( Tn2TR d) - ( Tn2TR a))) + (( Tn2TR a) - ( Tn2TR a))) - ((1 / jj) * (( Tn2TR b) - ( Tn2TR a)))) by RLVECT_1:def 3

      .= (((jt * (( Tn2TR d) - ( Tn2TR a))) + ( 0. ( TOP-REAL 2))) - ((1 / jj) * (( Tn2TR b) - ( Tn2TR a)))) by RLVECT_1: 5

      .= (jt * ((( Tn2TR d) - ( Tn2TR a)) - (( Tn2TR b) - ( Tn2TR a)))) by RLVECT_1: 34

      .= (jt * (( Tn2TR d) - ( Tn2TR b))) by ThWW

      .= ((jt * kk) * (( Tn2TR c) - ( Tn2TR b))) by RLVECT_1:def 7, Y1

      .= (kk * (( Tn2TR yy) - ( Tn2TR xx))) by W2, RLVECT_1:def 7;

      then ( Tn2TR t) in ( LSeg (( Tn2TR xx),( Tn2TR yy))) by Y1, ThConvAGI;

      then between (xx,t,yy) by ThConv6;

      hence thesis by T1, T2;

    end;

    begin

    ::$Notion-Name

    theorem :: GTARSKI2:48

    

     AxiomA11: for X,Y be Subset of TarskiEuclid2Space st (ex a be Element of TarskiEuclid2Space st for x,y be Element of TarskiEuclid2Space st x in X & y in Y holds between (a,x,y)) holds (ex b be Element of TarskiEuclid2Space st for x,y be Element of TarskiEuclid2Space st x in X & y in Y holds between (x,b,y))

    proof

      let X,Y be Subset of TarskiEuclid2Space ;

      given a be Element of TarskiEuclid2Space such that

       A1: for x,y be Element of TarskiEuclid2Space st x in X & y in Y holds between (a,x,y);

      per cases ;

        suppose

         SS: X c= {a} or Y = {} ;

        ex b be Element of TarskiEuclid2Space st for x,y be Element of TarskiEuclid2Space st x in X & y in Y holds between (x,b,y)

        proof

          take b = a;

          let x,y be Element of TarskiEuclid2Space ;

          assume x in X & y in Y;

          then x = a by SS, TARSKI:def 1;

          hence thesis by GTARSKI1: 17;

        end;

        hence thesis;

      end;

        suppose

         SSS: not X c= {a} & Y <> {} ;

        (X \ {a}) <> {} by XBOOLE_1: 37, SSS;

        then

        consider c be object such that

         G9: c in (X \ {a}) by XBOOLE_0:def 1;

        reconsider c as Element of TarskiEuclid2Space by G9;

        

         su: (X \ {a}) c= X by XBOOLE_1: 36;

        set S = { j where j be Real : j >= 1 & (( Tn2TR a) + (j * (( Tn2TR c) - ( Tn2TR a)))) in Y };

        S is real-membered

        proof

          let w be object;

          assume w in S;

          then

          consider j1 be Real such that

           G1: w = j1 & j1 >= 1 & (( Tn2TR a) + (j1 * (( Tn2TR c) - ( Tn2TR a)))) in Y;

          thus thesis by G1;

        end;

        then

        reconsider S as real-membered set;

        

         gg: 1 is LowerBound of S

        proof

          let x be ExtReal;

          assume x in S;

          then

          consider j1 be Real such that

           G1: x = j1 & j1 >= 1 & (( Tn2TR a) + (j1 * (( Tn2TR c) - ( Tn2TR a)))) in Y;

          thus thesis by G1;

        end;

        consider d be object such that

         G2: d in Y by XBOOLE_0:def 1, SSS;

        reconsider d as Element of TarskiEuclid2Space by G2;

        ( Tn2TR c) in ( LSeg (( Tn2TR a),( Tn2TR d))) by ThConv6, su, G9, A1, G2;

        then

        consider jda be Real such that

         G0: 0 <= jda & jda <= 1 & (( Tn2TR c) - ( Tn2TR a)) = (jda * (( Tn2TR d) - ( Tn2TR a))) by ThConvAG;

        set jd = (1 / jda);

        

         hh: jda <> 0

        proof

          assume jda = 0 ;

          

          then (( Tn2TR c) - ( Tn2TR a)) = (( 0. ( TOP-REAL 2)) + ( 0 * (( Tn2TR d) - ( Tn2TR a)))) by G0

          .= ( 0. ( TOP-REAL 2)) by THJE;

          hence thesis by G9, ZFMISC_1: 56, RLVECT_1: 21;

        end;

        

         Lem: for y be Element of TarskiEuclid2Space st y in Y holds ex j1 be Real st j1 >= 1 & (( Tn2TR y) - ( Tn2TR a)) = (j1 * (( Tn2TR c) - ( Tn2TR a)))

        proof

          let y be Element of TarskiEuclid2Space ;

          assume y in Y;

          then ( Tn2TR c) in ( LSeg (( Tn2TR a),( Tn2TR y))) by A1, su, G9, ThConv6;

          then

          consider j be Real such that

           H1: 0 <= j & j <= 1 & (( Tn2TR c) - ( Tn2TR a)) = (j * (( Tn2TR y) - ( Tn2TR a))) by ThConvAG;

          set j1 = (1 / j);

          

           H2: j <> 0

          proof

            assume j = 0 ;

            

            then (( Tn2TR c) - ( Tn2TR a)) = (( 0. ( TOP-REAL 2)) + ( 0 * (( Tn2TR y) - ( Tn2TR a)))) by H1

            .= ( 0. ( TOP-REAL 2)) by THJE;

            hence thesis by G9, ZFMISC_1: 56, RLVECT_1: 21;

          end;

          then

           H5: j1 >= 1 by H1, XREAL_1: 181;

          (j1 * (( Tn2TR c) - ( Tn2TR a))) = ((j1 * j) * (( Tn2TR y) - ( Tn2TR a))) by RLVECT_1:def 7, H1

          .= (1 * (( Tn2TR y) - ( Tn2TR a))) by H2, XCMPLX_0:def 7

          .= (( Tn2TR y) - ( Tn2TR a)) by RVSUM_1: 52;

          hence thesis by H5;

        end;

        

         Gy: (jd * (( Tn2TR c) - ( Tn2TR a))) = ((jd * jda) * (( Tn2TR d) - ( Tn2TR a))) by RLVECT_1:def 7, G0

        .= (1 * (( Tn2TR d) - ( Tn2TR a))) by hh, XCMPLX_0:def 7

        .= (( Tn2TR d) - ( Tn2TR a)) by RVSUM_1: 52;

        

         J2: jd >= 1 by XREAL_1: 181, G0, hh;

        ((jd * (( Tn2TR c) - ( Tn2TR a))) + ( Tn2TR a)) = (( Tn2TR d) + (( - ( Tn2TR a)) + ( Tn2TR a))) by RLVECT_1:def 3, Gy

        .= (( Tn2TR d) + ( 0. ( TOP-REAL 2))) by RLVECT_1: 5;

        then

         J1: jd in S by J2, G2;

        reconsider S as non empty bounded_below real-membered set by J1, gg, XXREAL_2:def 9;

        set k = ( inf S);

        set bb = (( Tn2TR a) + (k * (( Tn2TR c) - ( Tn2TR a))));

        

         p2: the MetrStruct of TarskiEuclid2Space = the MetrStruct of ( Euclid 2) by GTARSKI1:def 13;

        reconsider bb as Element of TarskiEuclid2Space by p2, EUCLID: 67;

        ex b be Element of TarskiEuclid2Space st for x,y be Element of TarskiEuclid2Space st x in X & y in Y holds between (x,b,y)

        proof

          take b = bb;

          let x,y be Element of TarskiEuclid2Space ;

          assume

           T1: x in X & y in Y;

          then

          consider j1 be Real such that

           HH: j1 >= 1 & (( Tn2TR y) - ( Tn2TR a)) = (j1 * (( Tn2TR c) - ( Tn2TR a))) by Lem;

          (( Tn2TR y) + (( - ( Tn2TR a)) + ( Tn2TR a))) = (( Tn2TR a) + (j1 * (( Tn2TR c) - ( Tn2TR a)))) by HH, RLVECT_1:def 3;

          then

           hH: (( Tn2TR y) + ( 0. ( TOP-REAL 2))) = (( Tn2TR a) + (j1 * (( Tn2TR c) - ( Tn2TR a)))) by RLVECT_1: 5;

          ( Tn2TR x) in ( LSeg (( Tn2TR a),( Tn2TR d))) by T1, A1, G2, ThConv6;

          then

          consider l be Real such that

           z1: 0 <= l & l <= 1 & (( Tn2TR x) - ( Tn2TR a)) = (l * (( Tn2TR d) - ( Tn2TR a))) by ThConvAG;

          

           z2: (( Tn2TR x) - ( Tn2TR a)) = ((l * jd) * (( Tn2TR c) - ( Tn2TR a))) by RLVECT_1:def 7, z1, Gy;

          set i = (l * jd);

          (( Tn2TR x) + (( - ( Tn2TR a)) + ( Tn2TR a))) = ((i * (( Tn2TR c) - ( Tn2TR a))) + ( Tn2TR a)) by z2, RLVECT_1:def 3;

          then

           E3: (( Tn2TR x) + ( 0. ( TOP-REAL 2))) = ((i * (( Tn2TR c) - ( Tn2TR a))) + ( Tn2TR a)) by RLVECT_1: 5;

          for h be ExtReal st h in S holds i <= h

          proof

            let h be ExtReal;

            assume h in S;

            then

            consider j1 be Real such that

             G1: h = j1 & j1 >= 1 & (( Tn2TR a) + (j1 * (( Tn2TR c) - ( Tn2TR a)))) in Y;

            set z = (( Tn2TR a) + (j1 * (( Tn2TR c) - ( Tn2TR a))));

            reconsider z as Element of TarskiEuclid2Space by EUCLID: 67, p2;

            ( Tn2TR x) in ( LSeg (( Tn2TR a),( Tn2TR z))) by T1, A1, G1, ThConv6;

            then

            consider ll be Real such that

             z1: 0 <= ll & ll <= 1 & (( Tn2TR x) - ( Tn2TR a)) = (ll * (( Tn2TR z) - ( Tn2TR a))) by ThConvAG;

            

             z0: (( Tn2TR c) - ( Tn2TR a)) <> ( 0. ( TOP-REAL 2))

            proof

              assume (( Tn2TR c) - ( Tn2TR a)) = ( 0. ( TOP-REAL 2));

              then (( Tn2TR c) + (( - ( Tn2TR a)) + ( Tn2TR a))) = (( 0. ( TOP-REAL 2)) + ( Tn2TR a)) by RLVECT_1:def 3;

              then (( Tn2TR c) + ( 0. ( TOP-REAL 2))) = (( 0. ( TOP-REAL 2)) + ( Tn2TR a)) by RLVECT_1: 5;

              hence thesis by G9, ZFMISC_1: 56;

            end;

            (( Tn2TR z) - ( Tn2TR a)) = ((j1 * (( Tn2TR c) - ( Tn2TR a))) + (( Tn2TR a) + ( - ( Tn2TR a)))) by RLVECT_1:def 3

            .= ((j1 * (( Tn2TR c) - ( Tn2TR a))) + ( 0. ( TOP-REAL 2))) by RLVECT_1: 5

            .= (j1 * (( Tn2TR c) - ( Tn2TR a)));

            then (( Tn2TR x) - ( Tn2TR a)) = ((ll * j1) * (( Tn2TR c) - ( Tn2TR a))) by z1, RLVECT_1:def 7;

            then (ll * j1) = i by RLVECT_1: 37, z0, z2;

            hence thesis by G1, XREAL_1: 153, z1;

          end;

          then

           fF: i is LowerBound of S by XXREAL_2:def 2;

          then

           f1: i <= k by XXREAL_2:def 4;

          j1 in S by hH, HH, T1;

          then

           F0: k <= j1 by XXREAL_2: 3;

          then

           f2: i <= j1 by f1, XXREAL_0: 2;

          

           ff: (( Tn2TR b) - ( Tn2TR x)) = ((( Tn2TR a) + (k * (( Tn2TR c) - ( Tn2TR a)))) + (( - (i * (( Tn2TR c) - ( Tn2TR a)))) + ( - ( Tn2TR a)))) by E3, RLVECT_1: 31

          .= ((((k * (( Tn2TR c) - ( Tn2TR a))) + ( Tn2TR a)) + ( - ( Tn2TR a))) + ( - (i * (( Tn2TR c) - ( Tn2TR a))))) by RLVECT_1:def 3

          .= (((k * (( Tn2TR c) - ( Tn2TR a))) + (( Tn2TR a) + ( - ( Tn2TR a)))) + ( - (i * (( Tn2TR c) - ( Tn2TR a))))) by RLVECT_1:def 3

          .= (((k * (( Tn2TR c) - ( Tn2TR a))) + ( 0. ( TOP-REAL 2))) + ( - (i * (( Tn2TR c) - ( Tn2TR a))))) by RLVECT_1: 5

          .= ((k * (( Tn2TR c) - ( Tn2TR a))) - (i * (( Tn2TR c) - ( Tn2TR a))))

          .= ((k - i) * (( Tn2TR c) - ( Tn2TR a))) by RLVECT_1: 35;

          set l = ((k - i) / (j1 - i));

          per cases ;

            suppose i = j1;

            then k = i by F0, f1, XXREAL_0: 1;

            

            then (( Tn2TR b) - ( Tn2TR x)) = (( 0. ( TOP-REAL 2)) + ( 0 * (( Tn2TR c) - ( Tn2TR a)))) by ff

            .= ( 0. ( TOP-REAL 2)) by THJE;

            then (( Tn2TR b) + (( - ( Tn2TR x)) + ( Tn2TR x))) = (( 0. ( TOP-REAL 2)) + ( Tn2TR x)) by RLVECT_1:def 3;

            then (( Tn2TR b) + ( 0. ( TOP-REAL 2))) = (( 0. ( TOP-REAL 2)) + ( Tn2TR x)) by RLVECT_1: 5;

            hence thesis by GTARSKI1: 17;

          end;

            suppose i <> j1;

            then i < j1 by f2, XXREAL_0: 1;

            then

             R1: (j1 - i) > 0 by XREAL_1: 50;

            (( Tn2TR y) - ( Tn2TR x)) = ((( Tn2TR a) + (j1 * (( Tn2TR c) - ( Tn2TR a)))) + (( - (i * (( Tn2TR c) - ( Tn2TR a)))) + ( - ( Tn2TR a)))) by RLVECT_1: 31, E3, hH

            .= ((((j1 * (( Tn2TR c) - ( Tn2TR a))) + ( Tn2TR a)) + ( - ( Tn2TR a))) - (i * (( Tn2TR c) - ( Tn2TR a)))) by RLVECT_1:def 3

            .= (((j1 * (( Tn2TR c) - ( Tn2TR a))) + (( Tn2TR a) + ( - ( Tn2TR a)))) - (i * (( Tn2TR c) - ( Tn2TR a)))) by RLVECT_1:def 3

            .= (((j1 * (( Tn2TR c) - ( Tn2TR a))) + ( 0. ( TOP-REAL 2))) - (i * (( Tn2TR c) - ( Tn2TR a)))) by RLVECT_1: 5

            .= ((j1 - i) * (( Tn2TR c) - ( Tn2TR a))) by RLVECT_1: 35;

            then ((1 / (j1 - i)) * (( Tn2TR y) - ( Tn2TR x))) = (((1 / (j1 - i)) * (j1 - i)) * (( Tn2TR c) - ( Tn2TR a))) by RLVECT_1:def 7;

            then ((1 / (j1 - i)) * (( Tn2TR y) - ( Tn2TR x))) = (1 * (( Tn2TR c) - ( Tn2TR a))) by XCMPLX_0:def 7, R1;

            then (( Tn2TR c) - ( Tn2TR a)) = ((1 / (j1 - i)) * (( Tn2TR y) - ( Tn2TR x))) by RVSUM_1: 52;

            then

             S2: (( Tn2TR b) - ( Tn2TR x)) = (l * (( Tn2TR y) - ( Tn2TR x))) by RLVECT_1:def 7, ff;

            

             R4: (k - i) <= (j1 - i) by XREAL_1: 13, F0;

            (k - i) >= 0 by fF, XREAL_1: 48, XXREAL_2:def 4;

            then ( Tn2TR b) in ( LSeg (( Tn2TR x),( Tn2TR y))) by S2, ThConvAGI, R4, XREAL_1: 183;

            hence thesis by ThConv6;

          end;

        end;

        hence thesis;

      end;

    end;

    registration

      cluster TarskiEuclid2Space -> satisfying_Lower_Dimension_Axiom satisfying_Upper_Dimension_Axiom satisfying_Euclid_Axiom satisfying_Continuity_Axiom;

      coherence by AxiomA8, AxiomA9, AxiomA10, AxiomA11;

    end

    begin

    reserve X,Y for Subset of TarskiEuclid2Space ;

    theorem :: GTARSKI2:49

    for a be Element of TarskiEuclid2Space st (for x,y be Element of TarskiEuclid2Space st x in X & y in Y holds between (a,x,y)) & a in Y holds X = {a} or X is empty

    proof

      let a be Element of TarskiEuclid2Space ;

      assume that

       A1: for x,y be Element of TarskiEuclid2Space st x in X & y in Y holds between (a,x,y) and

       A2: a in Y;

      

       M1: X c= {a}

      proof

        let x be object;

        assume

         L1: x in X;

        then

        reconsider x as Element of TarskiEuclid2Space ;

        a = x by GTARSKI1:def 10, A1, A2, L1;

        hence thesis by TARSKI:def 1;

      end;

      per cases ;

        suppose X is empty;

        hence thesis;

      end;

        suppose X is non empty;

        then

        consider x be object such that

         A3: x in X;

        reconsider x as Element of TarskiEuclid2Space by A3;

        a = x by GTARSKI1:def 10, A1, A2, A3;

        then {a} c= X by TARSKI:def 1, A3;

        hence thesis by M1;

      end;

    end;

    theorem :: GTARSKI2:50

    for a be Element of TarskiEuclid2Space st (for x,y be Element of TarskiEuclid2Space st x in X & y in Y holds between (a,x,y)) & X is non empty & Y is non empty & (X is trivial implies X <> {a}) holds ex b be Element of TarskiEuclid2Space st X c= ( Line (( Tn2TR a),( Tn2TR b))) & Y c= ( Line (( Tn2TR a),( Tn2TR b)))

    proof

      let a be Element of TarskiEuclid2Space such that

       A1: for x,y be Element of TarskiEuclid2Space st x in X & y in Y holds between (a,x,y) and

       A1A: X is non empty and

       A1B: Y is non empty and

       A3: X is trivial implies X <> {a};

      consider x0 be object such that

       K1: x0 in X by A1A;

      reconsider x0 as Element of TarskiEuclid2Space by K1;

      consider c be object such that

       MM: c in Y by A1B;

      reconsider c as Element of TarskiEuclid2Space by MM;

      

       V1: X c= ( LSeg (( Tn2TR a),( Tn2TR c)))

      proof

        let x be object;

        assume

         DA: x in X;

        then

        reconsider x1 = x as Element of TarskiEuclid2Space ;

        ( Tn2TR x1) in ( LSeg (( Tn2TR a),( Tn2TR c))) by ThConv6, A1, DA, MM;

        hence x in ( LSeg (( Tn2TR a),( Tn2TR c)));

      end;

      

       t2: ( LSeg (( Tn2TR a),( Tn2TR c))) c= ( Line (( Tn2TR a),( Tn2TR c))) by RLTOPSP1: 73;

      then

       T1: X c= ( Line (( Tn2TR a),( Tn2TR c))) by V1;

      

       T2: x0 in ( Line (( Tn2TR a),( Tn2TR c))) by t2, V1, K1;

      Y c= ( Line (( Tn2TR a),( Tn2TR c)))

      proof

        let y be object;

        assume

         V2: y in Y;

        then

        reconsider y0 = y as Element of TarskiEuclid2Space ;

        per cases ;

          suppose

           MU: x0 = a;

          per cases ;

            suppose X is trivial;

            then

            consider xx be object such that

             KL: X = {xx} by A1A, ZFMISC_1: 131;

            thus thesis by MU, K1, KL, TARSKI:def 1, A3;

          end;

            suppose X is non trivial;

            then

            consider a0,b0 be object such that

             LO1: a0 in X and

             LO2: b0 in X and

             LO3: a0 <> b0;

            ex x1 be object st x1 in X & x1 <> a

            proof

              assume

               AA: for x1 be object holds not x1 in X or x1 = a;

              a0 <> a or b0 <> a by LO3;

              hence contradiction by LO1, LO2, AA;

            end;

            then

            consider x1 be object such that

             K1: x1 in X and

             VAL: x1 <> a;

            reconsider x1 as Element of TarskiEuclid2Space by K1;

            

             N1: ( Tn2TR x1) in ( LSeg (( Tn2TR a),( Tn2TR y0))) by ThConv6, V2, K1, A1;

            

             n2: ( LSeg (( Tn2TR a),( Tn2TR y0))) c= ( Line (( Tn2TR a),( Tn2TR y0))) by RLTOPSP1: 73;

            ( Tn2TR a) in ( Line (( Tn2TR a),( Tn2TR y0))) by RLTOPSP1: 72;

            then

             ff: ( Line (( Tn2TR x1),( Tn2TR a))) = ( Line (( Tn2TR a),( Tn2TR y0))) by N1, n2, VAL, RLTOPSP1: 75;

            ( Tn2TR a) in ( Line (( Tn2TR a),( Tn2TR c))) by RLTOPSP1: 72;

            then ( Line (( Tn2TR a),( Tn2TR x1))) c= ( Line (( Tn2TR a),( Tn2TR c))) by K1, T1, RLTOPSP1: 74;

            hence thesis by ff, RLTOPSP1: 72;

          end;

        end;

          suppose

           VAL: x0 <> a;

          

           N1: ( Tn2TR x0) in ( LSeg (( Tn2TR a),( Tn2TR y0))) by ThConv6, V2, K1, A1;

          

           n2: ( LSeg (( Tn2TR a),( Tn2TR y0))) c= ( Line (( Tn2TR a),( Tn2TR y0))) by RLTOPSP1: 73;

          ( Tn2TR a) in ( Line (( Tn2TR a),( Tn2TR y0))) by RLTOPSP1: 72;

          then

           ff: ( Line (( Tn2TR x0),( Tn2TR a))) = ( Line (( Tn2TR a),( Tn2TR y0))) by N1, n2, VAL, RLTOPSP1: 75;

          ( Tn2TR a) in ( Line (( Tn2TR a),( Tn2TR c))) by RLTOPSP1: 72;

          then ( Line (( Tn2TR a),( Tn2TR x0))) c= ( Line (( Tn2TR a),( Tn2TR c))) by T2, RLTOPSP1: 74;

          hence thesis by ff, RLTOPSP1: 72;

        end;

      end;

      hence thesis by T1;

    end;