euclid_4.miz



    begin

    reserve a,b,s,t,u,lambda for Real,

n for Nat;

    reserve x,x1,x2,x3,y1,y2 for Element of ( REAL n);

    theorem :: EUCLID_4:1

    

     Th1: (( 0 * x) + x) = x & (x + ( 0* n)) = x

    proof

      reconsider x9 = x as Element of (n -tuples_on REAL );

      (( 0 * x) + x) = (( 0 * x9) + (1 * x9)) by RVSUM_1: 52

      .= (( 0 + 1) * x9) by RVSUM_1: 50

      .= x by RVSUM_1: 52;

      hence thesis by RVSUM_1: 16;

    end;

    theorem :: EUCLID_4:2

    

     Th2: (a * ( 0* n)) = ( 0* n)

    proof

       |.(a * ( 0* n)).| = ( |.a.| * |.( 0* n).|) by EUCLID: 11

      .= ( |.a.| * 0 ) by EUCLID: 7

      .= 0 ;

      hence thesis by EUCLID: 8;

    end;

    theorem :: EUCLID_4:3

    

     Th3: (1 * x) = x & ( 0 * x) = ( 0* n)

    proof

      reconsider x9 = x as Element of (n -tuples_on REAL );

      ( 0 * x) = ((( 0 * x9) + x9) - x9) by RVSUM_1: 42

      .= (x9 - x9) by Th1

      .= ( 0* n) by RVSUM_1: 37;

      hence thesis by RVSUM_1: 52;

    end;

    theorem :: EUCLID_4:4

    ((a * b) * x) = (a * (b * x)) by RVSUM_1: 49;

    theorem :: EUCLID_4:5

    (a * x) = ( 0* n) implies a = 0 or x = ( 0* n)

    proof

      assume that

       A1: (a * x) = ( 0* n) and

       A2: a <> 0 ;

      

      thus x = (1 * x) by Th3

      .= (((1 / a) * a) * x) by A2, XCMPLX_1: 106

      .= ((1 / a) * (a * x)) by RVSUM_1: 49

      .= ( 0* n) by A1, Th2;

    end;

    theorem :: EUCLID_4:6

    (a * (x1 + x2)) = ((a * x1) + (a * x2)) by RVSUM_1: 51;

    theorem :: EUCLID_4:7

    ((a + b) * x) = ((a * x) + (b * x)) by RVSUM_1: 50;

    theorem :: EUCLID_4:8

    (a * x1) = (a * x2) implies a = 0 or x1 = x2

    proof

      assume that

       A1: (a * x1) = (a * x2) and

       A2: a <> 0 ;

      (((1 / a) * a) * x1) = ((1 / a) * (a * x2)) by A1, RVSUM_1: 49;

      then (((1 / a) * a) * x1) = (((1 / a) * a) * x2) by RVSUM_1: 49;

      then (1 * x1) = (((1 / a) * a) * x2) by A2, XCMPLX_1: 106;

      then (1 * x1) = (1 * x2) by A2, XCMPLX_1: 106;

      

      hence x1 = (1 * x2) by Th3

      .= x2 by Th3;

    end;

    definition

      let n;

      let x1,x2 be Element of ( REAL n);

      :: EUCLID_4:def1

      func Line (x1,x2) -> Subset of ( REAL n) equals the set of all (((1 - lambda) * x1) + (lambda * x2));

      coherence

      proof

        set A = the set of all (((1 - lambda) * x1) + (lambda * x2));

        A c= ( REAL n)

        proof

          let x be object;

          assume x in A;

          then ex lambda st x = (((1 - lambda) * x1) + (lambda * x2));

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let n;

      let x1,x2 be Element of ( REAL n);

      cluster ( Line (x1,x2)) -> non empty;

      coherence

      proof

        

         A1: (1 - 0 ) = 1 & (1 * x1) = x1 by Th3;

        ( 0 * x2) = ( 0* n) & (x1 + ( 0* n)) = x1 by Th1, Th3;

        then x1 in ( Line (x1,x2)) by A1;

        hence thesis;

      end;

    end

    

     Lm1: ( Line (x1,x2)) c= ( Line (x2,x1))

    proof

      let z be object;

      assume z in ( Line (x1,x2));

      then

      consider t such that

       A1: z = (((1 - t) * x1) + (t * x2));

      z = (((1 - (1 - t)) * x2) + ((1 - t) * x1)) by A1;

      hence thesis;

    end;

    definition

      let n;

      let x1,x2 be Element of ( REAL n);

      :: original: Line

      redefine

      func Line (x1,x2);

      commutativity by Lm1;

    end

    theorem :: EUCLID_4:9

    

     Th9: x1 in ( Line (x1,x2)) & x2 in ( Line (x1,x2))

    proof

      

       A1: (1 - 0 ) = 1 & (1 * x1) = x1 by Th3;

      

       A2: (1 - 1) = 0 & ( 0 * x1) = ( 0* n) by Th3;

      

       A3: (1 * x2) = x2 & (( 0* n) + x2) = x2 by Th1, Th3;

      ( 0 * x2) = ( 0* n) & (x1 + ( 0* n)) = x1 by Th1, Th3;

      hence thesis by A1, A2, A3;

    end;

    

     Lm2: (x1 + (x2 + x3)) = ((x1 + x2) + x3) by FINSEQOP: 28;

    theorem :: EUCLID_4:10

    

     Th10: y1 in ( Line (x1,x2)) & y2 in ( Line (x1,x2)) implies ( Line (y1,y2)) c= ( Line (x1,x2))

    proof

      assume y1 in ( Line (x1,x2));

      then

      consider t such that

       A1: y1 = (((1 - t) * x1) + (t * x2));

      assume y2 in ( Line (x1,x2));

      then

      consider s such that

       A2: y2 = (((1 - s) * x1) + (s * x2));

      let z be object;

      assume z in ( Line (y1,y2));

      then

      consider u such that

       A3: z = (((1 - u) * y1) + (u * y2));

      z = ((((1 - u) * ((1 - t) * x1)) + ((1 - u) * (t * x2))) + (u * (((1 - s) * x1) + (s * x2)))) by A1, A2, A3, RVSUM_1: 51

      .= ((((1 - u) * ((1 - t) * x1)) + ((1 - u) * (t * x2))) + ((u * ((1 - s) * x1)) + (u * (s * x2)))) by RVSUM_1: 51

      .= (((((1 - u) * (1 - t)) * x1) + ((1 - u) * (t * x2))) + ((u * ((1 - s) * x1)) + (u * (s * x2)))) by RVSUM_1: 49

      .= (((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + ((u * ((1 - s) * x1)) + (u * (s * x2)))) by RVSUM_1: 49

      .= (((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + (((u * (1 - s)) * x1) + (u * (s * x2)))) by RVSUM_1: 49

      .= (((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + (((u * (1 - s)) * x1) + ((u * s) * x2))) by RVSUM_1: 49

      .= ((((1 - u) * (1 - t)) * x1) + ((((1 - u) * t) * x2) + (((u * (1 - s)) * x1) + ((u * s) * x2)))) by FINSEQOP: 28

      .= ((((1 - u) * (1 - t)) * x1) + (((u * (1 - s)) * x1) + ((((1 - u) * t) * x2) + ((u * s) * x2)))) by Lm2

      .= (((((1 - u) * (1 - t)) * x1) + ((u * (1 - s)) * x1)) + ((((1 - u) * t) * x2) + ((u * s) * x2))) by FINSEQOP: 28

      .= (((((1 - u) * (1 - t)) + (u * (1 - s))) * x1) + ((((1 - u) * t) * x2) + ((u * s) * x2))) by RVSUM_1: 50

      .= (((1 - (((1 * t) - (u * t)) + (u * s))) * x1) + ((((1 * t) - (u * t)) + (u * s)) * x2)) by RVSUM_1: 50;

      hence z in ( Line (x1,x2));

    end;

    theorem :: EUCLID_4:11

    

     Th11: y1 in ( Line (x1,x2)) & y2 in ( Line (x1,x2)) & y1 <> y2 implies ( Line (x1,x2)) c= ( Line (y1,y2))

    proof

      assume y1 in ( Line (x1,x2));

      then

      consider t such that

       A1: y1 = (((1 - t) * x1) + (t * x2));

      assume y2 in ( Line (x1,x2));

      then

      consider s such that

       A2: y2 = (((1 - s) * x1) + (s * x2));

      assume y1 <> y2;

      then

       A3: (t - s) <> 0 by A1, A2;

      

      then (((1 - ((t - 1) / (t - s))) * y1) + (((t - 1) / (t - s)) * y2)) = (((((1 * (t - s)) - (t - 1)) / (t - s)) * y1) + (((t - 1) / (t - s)) * y2)) by XCMPLX_1: 127

      .= (((((( - s) + 1) / (t - s)) * ((1 - t) * x1)) + (((( - s) + 1) / (t - s)) * (t * x2))) + (((t - 1) / (t - s)) * (((1 - s) * x1) + (s * x2)))) by A1, A2, RVSUM_1: 51

      .= (((((( - s) + 1) / (t - s)) * ((1 - t) * x1)) + (((( - s) + 1) / (t - s)) * (t * x2))) + ((((t - 1) / (t - s)) * ((1 - s) * x1)) + (((t - 1) / (t - s)) * (s * x2)))) by RVSUM_1: 51

      .= ((((((( - s) + 1) / (t - s)) * (1 - t)) * x1) + (((( - s) + 1) / (t - s)) * (t * x2))) + ((((t - 1) / (t - s)) * ((1 - s) * x1)) + (((t - 1) / (t - s)) * (s * x2)))) by RVSUM_1: 49

      .= ((((((( - s) + 1) / (t - s)) * (1 - t)) * x1) + ((((( - s) + 1) / (t - s)) * t) * x2)) + ((((t - 1) / (t - s)) * ((1 - s) * x1)) + (((t - 1) / (t - s)) * (s * x2)))) by RVSUM_1: 49

      .= ((((((( - s) + 1) / (t - s)) * (1 - t)) * x1) + ((((( - s) + 1) / (t - s)) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + (((t - 1) / (t - s)) * (s * x2)))) by RVSUM_1: 49

      .= ((((((( - s) + 1) / (t - s)) * (1 - t)) * x1) + ((((( - s) + 1) / (t - s)) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2))) by RVSUM_1: 49

      .= ((((((( - s) + 1) * (1 / (t - s))) * (1 - t)) * x1) + ((((( - s) + 1) / (t - s)) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2))) by XCMPLX_1: 99

      .= ((((((( - s) + 1) * (1 - t)) * (1 / (t - s))) * x1) + ((((( - s) + 1) / (t - s)) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2)))

      .= ((((((( - s) + 1) * (1 - t)) / (t - s)) * x1) + ((((( - s) + 1) / (t - s)) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2))) by XCMPLX_1: 99

      .= ((((((( - s) + 1) * (1 - t)) / (t - s)) * x1) + ((((( - s) + 1) * (1 / (t - s))) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2))) by XCMPLX_1: 99

      .= ((((((( - s) + 1) * (1 - t)) / (t - s)) * x1) + ((((( - s) + 1) * t) * (1 / (t - s))) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2)))

      .= ((((((( - s) + 1) * (1 - t)) / (t - s)) * x1) + ((((( - s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2))) by XCMPLX_1: 99

      .= ((((((( - s) + 1) * (1 - t)) / (t - s)) * x1) + ((((( - s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) * (1 / (t - s))) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2))) by XCMPLX_1: 99

      .= ((((((( - s) + 1) * (1 - t)) / (t - s)) * x1) + ((((( - s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) * (1 - s)) * (1 / (t - s))) * x1) + ((((t - 1) / (t - s)) * s) * x2)))

      .= ((((((( - s) + 1) * (1 - t)) / (t - s)) * x1) + ((((( - s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2))) by XCMPLX_1: 99

      .= ((((((( - s) + 1) * (1 - t)) / (t - s)) * x1) + ((((( - s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + ((((t - 1) * (1 / (t - s))) * s) * x2))) by XCMPLX_1: 99

      .= ((((((( - s) + 1) * (1 - t)) / (t - s)) * x1) + ((((( - s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + ((((t - 1) * s) * (1 / (t - s))) * x2)))

      .= ((((((( - s) + 1) * (1 - t)) / (t - s)) * x1) + ((((( - s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + ((((t - 1) * s) / (t - s)) * x2))) by XCMPLX_1: 99

      .= (((((( - s) + 1) * (1 - t)) / (t - s)) * x1) + (((((( - s) + 1) * t) / (t - s)) * x2) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + ((((t - 1) * s) / (t - s)) * x2)))) by FINSEQOP: 28

      .= (((((( - s) + 1) * (1 - t)) / (t - s)) * x1) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + (((((( - s) + 1) * t) / (t - s)) * x2) + ((((t - 1) * s) / (t - s)) * x2)))) by Lm2

      .= ((((((( - s) + 1) * (1 - t)) / (t - s)) * x1) + ((((t - 1) * (1 - s)) / (t - s)) * x1)) + (((((( - s) + 1) * t) / (t - s)) * x2) + ((((t - 1) * s) / (t - s)) * x2))) by FINSEQOP: 28

      .= ((((((( - s) + 1) * (1 - t)) / (t - s)) + (((t - 1) * (1 - s)) / (t - s))) * x1) + (((((( - s) + 1) * t) / (t - s)) * x2) + ((((t - 1) * s) / (t - s)) * x2))) by RVSUM_1: 50

      .= ((((((( - s) + 1) * (1 - t)) / (t - s)) + (((t - 1) * (1 - s)) / (t - s))) * x1) + (((((( - s) + 1) * t) / (t - s)) + (((t - 1) * s) / (t - s))) * x2)) by RVSUM_1: 50

      .= ((((((( - s) + 1) * (1 - t)) + ((t - 1) * (1 - s))) / (t - s)) * x1) + (((((( - s) + 1) * t) / (t - s)) + (((t - 1) * s) / (t - s))) * x2)) by XCMPLX_1: 62

      .= ((((((1 - t) * (1 - s)) + ( - ((1 - t) * (1 - s)))) / (t - s)) * x1) + (((((( - s) + 1) * t) + ((t - 1) * s)) / (t - s)) * x2)) by XCMPLX_1: 62

      .= (( 0* n) + (((((( - s) + 1) * t) + ((t - 1) * s)) / (t - s)) * x2)) by Th3

      .= (((1 * (t - s)) / (t - s)) * x2) by Th1

      .= (1 * x2) by A3, XCMPLX_1: 89

      .= x2 by Th3;

      then

       A4: x2 in ( Line (y1,y2));

      (((1 - (t / (t - s))) * y1) + ((t / (t - s)) * y2)) = (((((1 * (t - s)) - t) / (t - s)) * y1) + ((t / (t - s)) * y2)) by A3, XCMPLX_1: 127

      .= ((((( - s) / (t - s)) * ((1 - t) * x1)) + ((( - s) / (t - s)) * (t * x2))) + ((t / (t - s)) * (((1 - s) * x1) + (s * x2)))) by A1, A2, RVSUM_1: 51

      .= ((((( - s) / (t - s)) * ((1 - t) * x1)) + ((( - s) / (t - s)) * (t * x2))) + (((t / (t - s)) * ((1 - s) * x1)) + ((t / (t - s)) * (s * x2)))) by RVSUM_1: 51

      .= (((((( - s) / (t - s)) * (1 - t)) * x1) + ((( - s) / (t - s)) * (t * x2))) + (((t / (t - s)) * ((1 - s) * x1)) + ((t / (t - s)) * (s * x2)))) by RVSUM_1: 49

      .= (((((( - s) / (t - s)) * (1 - t)) * x1) + (((( - s) / (t - s)) * t) * x2)) + (((t / (t - s)) * ((1 - s) * x1)) + ((t / (t - s)) * (s * x2)))) by RVSUM_1: 49

      .= (((((( - s) / (t - s)) * (1 - t)) * x1) + (((( - s) / (t - s)) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + ((t / (t - s)) * (s * x2)))) by RVSUM_1: 49

      .= (((((( - s) / (t - s)) * (1 - t)) * x1) + (((( - s) / (t - s)) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2))) by RVSUM_1: 49

      .= (((((( - s) * (1 / (t - s))) * (1 - t)) * x1) + (((( - s) / (t - s)) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2))) by XCMPLX_1: 99

      .= (((((( - s) * (1 - t)) * (1 / (t - s))) * x1) + (((( - s) / (t - s)) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2)))

      .= (((((( - s) * (1 - t)) / (t - s)) * x1) + (((( - s) / (t - s)) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2))) by XCMPLX_1: 99

      .= (((((( - s) * (1 - t)) / (t - s)) * x1) + (((( - s) * (1 / (t - s))) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2))) by XCMPLX_1: 99

      .= (((((( - s) * (1 - t)) / (t - s)) * x1) + (((( - s) * t) * (1 / (t - s))) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2)))

      .= (((((( - s) * (1 - t)) / (t - s)) * x1) + (((( - s) * t) / (t - s)) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2))) by XCMPLX_1: 99

      .= (((((( - s) * (1 - t)) / (t - s)) * x1) + (((( - s) * t) / (t - s)) * x2)) + ((((t * (1 / (t - s))) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2))) by XCMPLX_1: 99

      .= (((((( - s) * (1 - t)) / (t - s)) * x1) + (((( - s) * t) / (t - s)) * x2)) + ((((t * (1 - s)) * (1 / (t - s))) * x1) + (((t / (t - s)) * s) * x2)))

      .= (((((( - s) * (1 - t)) / (t - s)) * x1) + (((( - s) * t) / (t - s)) * x2)) + ((((t * (1 - s)) / (t - s)) * x1) + (((t / (t - s)) * s) * x2))) by XCMPLX_1: 99

      .= (((((( - s) * (1 - t)) / (t - s)) * x1) + (((( - s) * t) / (t - s)) * x2)) + ((((t * (1 - s)) / (t - s)) * x1) + (((t * (1 / (t - s))) * s) * x2))) by XCMPLX_1: 99

      .= (((((( - s) * (1 - t)) / (t - s)) * x1) + (((( - s) * t) / (t - s)) * x2)) + ((((t * (1 - s)) / (t - s)) * x1) + (((t * s) * (1 / (t - s))) * x2)))

      .= (((((( - s) * (1 - t)) / (t - s)) * x1) + (((( - s) * t) / (t - s)) * x2)) + ((((t * (1 - s)) / (t - s)) * x1) + (((t * s) / (t - s)) * x2))) by XCMPLX_1: 99

      .= ((((( - s) * (1 - t)) / (t - s)) * x1) + ((((( - s) * t) / (t - s)) * x2) + ((((t * (1 - s)) / (t - s)) * x1) + (((t * s) / (t - s)) * x2)))) by FINSEQOP: 28

      .= ((((( - s) * (1 - t)) / (t - s)) * x1) + ((((t * (1 - s)) / (t - s)) * x1) + ((((( - s) * t) / (t - s)) * x2) + (((t * s) / (t - s)) * x2)))) by Lm2

      .= (((((( - s) * (1 - t)) / (t - s)) * x1) + (((t * (1 - s)) / (t - s)) * x1)) + ((((( - s) * t) / (t - s)) * x2) + (((t * s) / (t - s)) * x2))) by FINSEQOP: 28

      .= (((((( - s) * (1 - t)) / (t - s)) + ((t * (1 - s)) / (t - s))) * x1) + ((((( - s) * t) / (t - s)) * x2) + (((t * s) / (t - s)) * x2))) by RVSUM_1: 50

      .= (((((( - s) * (1 - t)) / (t - s)) + ((t * (1 - s)) / (t - s))) * x1) + ((((( - s) * t) / (t - s)) + ((t * s) / (t - s))) * x2)) by RVSUM_1: 50

      .= (((((( - s) * (1 - t)) + (t * (1 - s))) / (t - s)) * x1) + ((((( - s) * t) / (t - s)) + ((t * s) / (t - s))) * x2)) by XCMPLX_1: 62

      .= (((((( - s) * (1 - t)) + (t * (1 - s))) / (t - s)) * x1) + ((((( - s) * t) + (t * s)) / (t - s)) * x2)) by XCMPLX_1: 62

      .= (((((( - s) * (1 - t)) + (t * (1 - s))) / (t - s)) * x1) + ( 0* n)) by Th3

      .= (((1 * (t - s)) / (t - s)) * x1) by Th1

      .= (1 * x1) by A3, XCMPLX_1: 89

      .= x1 by Th3;

      then x1 in ( Line (y1,y2));

      hence thesis by A4, Th10;

    end;

    definition

      let n;

      let A be Subset of ( REAL n);

      :: EUCLID_4:def2

      attr A is being_line means ex x1, x2 st x1 <> x2 & A = ( Line (x1,x2));

    end

    

     Lm3: for A be Subset of ( REAL n), x1, x2 holds A is being_line & x1 in A & x2 in A & x1 <> x2 implies A = ( Line (x1,x2)) by Th10, Th11;

    theorem :: EUCLID_4:12

    for A,C be Subset of ( REAL n), x1, x2 holds A is being_line & C is being_line & x1 in A & x2 in A & x1 in C & x2 in C implies x1 = x2 or A = C

    proof

      let A,C be Subset of ( REAL n);

      let x1, x2;

      assume that

       A1: A is being_line and

       A2: C is being_line and

       A3: x1 in A & x2 in A and

       A4: x1 in C & x2 in C;

      assume

       A5: x1 <> x2;

      then A = ( Line (x1,x2)) by A1, A3, Lm3;

      hence thesis by A2, A4, A5, Lm3;

    end;

    theorem :: EUCLID_4:13

    

     Th13: for A be Subset of ( REAL n) st A is being_line holds ex x1, x2 st x1 in A & x2 in A & x1 <> x2

    proof

      let A be Subset of ( REAL n);

      assume A is being_line;

      then

      consider x1, x2 such that

       A1: x1 <> x2 and

       A2: A = ( Line (x1,x2));

      x1 in A & x2 in A by A2, Th9;

      hence thesis by A1;

    end;

    theorem :: EUCLID_4:14

    for A be Subset of ( REAL n) st A is being_line holds ex x2 st x1 <> x2 & x2 in A

    proof

      let A be Subset of ( REAL n);

      assume A is being_line;

      then

      consider y1, y2 such that

       A1: y1 in A and

       A2: y2 in A & y1 <> y2 by Th13;

      x1 = y1 implies x1 <> y2 & y2 in A by A2;

      hence thesis by A1;

    end;

    theorem :: EUCLID_4:15

    for x be Element of ( REAL n) holds |.x.| = ( sqrt |(x, x)|);

    theorem :: EUCLID_4:16

    

     Th16: for x be Element of ( REAL n) holds |(x, x)| = 0 iff |.x.| = 0

    proof

      let x be Element of ( REAL n);

      thus |(x, x)| = 0 implies |.x.| = 0

      proof

        assume |(x, x)| = 0 ;

        then ( |.x.| ^2 ) = 0 by EUCLID_2: 4;

        hence thesis by XCMPLX_1: 6;

      end;

       |.x.| = 0 implies |(x, x)| = ( 0 ^2 ) by EUCLID_2: 4;

      hence thesis;

    end;

    theorem :: EUCLID_4:17

    

     Th17: for x be Element of ( REAL n) holds |(x, x)| = 0 iff x = ( 0* n)

    proof

      let x be Element of ( REAL n);

      thus |(x, x)| = 0 implies x = ( 0* n)

      proof

        assume |(x, x)| = 0 ;

        then |.x.| = 0 by Th16;

        hence thesis by EUCLID: 8;

      end;

      thus x = ( 0* n) implies |(x, x)| = 0

      proof

        assume x = ( 0* n);

        

        then |(x, x)| = ((1 / 4) * (( |.(( 0* n) + ( 0* n)).| ^2 ) - ( |.(( 0* n) - ( 0* n)).| ^2 ))) by EUCLID_2: 3

        .= ((1 / 4) * (( |.( 0* n).| ^2 ) - ( |.(( 0* n) - ( 0* n)).| ^2 ))) by Th1

        .= ((1 / 4) * 0 ) by RVSUM_1: 32;

        hence thesis;

      end;

    end;

    theorem :: EUCLID_4:18

    

     Th18: for x be Element of ( REAL n) holds |(x, ( 0* n))| = 0

    proof

      let x be Element of ( REAL n);

       |(x, ( 0* n))| = ((1 / 4) * (( |.(x + ( 0* n)).| ^2 ) - ( |.(x - ( 0* n)).| ^2 ))) by EUCLID_2: 3

      .= ((1 / 4) * (( |.x.| ^2 ) - ( |.(x - ( 0* n)).| ^2 ))) by Th1

      .= ((1 / 4) * (( |.x.| ^2 ) - ( |.x.| ^2 ))) by RVSUM_1: 32

      .= ((1 / 4) * 0 );

      hence thesis;

    end;

    theorem :: EUCLID_4:19

    for x be Element of ( REAL n) holds |(( 0* n), x)| = 0 by Th18;

    theorem :: EUCLID_4:20

    

     Th20: for x1,x2,x3 be Element of ( REAL n) holds |((x1 + x2), x3)| = ( |(x1, x3)| + |(x2, x3)|)

    proof

      let x1,x2,x3 be Element of ( REAL n);

      

       A1: ( len x3) = n by CARD_1:def 7;

      ( len x1) = n & ( len x2) = n by CARD_1:def 7;

      hence thesis by A1, RVSUM_1: 120;

    end;

    theorem :: EUCLID_4:21

    

     Th21: for x1,x2 be Element of ( REAL n), a be Real holds |((a * x1), x2)| = (a * |(x1, x2)|)

    proof

      let x1,x2 be Element of ( REAL n), a be Real;

      ( len x1) = n & ( len x2) = n by CARD_1:def 7;

      hence thesis by RVSUM_1: 121;

    end;

    theorem :: EUCLID_4:22

    for x1,x2 be Element of ( REAL n), a be Real holds |(x1, (a * x2))| = (a * |(x1, x2)|) by Th21;

    theorem :: EUCLID_4:23

    

     Th23: for x1,x2 be Element of ( REAL n) holds |(( - x1), x2)| = ( - |(x1, x2)|)

    proof

      let x1,x2 be Element of ( REAL n);

      ( len x1) = n & ( len x2) = n by CARD_1:def 7;

      hence thesis by RVSUM_1: 122;

    end;

    theorem :: EUCLID_4:24

    for x1,x2 be Element of ( REAL n) holds |(x1, ( - x2))| = ( - |(x1, x2)|) by Th23;

    theorem :: EUCLID_4:25

    for x1,x2 be Element of ( REAL n) holds |(( - x1), ( - x2))| = |(x1, x2)|

    proof

      let x1,x2 be Element of ( REAL n);

      

      thus |(( - x1), ( - x2))| = ( - |(x1, ( - x2))|) by Th23

      .= (( - 1) * |(x1, ( - x2))|)

      .= (( - 1) * ( - |(x1, x2)|)) by Th23

      .= |(x1, x2)|;

    end;

    theorem :: EUCLID_4:26

    

     Th26: for x1,x2,x3 be Element of ( REAL n) holds |((x1 - x2), x3)| = ( |(x1, x3)| - |(x2, x3)|)

    proof

      let x1,x2,x3 be Element of ( REAL n);

      

       A1: ( len x3) = n by CARD_1:def 7;

      ( len x1) = n & ( len x2) = n by CARD_1:def 7;

      hence thesis by A1, RVSUM_1: 124;

    end;

    theorem :: EUCLID_4:27

    for a,b be Real, x1,x2,x3 be Element of ( REAL n) holds |(((a * x1) + (b * x2)), x3)| = ((a * |(x1, x3)|) + (b * |(x2, x3)|))

    proof

      let a,b be Real, x1,x2,x3 be Element of ( REAL n);

      

      thus |(((a * x1) + (b * x2)), x3)| = ( |((a * x1), x3)| + |((b * x2), x3)|) by Th20

      .= ((a * |(x1, x3)|) + |((b * x2), x3)|) by Th21

      .= ((a * |(x1, x3)|) + (b * |(x2, x3)|)) by Th21;

    end;

    theorem :: EUCLID_4:28

    for x1,y1,y2 be Element of ( REAL n) holds |(x1, (y1 + y2))| = ( |(x1, y1)| + |(x1, y2)|) by Th20;

    theorem :: EUCLID_4:29

    for x1,y1,y2 be Element of ( REAL n) holds |(x1, (y1 - y2))| = ( |(x1, y1)| - |(x1, y2)|) by Th26;

    theorem :: EUCLID_4:30

    

     Th30: for x1,x2,y1,y2 be Element of ( REAL n) holds |((x1 + x2), (y1 + y2))| = ((( |(x1, y1)| + |(x1, y2)|) + |(x2, y1)|) + |(x2, y2)|)

    proof

      let x1,x2,y1,y2 be Element of ( REAL n);

      

      thus |((x1 + x2), (y1 + y2))| = ( |(x1, (y1 + y2))| + |(x2, (y1 + y2))|) by Th20

      .= (( |(x1, y1)| + |(x1, y2)|) + |(x2, (y1 + y2))|) by Th20

      .= (( |(x1, y1)| + |(x1, y2)|) + ( |(x2, y1)| + |(x2, y2)|)) by Th20

      .= ((( |(x1, y1)| + |(x1, y2)|) + |(x2, y1)|) + |(x2, y2)|);

    end;

    theorem :: EUCLID_4:31

    

     Th31: for x1,x2,y1,y2 be Element of ( REAL n) holds |((x1 - x2), (y1 - y2))| = ((( |(x1, y1)| - |(x1, y2)|) - |(x2, y1)|) + |(x2, y2)|)

    proof

      let x1,x2,y1,y2 be Element of ( REAL n);

      

      thus |((x1 - x2), (y1 - y2))| = ( |(x1, (y1 - y2))| - |(x2, (y1 - y2))|) by Th26

      .= (( |(x1, y1)| - |(x1, y2)|) - |(x2, (y1 - y2))|) by Th26

      .= (( |(x1, y1)| - |(x1, y2)|) - ( |(x2, y1)| - |(x2, y2)|)) by Th26

      .= ((( |(x1, y1)| - |(x1, y2)|) - |(x2, y1)|) + |(x2, y2)|);

    end;

    theorem :: EUCLID_4:32

    

     Th32: for x,y be Element of ( REAL n) holds |((x + y), (x + y))| = (( |(x, x)| + (2 * |(x, y)|)) + |(y, y)|)

    proof

      let x,y be Element of ( REAL n);

      

      thus |((x + y), (x + y))| = ((( |(x, x)| + |(x, y)|) + |(y, x)|) + |(y, y)|) by Th30

      .= (( |(x, x)| + (2 * |(x, y)|)) + |(y, y)|);

    end;

    theorem :: EUCLID_4:33

    

     Th33: for x,y be Element of ( REAL n) holds |((x - y), (x - y))| = (( |(x, x)| - (2 * |(x, y)|)) + |(y, y)|)

    proof

      let x,y be Element of ( REAL n);

      

      thus |((x - y), (x - y))| = ((( |(x, x)| - |(x, y)|) - |(y, x)|) + |(y, y)|) by Th31

      .= (( |(x, x)| - (2 * |(x, y)|)) + |(y, y)|);

    end;

    theorem :: EUCLID_4:34

    for x,y be Element of ( REAL n) holds ( |.(x + y).| ^2 ) = ((( |.x.| ^2 ) + (2 * |(x, y)|)) + ( |.y.| ^2 ))

    proof

      let x,y be Element of ( REAL n);

      

      thus ( |.(x + y).| ^2 ) = |((x + y), (x + y))| by EUCLID_2: 4

      .= (( |(x, x)| + (2 * |(x, y)|)) + |(y, y)|) by Th32

      .= ((( |.x.| ^2 ) + (2 * |(x, y)|)) + |(y, y)|) by EUCLID_2: 4

      .= ((( |.x.| ^2 ) + (2 * |(x, y)|)) + ( |.y.| ^2 )) by EUCLID_2: 4;

    end;

    theorem :: EUCLID_4:35

    for x,y be Element of ( REAL n) holds ( |.(x - y).| ^2 ) = ((( |.x.| ^2 ) - (2 * |(x, y)|)) + ( |.y.| ^2 ))

    proof

      let x,y be Element of ( REAL n);

      

      thus ( |.(x - y).| ^2 ) = |((x - y), (x - y))| by EUCLID_2: 4

      .= (( |(x, x)| - (2 * |(x, y)|)) + |(y, y)|) by Th33

      .= ((( |.x.| ^2 ) - (2 * |(x, y)|)) + |(y, y)|) by EUCLID_2: 4

      .= ((( |.x.| ^2 ) - (2 * |(x, y)|)) + ( |.y.| ^2 )) by EUCLID_2: 4;

    end;

    theorem :: EUCLID_4:36

    for x,y be Element of ( REAL n) holds (( |.(x + y).| ^2 ) + ( |.(x - y).| ^2 )) = (2 * (( |.x.| ^2 ) + ( |.y.| ^2 )))

    proof

      let x,y be Element of ( REAL n);

      ( len x) = n & ( len y) = n by CARD_1:def 7;

      hence thesis by EUCLID_2: 13;

    end;

    theorem :: EUCLID_4:37

    for x,y be Element of ( REAL n) holds (( |.(x + y).| ^2 ) - ( |.(x - y).| ^2 )) = (4 * |(x, y)|)

    proof

      let x,y be Element of ( REAL n);

      ( len x) = n & ( len y) = n by CARD_1:def 7;

      hence thesis by EUCLID_2: 14;

    end;

    theorem :: EUCLID_4:38

    for x,y be Element of ( REAL n) holds |. |(x, y)|.| <= ( |.x.| * |.y.|)

    proof

      let x,y be Element of ( REAL n);

      ( len x) = n & ( len y) = n by CARD_1:def 7;

      hence thesis by EUCLID_2: 15;

    end;

    

     Lm4: ( - (a * x)) = (( - a) * x) & ( - (a * x)) = (a * ( - x))

    proof

      reconsider p = x as Point of ( TOP-REAL n) by EUCLID: 22;

      reconsider x9 = p as Element of (n -tuples_on REAL );

      

      thus ( - (a * x)) = ((( - 1) * a) * x9) by RVSUM_1: 49

      .= (( - a) * x);

      

      hence ( - (a * x)) = ((a * ( - 1)) * x)

      .= (a * ( - x)) by RVSUM_1: 49;

    end;

    

     Lm5: x1 <> x2 implies |.(x1 - x2).| <> 0

    proof

      now

        assume that

         A1: x1 <> x2 and

         A2: not |.(x1 - x2).| <> 0 ;

         |((x1 - x2), (x1 - x2))| = ( 0 ^2 ) by A2, EUCLID_2: 4;

        then (x1 - x2) = ( 0* n) by Th17;

        

        then x1 = (x1 - (x1 + ( - x2))) by RVSUM_1: 32

        .= ((x1 - x1) - ( - x2)) by RVSUM_1: 39

        .= (( 0* n) - ( - x2)) by RVSUM_1: 37

        .= x2 by RVSUM_1: 33;

        hence contradiction by A1;

      end;

      hence thesis;

    end;

    

     Lm6: for x1,x2 be Element of ( REAL n) holds y1 in ( Line (x1,x2)) & y2 in ( Line (x1,x2)) implies ex a st (y1 - y2) = (a * (x1 - x2))

    proof

      let x1,x2 be Element of ( REAL n);

      assume y1 in ( Line (x1,x2));

      then

      consider t such that

       A1: y1 = (((1 - t) * x1) + (t * x2));

      assume y2 in ( Line (x1,x2));

      then

      consider s such that

       A2: y2 = (((1 - s) * x1) + (s * x2));

      take (s - t);

      (y1 - y2) = (((((1 - t) * x1) + (t * x2)) - ((1 - s) * x1)) - (s * x2)) by A1, A2, RVSUM_1: 39

      .= (((((1 - t) * x1) + ( - ((1 - s) * x1))) + (t * x2)) + ( - (s * x2))) by Lm2

      .= ((((1 - t) * x1) + ( - ((1 - s) * x1))) + ((t * x2) + ( - (s * x2)))) by FINSEQOP: 28

      .= ((((1 - t) * x1) + (( - (1 - s)) * x1)) + ((t * x2) + ( - (s * x2)))) by Lm4

      .= ((((1 - t) * x1) + (( - (1 - s)) * x1)) + ((t * x2) + (( - s) * x2))) by Lm4

      .= ((((1 - t) + ( - (1 - s))) * x1) + ((t * x2) + (( - s) * x2))) by RVSUM_1: 50

      .= ((((1 - t) - (1 - s)) * x1) + ((t + ( - s)) * x2)) by RVSUM_1: 50

      .= (((s - t) * x1) + (( - (s + ( - t))) * x2))

      .= (((s - t) * x1) + ( - ((s - t) * x2))) by Lm4

      .= (((s - t) * x1) + ((s - t) * ( - x2))) by Lm4

      .= ((s - t) * (x1 - x2)) by RVSUM_1: 51;

      hence thesis;

    end;

    

     Lm7: for x1,x2,y1 be Element of ( REAL n) holds ex y2 be Element of ( REAL n) st y2 in ( Line (x1,x2)) & ((x1 - x2),(y1 - y2)) are_orthogonal & for x be Element of ( REAL n) st x in ( Line (x1,x2)) holds |.(y1 - y2).| <= |.(y1 - x).|

    proof

      let x1,x2,y1 be Element of ( REAL n);

      now

        per cases ;

          case

           A1: x1 <> x2;

          set mu = ( - ( |((x1 - x2), (y1 - x1))| / ( |.(x1 - x2).| ^2 )));

          set y2 = (((1 - mu) * x1) + (mu * x2));

           |.(x1 - x2).| <> 0 by A1, Lm5;

          then

           A2: ( |.(x1 - x2).| ^2 ) <> 0 by SQUARE_1: 12;

           |((x1 - x2), (y1 - y2))| = |((x1 - x2), ((y1 - ((1 + ( - mu)) * x1)) - (mu * x2)))| by RVSUM_1: 39

          .= |((x1 - x2), ((y1 - ((1 * x1) + (( - mu) * x1))) - (mu * x2)))| by RVSUM_1: 50

          .= |((x1 - x2), (((y1 - (1 * x1)) - (( - mu) * x1)) - (mu * x2)))| by RVSUM_1: 39

          .= |((x1 - x2), (((y1 - x1) - (( - mu) * x1)) - (mu * x2)))| by Th3

          .= |((x1 - x2), ((y1 - x1) - ((( - mu) * x1) + (mu * x2))))| by RVSUM_1: 39

          .= |((x1 - x2), ((y1 - x1) - ((( - mu) * x1) + ( - (( - mu) * x2)))))| by Lm4

          .= |((x1 - x2), ((y1 - x1) - ((( - mu) * x1) + (( - mu) * ( - x2)))))| by Lm4

          .= |((x1 - x2), ((y1 - x1) - (( - mu) * (x1 - x2))))| by RVSUM_1: 51

          .= ( |((x1 - x2), (y1 - x1))| - |((x1 - x2), (( - mu) * (x1 - x2)))|) by Th26

          .= ( |((x1 - x2), (y1 - x1))| - (( - mu) * |((x1 - x2), (x1 - x2))|)) by Th21

          .= ( |((x1 - x2), (y1 - x1))| + (mu * |((x1 - x2), (x1 - x2))|))

          .= ( |((x1 - x2), (y1 - x1))| + (mu * ( |.(x1 - x2).| ^2 ))) by EUCLID_2: 4

          .= ( |((x1 - x2), (y1 - x1))| + ((( - |((x1 - x2), (y1 - x1))|) / ( |.(x1 - x2).| ^2 )) * ( |.(x1 - x2).| ^2 ))) by XCMPLX_1: 187

          .= ( |((x1 - x2), (y1 - x1))| + ( - |((x1 - x2), (y1 - x1))|)) by A2, XCMPLX_1: 87

          .= 0 ;

          hence y2 in ( Line (x1,x2)) & ((x1 - x2),(y1 - y2)) are_orthogonal ;

        end;

          case

           A3: x1 = x2;

          let mu be Real;

          set y2 = (((1 - mu) * x1) + (mu * x2));

          take y2;

          (x1 - x2) = ( 0* n) by A3, RVSUM_1: 37;

          then |((x1 - x2), (y1 - y2))| = 0 by Th18;

          hence y2 in ( Line (x1,x2)) & ((x1 - x2),(y1 - y2)) are_orthogonal ;

        end;

      end;

      then

      consider y2 such that

       A4: y2 in ( Line (x1,x2)) and

       A5: ((x1 - x2),(y1 - y2)) are_orthogonal ;

      

       A6: |((x1 - x2), (y1 - y2))| = 0 by A5;

      for x be Element of ( REAL n) st x in ( Line (x1,x2)) holds |.(y1 - y2).| <= |.(y1 - x).|

      proof

        let x be Element of ( REAL n);

        assume x in ( Line (x1,x2));

        then

        consider a such that

         A7: (y2 - x) = (a * (x1 - x2)) by A4, Lm6;

        ((y2 - x) + (y1 - y2)) = (((( - x) + y2) + ( - y2)) + y1) by Lm2

        .= ((( - x) + (y2 - y2)) + y1) by FINSEQOP: 28

        .= ((( - x) + ( 0* n)) + y1) by RVSUM_1: 37

        .= (y1 - x) by Th1;

        

        then ( |.(y1 - x).| ^2 ) = |(((a * (x1 - x2)) + (y1 - y2)), ((a * (x1 - x2)) + (y1 - y2)))| by A7, EUCLID_2: 4

        .= (( |((a * (x1 - x2)), (a * (x1 - x2)))| + (2 * |((a * (x1 - x2)), (y1 - y2))|)) + |((y1 - y2), (y1 - y2))|) by Th32

        .= (((a * |((x1 - x2), (a * (x1 - x2)))|) + (2 * |((a * (x1 - x2)), (y1 - y2))|)) + |((y1 - y2), (y1 - y2))|) by Th21

        .= (((a * (a * |((x1 - x2), (x1 - x2))|)) + (2 * |((a * (x1 - x2)), (y1 - y2))|)) + |((y1 - y2), (y1 - y2))|) by Th21

        .= ((((a ^2 ) * |((x1 - x2), (x1 - x2))|) + (2 * |((a * (x1 - x2)), (y1 - y2))|)) + |((y1 - y2), (y1 - y2))|)

        .= ((((a ^2 ) * ( |.(x1 - x2).| ^2 )) + (2 * |((a * (x1 - x2)), (y1 - y2))|)) + |((y1 - y2), (y1 - y2))|) by EUCLID_2: 4

        .= ((((a ^2 ) * ( |.(x1 - x2).| ^2 )) + (2 * (a * |((x1 - x2), (y1 - y2))|))) + |((y1 - y2), (y1 - y2))|) by Th21

        .= (((a * |.(x1 - x2).|) ^2 ) + ( |.(y1 - y2).| ^2 )) by A6, EUCLID_2: 4;

        then 0 <= (( |.(y1 - x).| ^2 ) - ( |.(y1 - y2).| ^2 )) by XREAL_1: 63;

        then

         A8: ( |.(y1 - y2).| ^2 ) <= ( |.(y1 - x).| ^2 ) by XREAL_1: 49;

         0 <= ( |.(y1 - y2).| ^2 ) by XREAL_1: 63;

        then ( sqrt ( |.(y1 - y2).| ^2 )) <= ( sqrt ( |.(y1 - x).| ^2 )) by A8, SQUARE_1: 26;

        then |.(y1 - y2).| <= ( sqrt ( |.(y1 - x).| ^2 )) by EUCLID: 9, SQUARE_1: 22;

        hence thesis by EUCLID: 9, SQUARE_1: 22;

      end;

      hence thesis by A4, A5;

    end;

    ::$Canceled

    theorem :: EUCLID_4:40

    for R be Subset of REAL , x1,x2,y1 be Element of ( REAL n) st R = { |.(y1 - x).| where x be Element of ( REAL n) : x in ( Line (x1,x2)) } holds ex y2 be Element of ( REAL n) st y2 in ( Line (x1,x2)) & |.(y1 - y2).| = ( lower_bound R) & ((x1 - x2),(y1 - y2)) are_orthogonal

    proof

      let R be Subset of REAL , x1,x2,y1 be Element of ( REAL n);

      consider y2 be Element of ( REAL n) such that

       A1: y2 in ( Line (x1,x2)) and

       A2: ((x1 - x2),(y1 - y2)) are_orthogonal and

       A3: for x be Element of ( REAL n) st x in ( Line (x1,x2)) holds |.(y1 - y2).| <= |.(y1 - x).| by Lm7;

      assume

       A4: R = { |.(y1 - x).| where x be Element of ( REAL n) : x in ( Line (x1,x2)) };

      

       A5: for s be Real st 0 < s holds ex r be Real st r in R & r < ( |.(y1 - y2).| + s)

      proof

        let s be Real;

        assume

         A6: 0 < s;

        take |.(y1 - y2).|;

        thus thesis by A4, A1, A6, XREAL_1: 29;

      end;

      x1 in ( Line (x1,x2)) by Th9;

      then

       A7: |.(y1 - x1).| in R by A4;

      

       A8: for r be Real st r in R holds |.(y1 - y2).| <= r

      proof

        let r be Real;

        assume r in R;

        then ex x0 be Element of ( REAL n) st r = |.(y1 - x0).| & x0 in ( Line (x1,x2)) by A4;

        hence thesis by A3;

      end;

      R is bounded_below

      proof

        take |.(y1 - y2).|;

        let r be ExtReal;

        assume r in R;

        then ex x0 be Element of ( REAL n) st r = |.(y1 - x0).| & x0 in ( Line (x1,x2)) by A4;

        hence thesis by A3;

      end;

      then |.(y1 - y2).| = ( lower_bound R) by A7, A5, A8, SEQ_4:def 2;

      hence thesis by A1, A2;

    end;

    definition

      ::$Canceled

    end

    reserve p1,p2,q1,q2 for Point of ( TOP-REAL n);

    

     Lm8: for p1,p2 be Point of ( TOP-REAL n) holds ex x1,x2 be Element of ( REAL n) st p1 = x1 & p2 = x2 & ( Line (x1,x2)) = ( Line (p1,p2))

    proof

      let p1,p2 be Point of ( TOP-REAL n);

      reconsider x1 = p1, x2 = p2 as Element of ( REAL n) by EUCLID: 22;

      take x1, x2;

      thus p1 = x1 & p2 = x2;

      thus ( Line (x1,x2)) c= ( Line (p1,p2))

      proof

        let e be object;

        assume e in ( Line (x1,x2));

        then

        consider lambda such that

         A1: e = (((1 - lambda) * x1) + (lambda * x2));

        e = (((1 - lambda) * p1) + (lambda * p2)) by A1;

        hence e in ( Line (p1,p2));

      end;

      let e be object;

      assume e in ( Line (p1,p2));

      then

      consider lambda such that

       A2: e = (((1 - lambda) * p1) + (lambda * p2));

      e = (((1 - lambda) * x1) + (lambda * x2)) by A2;

      hence e in ( Line (x1,x2));

    end;

    theorem :: EUCLID_4:41

    p1 in ( Line (p1,p2)) & p2 in ( Line (p1,p2)) by RLTOPSP1: 72;

    theorem :: EUCLID_4:42

    q1 in ( Line (p1,p2)) & q2 in ( Line (p1,p2)) implies ( Line (q1,q2)) c= ( Line (p1,p2)) by RLTOPSP1: 74;

    theorem :: EUCLID_4:43

    q1 in ( Line (p1,p2)) & q2 in ( Line (p1,p2)) & q1 <> q2 implies ( Line (p1,p2)) c= ( Line (q1,q2)) by RLTOPSP1: 75;

    definition

      let n;

      let A be Subset of ( TOP-REAL n);

      :: EUCLID_4:def4

      attr A is being_line means ex p1, p2 st p1 <> p2 & A = ( Line (p1,p2));

    end

    

     Lm9: for A be Subset of ( TOP-REAL n), p1, p2 holds A is being_line & p1 in A & p2 in A & p1 <> p2 implies A = ( Line (p1,p2)) by RLTOPSP1: 75;

    theorem :: EUCLID_4:44

    for A,C be Subset of ( TOP-REAL n) holds A is being_line & C is being_line & p1 in A & p2 in A & p1 in C & p2 in C implies p1 = p2 or A = C

    proof

      let A,C be Subset of ( TOP-REAL n);

      assume that

       A1: A is being_line and

       A2: C is being_line and

       A3: p1 in A & p2 in A and

       A4: p1 in C & p2 in C;

      assume

       A5: p1 <> p2;

      then A = ( Line (p1,p2)) by A1, A3, Lm9;

      hence thesis by A2, A4, A5, Lm9;

    end;

    theorem :: EUCLID_4:45

    

     Th44: for A be Subset of ( TOP-REAL n) st A is being_line holds ex p1, p2 st p1 in A & p2 in A & p1 <> p2

    proof

      let A be Subset of ( TOP-REAL n);

      assume A is being_line;

      then

      consider p1, p2 such that

       A1: p1 <> p2 and

       A2: A = ( Line (p1,p2));

      p1 in A & p2 in A by A2, RLTOPSP1: 72;

      hence thesis by A1;

    end;

    theorem :: EUCLID_4:46

    for A be Subset of ( TOP-REAL n) st A is being_line holds ex p2 st p1 <> p2 & p2 in A

    proof

      let A be Subset of ( TOP-REAL n);

      assume A is being_line;

      then

      consider q1, q2 such that

       A1: q1 in A and

       A2: q2 in A & q1 <> q2 by Th44;

      p1 = q1 implies p1 <> q2 & q2 in A by A2;

      hence thesis by A1;

    end;

    theorem :: EUCLID_4:47

    for R be Subset of REAL , p1,p2,q1 be Point of ( TOP-REAL n) st R = { |.(q1 - p).| where p be Point of ( TOP-REAL n) : p in ( Line (p1,p2)) } holds ex q2 be Point of ( TOP-REAL n) st q2 in ( Line (p1,p2)) & |.(q1 - q2).| = ( lower_bound R) & ((p1 - p2),(q1 - q2)) are_orthogonal

    proof

      let R be Subset of REAL , p1,p2,q1 be Point of ( TOP-REAL n);

      reconsider y1 = q1 as Element of ( REAL n) by EUCLID: 22;

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

       A1: p1 = x1 & p2 = x2 and

       A2: ( Line (x1,x2)) = ( Line (p1,p2)) by Lm8;

      

       A3: (x1 - x2) = (p1 - p2) by A1;

      consider y2 be Element of ( REAL n) such that

       A4: y2 in ( Line (x1,x2)) and

       A5: ((x1 - x2),(y1 - y2)) are_orthogonal and

       A6: for x be Element of ( REAL n) st x in ( Line (x1,x2)) holds |.(y1 - y2).| <= |.(y1 - x).| by Lm7;

      reconsider q2 = y2 as Point of ( TOP-REAL n) by EUCLID: 22;

      assume

       A7: R = { |.(q1 - p).| where p be Point of ( TOP-REAL n) : p in ( Line (p1,p2)) };

      

       A8: for s be Real st 0 < s holds ex r be Real st r in R & r < ( |.(q1 - q2).| + s)

      proof

        let s be Real;

        assume

         A9: 0 < s;

        take |.(q1 - q2).|;

        thus thesis by A7, A2, A4, A9, XREAL_1: 29;

      end;

      p1 in ( Line (p1,p2)) by RLTOPSP1: 72;

      then

       A10: |.(q1 - p1).| in R by A7;

      

       A11: for r be Real st r in R holds |.(q1 - q2).| <= r

      proof

        let r be Real;

        assume r in R;

        then

        consider p0 be Point of ( TOP-REAL n) such that

         A12: r = |.(q1 - p0).| & p0 in ( Line (p1,p2)) by A7;

        the carrier of ( Euclid n) = the carrier of ( TOP-REAL n) by EUCLID: 67;

        then

        reconsider x = p0 as Element of ( REAL n);

        thus |.(q1 - q2).| <= r by A2, A6, A12;

      end;

      R is bounded_below

      proof

        take |.(q1 - q2).|;

        let r be ExtReal;

        assume r in R;

        then

        consider p0 be Point of ( TOP-REAL n) such that

         A13: r = |.(q1 - p0).| & p0 in ( Line (p1,p2)) by A7;

        the carrier of ( Euclid n) = the carrier of ( TOP-REAL n) by EUCLID: 67;

        then

        reconsider x = p0 as Element of ( REAL n);

        thus |.(q1 - q2).| <= r by A2, A6, A13;

      end;

      then (y1 - y2) = (q1 - q2) & |.(q1 - q2).| = ( lower_bound R) by A10, A8, A11, SEQ_4:def 2;

      hence thesis by A2, A4, A5, A3;

    end;