euclidlp.miz



    begin

    reserve a,a1,a2,a3,b,b1,b2,b3,r,s,t,u for Real;

    reserve n for Nat;

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

    theorem :: EUCLIDLP:1

    

     Th1: ((s / t) * (u * x)) = (((s * u) / t) * x) & ((1 / t) * (u * x)) = ((u / t) * x)

    proof

      

      thus ((s / t) * (u * x)) = (((s / t) * u) * x) by EUCLID_4: 4

      .= (((s * u) / t) * x) by XCMPLX_1: 74;

      

      thus ((1 / t) * (u * x)) = (((1 / t) * u) * x) by EUCLID_4: 4

      .= ((u / t) * x) by XCMPLX_1: 99;

    end;

    theorem :: EUCLIDLP:2

    

     Th2: (x - x) = ( 0* n) & (x + ( - x)) = ( 0* n)

    proof

      thus (x - x) = ( 0* n) by RVSUM_1: 37;

      hence thesis;

    end;

    theorem :: EUCLIDLP:3

    

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

    proof

      

      thus ( - (a * x)) = ((( - 1) * a) * x) by EUCLID_4: 4

      .= (( - a) * x);

      

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

      .= (a * ( - x)) by EUCLID_4: 4;

    end;

    theorem :: EUCLIDLP:4

    

     Th4: (x1 - (x2 - x3)) = ((x1 - x2) + x3)

    proof

      

      thus (x1 - (x2 - x3)) = ((x1 - x2) - ( - x3)) by RVSUM_1: 39

      .= ((x1 - x2) + x3);

    end;

    theorem :: EUCLIDLP:5

    

     Th5: (x1 + (x2 - x3)) = ((x1 + x2) - x3)

    proof

      

      thus (x1 + (x2 - x3)) = ((x1 + x2) + ( - x3)) by RVSUM_1: 15

      .= ((x1 + x2) - x3);

    end;

    theorem :: EUCLIDLP:6

    

     Th6: x1 = (x2 + x3) iff x2 = (x1 - x3)

    proof

      thus x1 = (x2 + x3) implies x2 = (x1 - x3)

      proof

        assume x1 = (x2 + x3);

        

        hence (x1 - x3) = (x2 + (x3 + ( - x3))) by RVSUM_1: 15

        .= (x2 + ( 0* n)) by Th2

        .= x2 by EUCLID_4: 1;

      end;

      now

        assume x2 = (x1 - x3);

        

        hence (x2 + x3) = (x1 + (( - x3) + x3)) by RVSUM_1: 15

        .= (x1 + ( 0* n)) by Th2

        .= x1 by EUCLID_4: 1;

      end;

      hence thesis;

    end;

    theorem :: EUCLIDLP:7

    

     Th7: x = ((x1 + x2) + x3) iff (x - x1) = (x2 + x3)

    proof

      thus x = ((x1 + x2) + x3) implies (x - x1) = (x2 + x3)

      proof

        assume x = ((x1 + x2) + x3);

        then x = (x1 + (x2 + x3)) by RVSUM_1: 15;

        hence thesis by Th6;

      end;

      now

        assume (x - x1) = (x2 + x3);

        

        hence x = (x1 + (x2 + x3)) by Th6

        .= ((x1 + x2) + x3) by RVSUM_1: 15;

      end;

      hence thesis;

    end;

    theorem :: EUCLIDLP:8

    

     Th8: ( - ((x1 + x2) + x3)) = ((( - x1) + ( - x2)) + ( - x3))

    proof

      

      thus ( - ((x1 + x2) + x3)) = (( 0* n) - ((x1 + x2) + x3)) by RVSUM_1: 33

      .= ((( 0* n) - (x1 + x2)) - x3) by RVSUM_1: 39

      .= (((( 0* n) - x1) - x2) - x3) by RVSUM_1: 39

      .= ((( - x1) + ( - x2)) + ( - x3)) by RVSUM_1: 33;

    end;

    

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

    proof

      now

        assume that

         A1: x1 <> x2 and

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

         |((x1 - x2), (x1 - x2))| = 0 by A2, EUCLID_4: 16;

        then (x1 - x2) = ( 0* n) by EUCLID_4: 17;

        

        then x1 = (x2 + ( 0* n)) by Th6

        .= x2 by EUCLID_4: 1;

        hence contradiction by A1;

      end;

      hence thesis;

    end;

    theorem :: EUCLIDLP:9

    

     Th9: x1 = x2 iff (x1 - x2) = ( 0* n)

    proof

      thus x1 = x2 implies (x1 - x2) = ( 0* n) by Th2;

      assume (x1 - x2) = ( 0* n);

      

      hence x1 = (x2 + ( 0* n)) by Th6

      .= x2 by EUCLID_4: 1;

    end;

    theorem :: EUCLIDLP:10

    

     Th10: (x1 - x0) = (t * x) & x1 <> x0 implies t <> 0

    proof

      assume that

       A1: (x1 - x0) = (t * x) and

       A2: x1 <> x0;

      assume not t <> 0 ;

      then (x1 - x0) = ( 0* n) by A1, EUCLID_4: 3;

      hence contradiction by A2, Th9;

    end;

    theorem :: EUCLIDLP:11

    

     Th11: ((a - b) * x) = ((a * x) + (( - b) * x)) & ((a - b) * x) = ((a * x) + ( - (b * x))) & ((a - b) * x) = ((a * x) - (b * x))

    proof

      

      thus

       A1: ((a - b) * x) = ((a + ( - b)) * x)

      .= ((a * x) + (( - b) * x)) by EUCLID_4: 7;

      hence ((a - b) * x) = ((a * x) + ( - (b * x))) by Th3;

      thus thesis by A1, Th3;

    end;

    theorem :: EUCLIDLP:12

    

     Th12: (a * (x - y)) = ((a * x) + ( - (a * y))) & (a * (x - y)) = ((a * x) + (( - a) * y)) & (a * (x - y)) = ((a * x) - (a * y))

    proof

      

      thus

       A1: (a * (x - y)) = ((a * x) + (a * ( - y))) by EUCLID_4: 6

      .= ((a * x) + ( - (a * y))) by Th3;

      hence (a * (x - y)) = ((a * x) + (( - a) * y)) by Th3;

      thus thesis by A1;

    end;

    theorem :: EUCLIDLP:13

    

     Th13: (((s - t) - u) * x) = (((s * x) - (t * x)) - (u * x))

    proof

      

      thus (((s - t) - u) * x) = (((s - t) * x) - (u * x)) by Th11

      .= (((s * x) - (t * x)) - (u * x)) by Th11;

    end;

    theorem :: EUCLIDLP:14

    

     Th14: (x - (((a1 * x1) + (a2 * x2)) + (a3 * x3))) = (x + (((( - a1) * x1) + (( - a2) * x2)) + (( - a3) * x3)))

    proof

      

      thus (x - (((a1 * x1) + (a2 * x2)) + (a3 * x3))) = (x + ((( - (a1 * x1)) + ( - (a2 * x2))) + ( - (a3 * x3)))) by Th8

      .= (x + (((( - a1) * x1) + ( - (a2 * x2))) + ( - (a3 * x3)))) by Th3

      .= (x + (((( - a1) * x1) + (( - a2) * x2)) + ( - (a3 * x3)))) by Th3

      .= (x + (((( - a1) * x1) + (( - a2) * x2)) + (( - a3) * x3))) by Th3;

    end;

    theorem :: EUCLIDLP:15

    (x - (((s + t) + u) * y)) = (((x + (( - s) * y)) + (( - t) * y)) + (( - u) * y))

    proof

      

      thus (x - (((s + t) + u) * y)) = (x - (((s + t) * y) + (u * y))) by EUCLID_4: 7

      .= (x - (((s * y) + (t * y)) + (u * y))) by EUCLID_4: 7

      .= (x + (((( - s) * y) + (( - t) * y)) + (( - u) * y))) by Th14

      .= ((x + ((( - s) * y) + (( - t) * y))) + (( - u) * y)) by RVSUM_1: 15

      .= (((x + (( - s) * y)) + (( - t) * y)) + (( - u) * y)) by RVSUM_1: 15;

    end;

    theorem :: EUCLIDLP:16

    

     Th16: ((x1 + x2) + (y1 + y2)) = ((x1 + y1) + (x2 + y2))

    proof

      

      thus ((x1 + x2) + (y1 + y2)) = (((x1 + x2) + y1) + y2) by RVSUM_1: 15

      .= (((x1 + y1) + x2) + y2) by RVSUM_1: 15

      .= ((x1 + y1) + (x2 + y2)) by RVSUM_1: 15;

    end;

    theorem :: EUCLIDLP:17

    

     Th17: (((x1 + x2) + x3) + ((y1 + y2) + y3)) = (((x1 + y1) + (x2 + y2)) + (x3 + y3))

    proof

      

      thus (((x1 + x2) + x3) + ((y1 + y2) + y3)) = (((x1 + x2) + (y1 + y2)) + (x3 + y3)) by Th16

      .= (((x1 + y1) + (x2 + y2)) + (x3 + y3)) by Th16;

    end;

    theorem :: EUCLIDLP:18

    

     Th18: ((x1 + x2) - (y1 + y2)) = ((x1 - y1) + (x2 - y2))

    proof

      

      thus ((x1 + x2) - (y1 + y2)) = (((x1 + x2) - y1) - y2) by RVSUM_1: 39

      .= ((x1 + x2) + (( - y1) + ( - y2))) by RVSUM_1: 15

      .= ((x1 - y1) + (x2 - y2)) by Th16;

    end;

    theorem :: EUCLIDLP:19

    (((x1 + x2) + x3) - ((y1 + y2) + y3)) = (((x1 - y1) + (x2 - y2)) + (x3 - y3))

    proof

      

      thus (((x1 + x2) + x3) - ((y1 + y2) + y3)) = (((x1 + x2) - (y1 + y2)) + (x3 - y3)) by Th18

      .= (((x1 - y1) + (x2 - y2)) + (x3 - y3)) by Th18;

    end;

    theorem :: EUCLIDLP:20

    

     Th20: (a * ((x1 + x2) + x3)) = (((a * x1) + (a * x2)) + (a * x3))

    proof

      

      thus (a * ((x1 + x2) + x3)) = ((a * (x1 + x2)) + (a * x3)) by EUCLID_4: 6

      .= (((a * x1) + (a * x2)) + (a * x3)) by EUCLID_4: 6;

    end;

    theorem :: EUCLIDLP:21

    

     Th21: (a * ((b1 * x1) + (b2 * x2))) = (((a * b1) * x1) + ((a * b2) * x2))

    proof

      

      thus (a * ((b1 * x1) + (b2 * x2))) = ((a * (b1 * x1)) + (a * (b2 * x2))) by EUCLID_4: 6

      .= (((a * b1) * x1) + (a * (b2 * x2))) by EUCLID_4: 4

      .= (((a * b1) * x1) + ((a * b2) * x2)) by EUCLID_4: 4;

    end;

    theorem :: EUCLIDLP:22

    

     Th22: (a * (((b1 * x1) + (b2 * x2)) + (b3 * x3))) = ((((a * b1) * x1) + ((a * b2) * x2)) + ((a * b3) * x3))

    proof

      

      thus (a * (((b1 * x1) + (b2 * x2)) + (b3 * x3))) = (((a * (b1 * x1)) + (a * (b2 * x2))) + (a * (b3 * x3))) by Th20

      .= ((((a * b1) * x1) + (a * (b2 * x2))) + (a * (b3 * x3))) by EUCLID_4: 4

      .= ((((a * b1) * x1) + ((a * b2) * x2)) + (a * (b3 * x3))) by EUCLID_4: 4

      .= ((((a * b1) * x1) + ((a * b2) * x2)) + ((a * b3) * x3)) by EUCLID_4: 4;

    end;

    theorem :: EUCLIDLP:23

    

     Th23: (((a1 * x1) + (a2 * x2)) + ((b1 * x1) + (b2 * x2))) = (((a1 + b1) * x1) + ((a2 + b2) * x2))

    proof

      

      thus (((a1 * x1) + (a2 * x2)) + ((b1 * x1) + (b2 * x2))) = (((a1 * x1) + (b1 * x1)) + ((a2 * x2) + (b2 * x2))) by Th16

      .= (((a1 + b1) * x1) + ((a2 * x2) + (b2 * x2))) by EUCLID_4: 7

      .= (((a1 + b1) * x1) + ((a2 + b2) * x2)) by EUCLID_4: 7;

    end;

    theorem :: EUCLIDLP:24

    

     Th24: ((((a1 * x1) + (a2 * x2)) + (a3 * x3)) + (((b1 * x1) + (b2 * x2)) + (b3 * x3))) = ((((a1 + b1) * x1) + ((a2 + b2) * x2)) + ((a3 + b3) * x3))

    proof

      

      thus ((((a1 * x1) + (a2 * x2)) + (a3 * x3)) + (((b1 * x1) + (b2 * x2)) + (b3 * x3))) = ((((a1 * x1) + (a2 * x2)) + ((b1 * x1) + (b2 * x2))) + ((a3 * x3) + (b3 * x3))) by Th16

      .= ((((a1 + b1) * x1) + ((a2 + b2) * x2)) + ((a3 * x3) + (b3 * x3))) by Th23

      .= ((((a1 + b1) * x1) + ((a2 + b2) * x2)) + ((a3 + b3) * x3)) by EUCLID_4: 7;

    end;

    theorem :: EUCLIDLP:25

    

     Th25: (((a1 * x1) + (a2 * x2)) - ((b1 * x1) + (b2 * x2))) = (((a1 - b1) * x1) + ((a2 - b2) * x2))

    proof

      

      thus (((a1 * x1) + (a2 * x2)) - ((b1 * x1) + (b2 * x2))) = (((a1 * x1) - (b1 * x1)) + ((a2 * x2) - (b2 * x2))) by Th18

      .= (((a1 - b1) * x1) + ((a2 * x2) - (b2 * x2))) by Th11

      .= (((a1 - b1) * x1) + ((a2 - b2) * x2)) by Th11;

    end;

    theorem :: EUCLIDLP:26

    

     Th26: ((((a1 * x1) + (a2 * x2)) + (a3 * x3)) - (((b1 * x1) + (b2 * x2)) + (b3 * x3))) = ((((a1 - b1) * x1) + ((a2 - b2) * x2)) + ((a3 - b3) * x3))

    proof

      

      thus ((((a1 * x1) + (a2 * x2)) + (a3 * x3)) - (((b1 * x1) + (b2 * x2)) + (b3 * x3))) = ((((a1 * x1) + (a2 * x2)) - ((b1 * x1) + (b2 * x2))) + ((a3 * x3) - (b3 * x3))) by Th18

      .= ((((a1 - b1) * x1) + ((a2 - b2) * x2)) + ((a3 * x3) - (b3 * x3))) by Th25

      .= ((((a1 - b1) * x1) + ((a2 - b2) * x2)) + ((a3 - b3) * x3)) by Th11;

    end;

    theorem :: EUCLIDLP:27

    

     Th27: ((a1 + a2) + a3) = 1 implies (((a1 * x1) + (a2 * x2)) + (a3 * x3)) = ((x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)))

    proof

      assume ((a1 + a2) + a3) = 1;

      then a1 = ((1 - a2) - a3);

      

      hence (((a1 * x1) + (a2 * x2)) + (a3 * x3)) = (((((1 * x1) - (a2 * x1)) - (a3 * x1)) + (a2 * x2)) + (a3 * x3)) by Th13

      .= ((((x1 + ( - (a2 * x1))) - (a3 * x1)) + (a2 * x2)) + (a3 * x3)) by EUCLID_4: 3

      .= ((((x1 + ( - (a2 * x1))) + (a2 * x2)) + ( - (a3 * x1))) + (a3 * x3)) by RVSUM_1: 15

      .= (((x1 + ((a2 * x2) + ( - (a2 * x1)))) + ( - (a3 * x1))) + (a3 * x3)) by RVSUM_1: 15

      .= ((x1 + ((a2 * x2) + ( - (a2 * x1)))) + ((a3 * x3) + ( - (a3 * x1)))) by RVSUM_1: 15

      .= ((x1 + (a2 * (x2 - x1))) + ((a3 * x3) + ( - (a3 * x1)))) by Th12

      .= ((x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1))) by Th12;

    end;

    theorem :: EUCLIDLP:28

    

     Th28: x = ((x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1))) implies ex a1 be Real st x = (((a1 * x1) + (a2 * x2)) + (a3 * x3)) & ((a1 + a2) + a3) = 1

    proof

      assume

       A1: x = ((x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1)));

      reconsider a1 = ((1 - a2) - a3) as Real;

      take a1;

      (((a1 * x1) + (a2 * x2)) + (a3 * x3)) = (((((1 * x1) - (a2 * x1)) - (a3 * x1)) + (a2 * x2)) + (a3 * x3)) by Th13

      .= ((((x1 + ( - (a2 * x1))) - (a3 * x1)) + (a2 * x2)) + (a3 * x3)) by EUCLID_4: 3

      .= ((((x1 + ( - (a2 * x1))) + (a2 * x2)) + ( - (a3 * x1))) + (a3 * x3)) by RVSUM_1: 15

      .= (((x1 + ((a2 * x2) + ( - (a2 * x1)))) + ( - (a3 * x1))) + (a3 * x3)) by RVSUM_1: 15

      .= ((x1 + ((a2 * x2) + ( - (a2 * x1)))) + ((a3 * x3) + ( - (a3 * x1)))) by RVSUM_1: 15

      .= ((x1 + (a2 * (x2 - x1))) + ((a3 * x3) + ( - (a3 * x1)))) by Th12

      .= x by A1, Th12;

      hence thesis;

    end;

    theorem :: EUCLIDLP:29

    for n be Nat st n >= 1 holds ( 1* n) <> ( 0* n)

    proof

      let n be Nat;

      assume n >= 1;

      then

       A1: 1 in ( Seg n) by FINSEQ_1: 1;

      assume

       A2: ( 1* n) = ( 0* n);

      ( 1* n) = (n |-> 1) & ((n |-> 0 ) . 1) = 0 by A1, FUNCOP_1: 7;

      hence contradiction by A2, A1, FUNCOP_1: 7;

    end;

    theorem :: EUCLIDLP:30

    

     Th30: 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))

    proof

      let A be Subset of ( REAL n);

      let x1, x2;

      assume that

       A1: A is being_line and

       A2: x1 in A & x2 in A & x1 <> x2;

      ex y1, y2 st y1 <> y2 & A = ( Line (y1,y2)) by A1;

      then ( Line (x1,x2)) c= A & A c= ( Line (x1,x2)) by A2, EUCLID_4: 10, EUCLID_4: 11;

      hence thesis by XBOOLE_0:def 10;

    end;

    theorem :: EUCLIDLP:31

    

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

    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);

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

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

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

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

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

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

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

      .= ((s - t) * (x2 - x1)) by Th12;

      hence thesis;

    end;

    definition

      let n;

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

      :: EUCLIDLP:def1

      pred x1 // x2 means

      : Def1: x1 <> ( 0* n) & x2 <> ( 0* n) & ex r st x1 = (r * x2);

    end

    theorem :: EUCLIDLP:32

    

     Th32: for x1,x2 be Element of ( REAL n) st x1 // x2 holds ex a st a <> 0 & x1 = (a * x2)

    proof

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

      assume

       A1: x1 // x2;

      then

      consider a such that

       A2: x1 = (a * x2);

      x1 <> ( 0* n) by A1;

      then a <> 0 by A2, EUCLID_4: 3;

      hence thesis by A2;

    end;

    definition

      let n;

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

      :: original: //

      redefine

      pred x1 // x2;

      symmetry

      proof

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

        assume

         A1: x1 // x2;

        then

         A2: x1 <> ( 0* n) & x2 <> ( 0* n);

        consider a such that

         A3: a <> 0 and

         A4: x1 = (a * x2) by A1, Th32;

        ((1 / a) * x1) = ((a / a) * x2) by A4, Th1

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

        .= x2 by EUCLID_4: 3;

        hence thesis by A2;

      end;

    end

    theorem :: EUCLIDLP:33

    

     Th33: x1 // x2 & x2 // x3 implies x1 // x3

    proof

      assume that

       A1: x1 // x2 and

       A2: x2 // x3;

      

       A3: ex t st x1 = (t * x3)

      proof

        consider b such that

         A4: x2 = (b * x3) by A2;

        consider a such that

         A5: x1 = (a * x2) by A1;

        x1 = ((a * b) * x3) by A5, A4, EUCLID_4: 4;

        hence thesis;

      end;

      x1 <> ( 0* n) & x3 <> ( 0* n) by A1, A2;

      hence thesis by A3;

    end;

    definition

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

      :: EUCLIDLP:def2

      pred x1,x2 are_lindependent2 means for a1,a2 be Real st ((a1 * x1) + (a2 * x2)) = ( 0* n) holds a1 = 0 & a2 = 0 ;

      symmetry ;

    end

    notation

      let n;

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

      antonym x1,x2 are_ldependent2 for x1,x2 are_lindependent2 ;

    end

    

     Lm2: (x1,x2) are_lindependent2 implies x1 <> ( 0* n)

    proof

      assume that

       A1: (x1,x2) are_lindependent2 and

       A2: not x1 <> ( 0* n);

      (1 * x1) = ( 0* n) by A2, EUCLID_4: 2;

      

      then ((1 * x1) + ( 0 * x2)) = (( 0* n) + ( 0* n)) by EUCLID_4: 3

      .= ( 0* n) by EUCLID_4: 1;

      hence contradiction by A1;

    end;

    theorem :: EUCLIDLP:34

    (x1,x2) are_lindependent2 implies x1 <> ( 0* n) & x2 <> ( 0* n) by Lm2;

    theorem :: EUCLIDLP:35

    

     Th35: for x1, x2 st (x1,x2) are_lindependent2 holds ((a1 * x1) + (a2 * x2)) = ((b1 * x1) + (b2 * x2)) implies a1 = b1 & a2 = b2

    proof

      let x1, x2;

      assume

       A1: (x1,x2) are_lindependent2 ;

      assume

       A2: ((a1 * x1) + (a2 * x2)) = ((b1 * x1) + (b2 * x2));

      ( 0* n) = (((a1 * x1) + (a2 * x2)) - ((a1 * x1) + (a2 * x2))) by Th2

      .= (((a1 - b1) * x1) + ((a2 - b2) * x2)) by A2, Th25;

      then (a1 - b1) = 0 & (a2 - b2) = 0 by A1;

      hence thesis;

    end;

    theorem :: EUCLIDLP:36

    

     Th36: for x1, x2, y1, y1 st (y1,y2) are_lindependent2 & y1 = ((a1 * x1) + (a2 * x2)) & y2 = ((b1 * x1) + (b2 * x2)) holds ex c1,c2,d1,d2 be Real st x1 = ((c1 * y1) + (c2 * y2)) & x2 = ((d1 * y1) + (d2 * y2))

    proof

      let x1, x2, y1, y1;

      assume

       A1: (y1,y2) are_lindependent2 ;

      assume that

       A2: y1 = ((a1 * x1) + (a2 * x2)) and

       A3: y2 = ((b1 * x1) + (b2 * x2));

      

       A4: (( - (b1 * y1)) + (a1 * y2)) = ((( - b1) * ((a1 * x1) + (a2 * x2))) + (a1 * ((b1 * x1) + (b2 * x2)))) by A2, A3, Th3

      .= ((((( - b1) * a1) * x1) + ((( - b1) * a2) * x2)) + (a1 * ((b1 * x1) + (b2 * x2)))) by Th21

      .= (((( - (a1 * b1)) * x1) + (( - (a2 * b1)) * x2)) + (((a1 * b1) * x1) + ((a1 * b2) * x2))) by Th21

      .= (((( - (a1 * b1)) + (a1 * b1)) * x1) + ((( - (a2 * b1)) + (a1 * b2)) * x2)) by Th23

      .= (( 0* n) + ((( - (a2 * b1)) + (a1 * b2)) * x2)) by EUCLID_4: 3

      .= (((a1 * b2) - (a2 * b1)) * x2) by EUCLID_4: 1;

      

       A5: ((b2 * y1) - (a2 * y2)) = ((((a1 * b2) * x1) + ((a2 * b2) * x2)) - (a2 * ((b1 * x1) + (b2 * x2)))) by A2, A3, Th21

      .= ((((a1 * b2) * x1) + ((a2 * b2) * x2)) - (((a2 * b1) * x1) + ((a2 * b2) * x2))) by Th21

      .= ((((a1 * b2) - (a2 * b1)) * x1) + (((a2 * b2) - (a2 * b2)) * x2)) by Th25

      .= ((((a1 * b2) - (a2 * b1)) * x1) + ( 0* n)) by EUCLID_4: 3

      .= (((a1 * b2) - (a2 * b1)) * x1) by EUCLID_4: 1;

      

       A6: ((a1 * b2) - (a2 * b1)) <> 0

      proof

        assume not ((a1 * b2) - (a2 * b1)) <> 0 ;

        

        then

         A7: ((b2 * y1) + (( - a2) * y2)) = ( 0 * x1) by A5, Th3

        .= ( 0* n) by EUCLID_4: 3;

        

        then

         A8: y2 = ((b1 * x1) + ( 0 * x2)) by A1, A3

        .= ((b1 * x1) + ( 0* n)) by EUCLID_4: 3

        .= (b1 * x1) by EUCLID_4: 1;

        

         A9: ( - a2) = 0 by A1, A7;

        

        then y1 = ((a1 * x1) + ( 0* n)) by A2, EUCLID_4: 3

        .= (a1 * x1) by EUCLID_4: 1;

        

        then ((b1 * y1) + (( - a1) * y2)) = (((a1 * b1) * x1) + (( - a1) * (b1 * x1))) by A8, EUCLID_4: 4

        .= (((a1 * b1) * x1) + ((( - a1) * b1) * x1)) by EUCLID_4: 4

        .= (((a1 * b1) + (( - a1) * b1)) * x1) by EUCLID_4: 7

        .= ( 0* n) by EUCLID_4: 3;

        then ( - a1) = 0 by A1;

        

        then y1 = (( 0* n) + ( 0 * x2)) by A2, A9, EUCLID_4: 3

        .= (( 0* n) + ( 0* n)) by EUCLID_4: 3

        .= ( 0* n) by EUCLID_4: 1;

        hence contradiction by A1, Lm2;

      end;

      

       A10: x2 = (1 * x2) by EUCLID_4: 3

      .= (((1 / ((a1 * b2) - (a2 * b1))) * ((a1 * b2) - (a2 * b1))) * x2) by A6, XCMPLX_1: 106

      .= ((1 / ((a1 * b2) - (a2 * b1))) * (((a1 * b2) - (a2 * b1)) * x2)) by EUCLID_4: 4

      .= (((1 / ((a1 * b2) - (a2 * b1))) * ( - (b1 * y1))) + ((1 / ((a1 * b2) - (a2 * b1))) * (a1 * y2))) by A4, EUCLID_4: 6

      .= (((1 / ((a1 * b2) - (a2 * b1))) * (( - b1) * y1)) + ((1 / ((a1 * b2) - (a2 * b1))) * (a1 * y2))) by Th3

      .= (((( - b1) / ((a1 * b2) - (a2 * b1))) * y1) + ((1 / ((a1 * b2) - (a2 * b1))) * (a1 * y2))) by Th1

      .= (((( - b1) / ((a1 * b2) - (a2 * b1))) * y1) + ((a1 / ((a1 * b2) - (a2 * b1))) * y2)) by Th1;

      set d2 = (a1 / ((a1 * b2) - (a2 * b1)));

      set d1 = (( - b1) / ((a1 * b2) - (a2 * b1)));

      set c2 = (( - a2) / ((a1 * b2) - (a2 * b1)));

      set c1 = (b2 / ((a1 * b2) - (a2 * b1)));

      take c1, c2, d1, d2;

      x1 = (1 * x1) by EUCLID_4: 3

      .= (((1 / ((a1 * b2) - (a2 * b1))) * ((a1 * b2) - (a2 * b1))) * x1) by A6, XCMPLX_1: 106

      .= ((1 / ((a1 * b2) - (a2 * b1))) * (((a1 * b2) - (a2 * b1)) * x1)) by EUCLID_4: 4

      .= (((1 / ((a1 * b2) - (a2 * b1))) * (b2 * y1)) - ((1 / ((a1 * b2) - (a2 * b1))) * (a2 * y2))) by A5, Th12

      .= (((b2 / ((a1 * b2) - (a2 * b1))) * y1) - ((1 / ((a1 * b2) - (a2 * b1))) * (a2 * y2))) by Th1

      .= (((b2 / ((a1 * b2) - (a2 * b1))) * y1) + ( - (((1 / ((a1 * b2) - (a2 * b1))) * a2) * y2))) by EUCLID_4: 4

      .= (((b2 / ((a1 * b2) - (a2 * b1))) * y1) + (( - ((1 / ((a1 * b2) - (a2 * b1))) * a2)) * y2)) by Th3

      .= (((b2 / ((a1 * b2) - (a2 * b1))) * y1) + (((1 / ((a1 * b2) - (a2 * b1))) * ( - a2)) * y2))

      .= (((b2 / ((a1 * b2) - (a2 * b1))) * y1) + ((( - a2) / ((a1 * b2) - (a2 * b1))) * y2)) by XCMPLX_1: 99;

      hence thesis by A10;

    end;

    theorem :: EUCLIDLP:37

    

     Th37: (x1,x2) are_lindependent2 implies x1 <> x2

    proof

      assume

       A1: (x1,x2) are_lindependent2 ;

      assume

       A2: x1 = x2;

      ((1 * x1) + (( - 1) * x2)) = (1 * (x1 - x2)) by Th12

      .= (1 * ( 0* n)) by A2, Th2

      .= ( 0* n) by EUCLID_4: 2;

      hence contradiction by A1;

    end;

    theorem :: EUCLIDLP:38

    ((x2 - x1),(x3 - x1)) are_lindependent2 implies x2 <> x3 by Th37;

    theorem :: EUCLIDLP:39

    (x1,x2) are_lindependent2 implies ((x1 + (t * x2)),x2) are_lindependent2

    proof

      assume

       A1: (x1,x2) are_lindependent2 ;

      for a,b be Real st ((a * (x1 + (t * x2))) + (b * x2)) = ( 0* n) holds a = 0 & b = 0

      proof

        let a, b;

        assume ((a * (x1 + (t * x2))) + (b * x2)) = ( 0* n);

        

        then

         A2: ( 0* n) = ((a * ((1 * x1) + (t * x2))) + (b * x2)) by EUCLID_4: 3

        .= ((((a * 1) * x1) + ((a * t) * x2)) + (b * x2)) by Th21

        .= ((a * x1) + (((a * t) * x2) + (b * x2))) by RVSUM_1: 15

        .= ((a * x1) + (((a * t) + b) * x2)) by EUCLID_4: 7;

        then a = 0 by A1;

        hence thesis by A1, A2;

      end;

      hence thesis;

    end;

    theorem :: EUCLIDLP:40

    

     Th40: ((x1 - x0),(x3 - x2)) are_lindependent2 & y0 in ( Line (x0,x1)) & y1 in ( Line (x0,x1)) & y0 <> y1 & y2 in ( Line (x2,x3)) & y3 in ( Line (x2,x3)) & y2 <> y3 implies ((y1 - y0),(y3 - y2)) are_lindependent2

    proof

      assume that

       A1: ((x1 - x0),(x3 - x2)) are_lindependent2 and

       A2: y0 in ( Line (x0,x1)) & y1 in ( Line (x0,x1)) and

       A3: y0 <> y1 and

       A4: y2 in ( Line (x2,x3)) & y3 in ( Line (x2,x3)) and

       A5: y2 <> y3;

      consider s be Real such that

       A6: (y1 - y0) = (s * (x1 - x0)) by A2, Th31;

      consider t be Real such that

       A7: (y3 - y2) = (t * (x3 - x2)) by A4, Th31;

      for a, b st ((a * (y1 - y0)) + (b * (y3 - y2))) = ( 0* n) holds a = 0 & b = 0

      proof

        let a, b;

        assume ((a * (y1 - y0)) + (b * (y3 - y2))) = ( 0* n);

        

        then

         A8: ( 0* n) = (((a * s) * (x1 - x0)) + (b * (t * (x3 - x2)))) by A6, A7, EUCLID_4: 4

        .= (((a * s) * (x1 - x0)) + ((b * t) * (x3 - x2))) by EUCLID_4: 4;

        then

         A9: (a * s) = 0 by A1;

        

         A10: (b * t) = 0 by A1, A8;

        

         A11: b = ((b * t) / t) by A5, A7, Th10, XCMPLX_1: 89

        .= 0 by A10;

        a = ((a * s) / s) by A3, A6, Th10, XCMPLX_1: 89

        .= 0 by A9;

        hence thesis by A11;

      end;

      hence thesis;

    end;

    

     Lm3: x1 // x2 implies (x1,x2) are_ldependent2

    proof

      assume x1 // x2;

      then

      consider r be Real such that

       A1: x1 = (r * x2);

      assume

       A2: (x1,x2) are_lindependent2 ;

      ( 0* n) = (x1 - x1) by Th2

      .= ((1 * x1) + ( - (r * x2))) by A1, EUCLID_4: 3

      .= ((1 * x1) + (( - r) * x2)) by Th3;

      hence contradiction by A2;

    end;

    theorem :: EUCLIDLP:41

    x1 // x2 implies (x1,x2) are_ldependent2 & x1 <> ( 0* n) & x2 <> ( 0* n) by Lm3;

    

     Lm4: (x1,x2) are_ldependent2 & x1 <> ( 0* n) & x2 <> ( 0* n) implies x1 // x2

    proof

      assume that

       A1: (x1,x2) are_ldependent2 and

       A2: x1 <> ( 0* n) & x2 <> ( 0* n);

      consider a1,a2 be Real such that

       A3: ((a1 * x1) + (a2 * x2)) = ( 0* n) and

       A4: a1 <> 0 or a2 <> 0 by A1;

      now

        per cases by A4;

          case

           A5: a1 <> 0 ;

          set t = (( - a2) / a1);

          take t;

          

           A6: (a1 * x1) = (( 0* n) - (a2 * x2)) by A3, Th6

          .= ( - (a2 * x2)) by RVSUM_1: 33;

          x1 = (1 * x1) by EUCLID_4: 3

          .= ((a1 / a1) * x1) by A5, XCMPLX_1: 60

          .= ((1 / a1) * (a1 * x1)) by Th1

          .= ((1 / a1) * (( - a2) * x2)) by A6, Th3

          .= ((( - a2) / a1) * x2) by Th1;

          hence thesis by A2;

        end;

          case

           A7: a2 <> 0 ;

          set s = (( - a1) / a2);

          take s;

          

           A8: (a2 * x2) = (( 0* n) - (a1 * x1)) by A3, Th6

          .= ( - (a1 * x1)) by RVSUM_1: 33;

          x2 = (1 * x2) by EUCLID_4: 3

          .= ((a2 / a2) * x2) by A7, XCMPLX_1: 60

          .= ((1 / a2) * (a2 * x2)) by Th1

          .= ((1 / a2) * (( - a1) * x1)) by A8, Th3

          .= ((( - a1) / a2) * x1) by Th1;

          hence thesis by A2, Def1;

        end;

      end;

      hence thesis;

    end;

    theorem :: EUCLIDLP:42

    (x1,x2) are_ldependent2 implies x1 = ( 0* n) or x2 = ( 0* n) or x1 // x2 by Lm4;

    theorem :: EUCLIDLP:43

    

     Th43: 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

    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, Lm1;

          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 EUCLID_4: 7

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

          .= |((x1 - x2), (((y1 - x1) - (( - mu) * x1)) - (mu * x2)))| by EUCLID_4: 3

          .= |((x1 - x2), ((y1 - 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 Th3

          .= |((x1 - x2), ((y1 - x1) - (( - mu) * (x1 - x2))))| by EUCLID_4: 6

          .= ( |((x1 - x2), (y1 - x1))| - |((x1 - x2), (( - mu) * (x1 - x2)))|) by EUCLID_4: 26

          .= ( |((x1 - x2), (y1 - x1))| - (( - mu) * |((x1 - x2), (x1 - x2))|)) by EUCLID_4: 21

          .= ( |((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 by RVSUM_1:def 17;

        end;

          case

           A3: x1 = x2;

          let mu be Real;

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

          take y2;

          (x1 - x2) = ( 0* n) by A3, Th2;

          then |((x1 - x2), (y1 - y2))| = 0 by EUCLID_4: 18;

          hence y2 in ( Line (x1,x2)) & ((x1 - x2),(y1 - y2)) are_orthogonal by RVSUM_1:def 17;

        end;

      end;

      hence thesis;

    end;

    definition

      let n;

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

      :: EUCLIDLP:def3

      pred x1 _|_ x2 means x1 <> ( 0* n) & x2 <> ( 0* n) & (x1,x2) are_orthogonal ;

      symmetry ;

    end

    theorem :: EUCLIDLP:44

    

     Th44: x _|_ y0 & y0 // y1 implies x _|_ y1

    proof

      assume that

       A1: x _|_ y0 and

       A2: y0 // y1;

      

       A3: (x,y0) are_orthogonal by A1;

      consider r such that

       A4: y1 = (r * y0) by A2, Def1;

       |(x, y1)| = (r * |(x, y0)|) by A4, EUCLID_4: 22

      .= (r * 0 ) by A3, RVSUM_1:def 17

      .= 0 ;

      then

       A5: (x,y1) are_orthogonal by RVSUM_1:def 17;

      x <> ( 0* n) & y1 <> ( 0* n) by A1, A2;

      hence thesis by A5;

    end;

    theorem :: EUCLIDLP:45

    

     Th45: x _|_ y implies (x,y) are_lindependent2

    proof

      assume

       A1: x _|_ y;

      then (x,y) are_orthogonal ;

      then

       A2: |(x, y)| = 0 by RVSUM_1:def 17;

      x <> ( 0* n) by A1;

      then |(x, x)| <> 0 by EUCLID_4: 17;

      then

       A3: |(x, x)| > 0 by RVSUM_1: 119;

      y <> ( 0* n) by A1;

      then

       A4: |(y, y)| <> 0 by EUCLID_4: 17;

      then

       A5: |(y, y)| > 0 by RVSUM_1: 119;

      for a, b st ((a * x) + (b * y)) = ( 0* n) holds a = 0 & b = 0

      proof

        let a, b;

        assume ((a * x) + (b * y)) = ( 0* n);

        

        then

         A6: 0 = |(((a * x) + (b * y)), ((a * x) + (b * y)))| by EUCLID_4: 17

        .= (( |((a * x), (a * x))| + (2 * |((a * x), (b * y))|)) + |((b * y), (b * y))|) by EUCLID_4: 32

        .= (((a * |(x, (a * x))|) + (2 * |((a * x), (b * y))|)) + |((b * y), (b * y))|) by EUCLID_4: 21

        .= (((a * |(x, (a * x))|) + (2 * (a * |(x, (b * y))|))) + |((b * y), (b * y))|) by EUCLID_4: 21

        .= (((a * |(x, (a * x))|) + ((2 * a) * |(x, (b * y))|)) + (b * |(y, (b * y))|)) by EUCLID_4: 21

        .= (((a * (a * |(x, x)|)) + ((2 * a) * |(x, (b * y))|)) + (b * |(y, (b * y))|)) by EUCLID_4: 22

        .= ((((a * a) * |(x, x)|) + ((2 * a) * (b * |(x, y)|))) + (b * |(y, (b * y))|)) by EUCLID_4: 22

        .= ((((a * a) * |(x, x)|) + (((2 * a) * b) * |(x, y)|)) + (b * (b * |(y, y)|))) by EUCLID_4: 22

        .= (((a * a) * |(x, x)|) + ((b * b) * |(y, y)|)) by A2;

        

         A7: (b * b) >= 0 by XREAL_1: 63;

        

         A8: (a * a) = 0

        proof

          assume (a * a) <> 0 ;

          then (a * a) > 0 by XREAL_1: 63;

          then ((a * a) * |(x, x)|) > 0 by A3, XREAL_1: 129;

          hence contradiction by A5, A6, A7;

        end;

        then (b * b) = 0 by A4, A6, XCMPLX_1: 6;

        hence thesis by A8, XCMPLX_1: 6;

      end;

      hence thesis;

    end;

    theorem :: EUCLIDLP:46

    x1 // x2 implies not x1 _|_ x2

    proof

      assume

       A1: x1 // x2;

      then

      consider r such that

       A2: x1 = (r * x2);

      x2 <> ( 0* n) by A1;

      then

       A3: |(x2, x2)| <> 0 by EUCLID_4: 17;

      x1 <> ( 0* n) by A1;

      then

       A4: r <> 0 by A2, EUCLID_4: 3;

       |(x1, x2)| = (r * |(x2, x2)|) by A2, EUCLID_4: 21;

      then |(x1, x2)| <> 0 by A4, A3, XCMPLX_1: 6;

      then not (x1,x2) are_orthogonal by RVSUM_1:def 17;

      hence thesis;

    end;

    definition

      let n;

      :: EUCLIDLP:def4

      func line_of_REAL n -> Subset-Family of ( REAL n) equals the set of all ( Line (x1,x2)) where x1,x2 be Element of ( REAL n);

      correctness

      proof

        set A = the set of all ( Line (x1,x2)) where x1,x2 be Element of ( REAL n);

        A c= ( bool ( REAL n))

        proof

          let L be object;

          assume L in A;

          then ex x1,x2 be Element of ( REAL n) st L = ( Line (x1,x2));

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let n;

      cluster ( line_of_REAL n) -> non empty;

      coherence

      proof

        reconsider L = ( Line (( 0* n),( 1* n))) as Subset of ( REAL n);

        L in ( line_of_REAL n);

        hence thesis;

      end;

    end

    theorem :: EUCLIDLP:47

    

     Th47: ( Line (x1,x2)) in ( line_of_REAL n);

    reserve L,L0,L1,L2 for Element of ( line_of_REAL n);

    theorem :: EUCLIDLP:48

    

     Th48: x1 in L & x2 in L implies ( Line (x1,x2)) c= L

    proof

      L in ( line_of_REAL n);

      then ex y1,y2 be Element of ( REAL n) st L = ( Line (y1,y2));

      hence thesis by EUCLID_4: 10;

    end;

    theorem :: EUCLIDLP:49

    

     Th49: L1 meets L2 iff ex x st x in L1 & x in L2

    proof

      thus L1 meets L2 implies ex x st x in L1 & x in L2

      proof

        assume L1 meets L2;

        then

        consider x be object such that

         A1: x in L1 and

         A2: x in L2 by XBOOLE_0: 3;

        reconsider x as Element of ( REAL n) by A1;

        take x;

        thus thesis by A1, A2;

      end;

      thus thesis by XBOOLE_0: 3;

    end;

    theorem :: EUCLIDLP:50

    L0 misses L1 & x in L0 implies not x in L1 by Th49;

    theorem :: EUCLIDLP:51

    

     Th51: ex x1, x2 st L = ( Line (x1,x2))

    proof

      L in ( line_of_REAL n);

      then

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

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

      take x1, x2;

      thus thesis by A1;

    end;

    theorem :: EUCLIDLP:52

    

     Th52: ex x st x in L

    proof

      consider x1, x2 such that

       A1: L = ( Line (x1,x2)) by Th51;

      take x1;

      thus thesis by A1, EUCLID_4: 9;

    end;

    theorem :: EUCLIDLP:53

    

     Th53: L is being_line implies ex x1 st x1 <> x0 & x1 in L

    proof

      assume L is being_line;

      then

      consider y1, y2 such that

       A1: y1 in L and

       A2: y2 in L & y1 <> y2 by EUCLID_4: 13;

      now

        per cases ;

          case

           A3: y1 = x0;

          take y2;

          thus y2 <> x0 & y2 in L by A2, A3;

        end;

          case

           A4: y1 <> x0;

          take y1;

          thus y1 <> x0 & y1 in L by A1, A4;

        end;

      end;

      hence thesis;

    end;

    theorem :: EUCLIDLP:54

    

     Th54: ( not x in L) & L is being_line implies ex x1, x2 st L = ( Line (x1,x2)) & (x - x1) _|_ (x2 - x1)

    proof

      assume that

       A1: not x in L and

       A2: L is being_line;

      consider y0, y1 such that

       A3: y0 <> y1 and

       A4: L = ( Line (y0,y1)) by A2;

      

       A5: (y0 - y1) <> ( 0* n) by A3, Th9;

      consider x1 be Element of ( REAL n) such that

       A6: x1 in ( Line (y0,y1)) and

       A7: ((y0 - y1),(x - x1)) are_orthogonal by Th43;

      (x - x1) <> ( 0* n) by A1, A4, A6, Th9;

      then

       A8: (y0 - y1) _|_ (x - x1) by A7, A5;

      take x1;

      consider x2 be Element of ( REAL n) such that

       A9: x1 <> x2 and

       A10: x2 in L by A2, EUCLID_4: 14;

      take x2;

      

       A11: (x2 - x1) <> ( 0* n) by A9, Th9;

      ex a be Real st (x2 - x1) = (a * (y0 - y1)) by A4, A6, A10, Th31;

      then (x2 - x1) // (y0 - y1) by A5, A11;

      hence thesis by A2, A4, A6, A8, A9, A10, Th30, Th44;

    end;

    theorem :: EUCLIDLP:55

    

     Th55: ( not x in L) & L is being_line implies ex x1, x2 st L = ( Line (x1,x2)) & ((x - x1),(x2 - x1)) are_lindependent2

    proof

      assume ( not x in L) & L is being_line;

      then

      consider x1, x2 such that

       A1: L = ( Line (x1,x2)) & (x - x1) _|_ (x2 - x1) by Th54;

      take x1;

      take x2;

      thus thesis by A1, Th45;

    end;

    definition

      let n be Nat, x be Element of ( REAL n), L be Element of ( line_of_REAL n);

      :: EUCLIDLP:def5

      func dist_v (x,L) -> Subset of REAL equals { |.(x - x0).| where x0 be Element of ( REAL n) : x0 in L };

      correctness

      proof

        set A = { |.(x - x0).| where x0 be Element of ( REAL n) : x0 in L };

        A c= REAL

        proof

          let r be object;

          assume r in A;

          then ex x0 be Element of ( REAL n) st r = |.(x - x0).| & x0 in L;

          hence thesis by XREAL_0:def 1;

        end;

        hence thesis;

      end;

    end

    definition

      let n be Nat, x be Element of ( REAL n), L be Element of ( line_of_REAL n);

      :: EUCLIDLP:def6

      func dist (x,L) -> Real equals ( lower_bound ( dist_v (x,L)));

      correctness ;

    end

    theorem :: EUCLIDLP:56

    L = ( Line (x1,x2)) implies { |.(x - x0).| where x0 be Element of ( REAL n) : x0 in ( Line (x1,x2)) } = ( dist_v (x,L));

    theorem :: EUCLIDLP:57

    

     Th57: ex x0 st x0 in L & |.(x - x0).| = ( dist (x,L))

    proof

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

       A1: L = ( Line (x1,x2)) by Th51;

      { |.(x - x9).| where x9 be Element of ( REAL n) : x9 in ( Line (x1,x2)) } = ( dist_v (x,L)) by A1;

      then

      reconsider R = { |.(x - x9).| where x9 be Element of ( REAL n) : x9 in ( Line (x1,x2)) } as Subset of REAL ;

      consider x0 be Element of ( REAL n) such that

       A2: x0 in ( Line (x1,x2)) & |.(x - x0).| = ( lower_bound R) and ((x1 - x2),(x - x0)) are_orthogonal by EUCLID_4: 40;

      take x0;

      thus thesis by A1, A2;

    end;

    theorem :: EUCLIDLP:58

    ( dist (x,L)) >= 0

    proof

      ex x0 be Element of ( REAL n) st x0 in L & |.(x - x0).| = ( dist (x,L)) by Th57;

      hence thesis;

    end;

    theorem :: EUCLIDLP:59

    x in L iff ( dist (x,L)) = 0

    proof

      thus x in L implies ( dist (x,L)) = 0

      proof

        

         A1: for r be Real st r in ( dist_v (x,L)) holds 0 <= r

        proof

          let r be Real;

          assume r in ( dist_v (x,L));

          then ex x0 be Element of ( REAL n) st r = |.(x - x0).| & x0 in L;

          hence thesis;

        end;

        

         A2: ( dist_v (x,L)) is bounded_below

        proof

          take 0 ;

          let r be ExtReal;

          assume r in ( dist_v (x,L));

          then ex x0 be Element of ( REAL n) st r = |.(x - x0).| & x0 in L;

          hence thesis;

        end;

        assume

         A3: x in L;

         |.(x - x).| = |.( 0* n).| by Th9

        .= ( sqrt |(( 0* n), ( 0* n))|) by EUCLID_4: 15

        .= 0 by EUCLID_4: 17, SQUARE_1: 17;

        then

         A4: 0 in ( dist_v (x,L)) by A3;

        then for s be Real st 0 < s holds ex r be Real st r in ( dist_v (x,L)) & r < ( 0 + s);

        hence thesis by A4, A1, A2, SEQ_4:def 2;

      end;

      now

        consider x0 be Element of ( REAL n) such that

         A5: x0 in L and

         A6: |.(x - x0).| = ( dist (x,L)) by Th57;

        assume ( dist (x,L)) = 0 ;

        then |((x - x0), (x - x0))| = 0 by A6, EUCLID_4: 16;

        then (x - x0) = ( 0* n) by EUCLID_4: 17;

        hence x in L by A5, Th9;

      end;

      hence thesis;

    end;

    definition

      let n;

      let L1, L2;

      :: EUCLIDLP:def7

      pred L1 // L2 means ex x1,x2,y1,y2 be Element of ( REAL n) st L1 = ( Line (x1,x2)) & L2 = ( Line (y1,y2)) & (x2 - x1) // (y2 - y1);

      symmetry ;

    end

    theorem :: EUCLIDLP:60

    L0 // L1 & L1 // L2 implies L0 // L2

    proof

      assume that

       A1: L0 // L1 and

       A2: L1 // L2;

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

       A3: L0 = ( Line (x0,x1)) and

       A4: L1 = ( Line (x2,x3)) and

       A5: (x1 - x0) // (x3 - x2) by A1;

      

       A6: (x3 - x2) <> ( 0* n) by A5;

      consider y0,y1,y2,y3 be Element of ( REAL n) such that

       A7: L1 = ( Line (y0,y1)) and

       A8: L2 = ( Line (y2,y3)) and

       A9: (y1 - y0) // (y3 - y2) by A2;

      

       A10: (y1 - y0) <> ( 0* n) by A9;

      x3 in ( Line (y1,y0)) & x2 in ( Line (y1,y0)) by A4, A7, EUCLID_4: 9;

      then ex a st (x3 - x2) = (a * (y1 - y0)) by Th31;

      then (x3 - x2) // (y1 - y0) by A6, A10;

      then (x1 - x0) // (y1 - y0) by A5, Th33;

      then (x1 - x0) // (y3 - y2) by A9, Th33;

      hence thesis by A3, A8;

    end;

    definition

      let n;

      let L1, L2;

      :: EUCLIDLP:def8

      pred L1 _|_ L2 means ex x1,x2,y1,y2 be Element of ( REAL n) st L1 = ( Line (x1,x2)) & L2 = ( Line (y1,y2)) & (x2 - x1) _|_ (y2 - y1);

      symmetry ;

    end

    theorem :: EUCLIDLP:61

    

     Th61: L0 _|_ L1 & L1 // L2 implies L0 _|_ L2

    proof

      assume that

       A1: L0 _|_ L1 and

       A2: L1 // L2;

      consider x0, x1, x2, x3 such that

       A3: L0 = ( Line (x0,x1)) and

       A4: L1 = ( Line (x2,x3)) and

       A5: (x1 - x0) _|_ (x3 - x2) by A1;

      

       A6: (x3 - x2) <> ( 0* n) by A5;

      consider y0, y1, y2, y3 such that

       A7: L1 = ( Line (y0,y1)) and

       A8: L2 = ( Line (y2,y3)) and

       A9: (y1 - y0) // (y3 - y2) by A2;

      

       A10: (y1 - y0) <> ( 0* n) by A9;

      x2 in ( Line (y0,y1)) & x3 in ( Line (y0,y1)) by A4, A7, EUCLID_4: 9;

      then ex a st (x3 - x2) = (a * (y1 - y0)) by Th31;

      then (x3 - x2) // (y1 - y0) by A6, A10;

      then (x1 - x0) _|_ (y3 - y2) by A5, A9, Th33, Th44;

      hence thesis by A3, A8;

    end;

    theorem :: EUCLIDLP:62

    

     Th62: ( not x in L) & L is being_line implies ex L0 st x in L0 & L0 _|_ L & L0 meets L

    proof

      assume ( not x in L) & L is being_line;

      then

      consider x1, x2 such that

       A1: L = ( Line (x1,x2)) and

       A2: (x - x1) _|_ (x2 - x1) by Th54;

      reconsider L0 = ( Line (x1,x)) as Subset of ( REAL n);

      reconsider L0 as Element of ( line_of_REAL n) by Th47;

      x1 in L0 & x1 in L by A1, EUCLID_4: 9;

      then

       A3: x in L0 & L0 meets L by Th49, EUCLID_4: 9;

      L0 _|_ L by A1, A2;

      hence thesis by A3;

    end;

    theorem :: EUCLIDLP:63

    

     Th63: L1 misses L2 implies ex x st x in L1 & not x in L2

    proof

      assume

       A1: L1 misses L2;

      consider x such that

       A2: x in L1 by Th52;

      take x;

      thus thesis by A1, A2, Th49;

    end;

    theorem :: EUCLIDLP:64

    

     Th64: x1 in L & x2 in L & x1 <> x2 implies ( Line (x1,x2)) = L & L is being_line

    proof

      assume that

       A1: x1 in L & x2 in L and

       A2: x1 <> x2;

      

       A3: ( Line (x1,x2)) c= L by A1, Th48;

      L in ( line_of_REAL n);

      then ex y1,y2 be Element of ( REAL n) st L = ( Line (y1,y2));

      then L c= ( Line (x1,x2)) by A1, A2, EUCLID_4: 11;

      then ( Line (x1,x2)) = L by A3, XBOOLE_0:def 10;

      hence thesis by A2;

    end;

    theorem :: EUCLIDLP:65

    

     Th65: L1 is being_line & L1 = L2 implies L1 // L2

    proof

      assume L1 is being_line;

      then

      consider x0, x1 such that

       A1: x0 <> x1 and

       A2: L1 = ( Line (x0,x1));

      assume

       A3: L1 = L2;

      

       A4: (x1 - x0) = (1 * (x1 - x0)) by EUCLID_4: 3;

      (x1 - x0) <> ( 0* n) by A1, Th9;

      then (x1 - x0) // (x1 - x0) by A4;

      hence thesis by A3, A2;

    end;

    theorem :: EUCLIDLP:66

    

     Th66: L1 // L2 implies L1 is being_line & L2 is being_line

    proof

      assume L1 // L2;

      then

      consider x1, x2, y1, y2 such that

       A1: L1 = ( Line (x1,x2)) & L2 = ( Line (y1,y2)) and

       A2: (x2 - x1) // (y2 - y1);

      (y2 - y1) <> ( 0* n) by A2;

      then

       A3: y2 <> y1 by Th9;

      (x2 - x1) <> ( 0* n) by A2;

      then x2 <> x1 by Th9;

      hence thesis by A1, A3;

    end;

    theorem :: EUCLIDLP:67

    

     Th67: L1 _|_ L2 implies L1 is being_line & L2 is being_line

    proof

      assume L1 _|_ L2;

      then

      consider x1, x2, y1, y2 such that

       A1: L1 = ( Line (x1,x2)) & L2 = ( Line (y1,y2)) and

       A2: (x2 - x1) _|_ (y2 - y1);

      (y2 - y1) <> ( 0* n) by A2;

      then

       A3: y2 <> y1 by Th9;

      (x2 - x1) <> ( 0* n) by A2;

      then x2 <> x1 by Th9;

      hence thesis by A1, A3;

    end;

    theorem :: EUCLIDLP:68

    x in L & a <> 1 & (a * x) in L implies ( 0* n) in L

    proof

      assume that

       A1: x in L and

       A2: a <> 1 and

       A3: (a * x) in L;

      

       A4: (1 - a) <> 0 by A2;

      

       A5: ((1 - (1 / (1 - a))) + ((1 / (1 - a)) * a)) = ((1 - (1 / (1 - a))) + (a / (1 - a))) by XCMPLX_1: 99

      .= (1 + (( - (1 / (1 - a))) + (a / (1 - a))))

      .= (1 + ((( - 1) / (1 - a)) + (a / (1 - a)))) by XCMPLX_1: 187

      .= (1 + ((( - 1) + a) / (1 - a))) by XCMPLX_1: 62

      .= (1 + (( - (( - a) + 1)) / (1 - a)))

      .= (1 + ( - ((1 - a) / (1 - a)))) by XCMPLX_1: 187

      .= (1 - ((1 - a) / (1 - a)))

      .= (1 - 1) by A4, XCMPLX_1: 60

      .= 0 ;

      ( 0* n) = ( 0 * x) by EUCLID_4: 3

      .= (((1 - (1 / (1 - a))) * x) + (((1 / (1 - a)) * a) * x)) by A5, EUCLID_4: 7

      .= (((1 - (1 / (1 - a))) * x) + ((1 / (1 - a)) * (a * x))) by EUCLID_4: 4;

      then

       A6: ( 0* n) in ( Line (x,(a * x)));

      ( Line (x,(a * x))) c= L by A1, A3, Th48;

      hence thesis by A6;

    end;

    theorem :: EUCLIDLP:69

    x1 in L & x2 in L implies ex x3 st x3 in L & (x3 - x1) = (a * (x2 - x1))

    proof

      set x3 = (((1 - a) * x1) + (a * x2));

      assume x1 in L & x2 in L;

      then

       A1: ( Line (x1,x2)) c= L by Th48;

      x3 = (((1 * x1) + ( - (a * x1))) + (a * x2)) by Th11

      .= ((x1 + ( - (a * x1))) + (a * x2)) by EUCLID_4: 3

      .= (x1 + ((a * x2) + ( - (a * x1)))) by RVSUM_1: 15

      .= (x1 + (a * (x2 - x1))) by Th12;

      then x3 in ( Line (x1,x2)) & (x3 - x1) = (a * (x2 - x1)) by Th6;

      hence thesis by A1;

    end;

    theorem :: EUCLIDLP:70

    

     Th70: x1 in L & x2 in L & x3 in L & x1 <> x2 implies ex a st (x3 - x1) = (a * (x2 - x1))

    proof

      assume x1 in L & x2 in L & x3 in L & x1 <> x2;

      then x1 in ( Line (x1,x2)) & x3 in ( Line (x1,x2)) by Th64;

      then

      consider a such that

       A1: (x3 - x1) = (a * (x2 - x1)) by Th31;

      take a;

      thus thesis by A1;

    end;

    theorem :: EUCLIDLP:71

    

     Th71: L1 // L2 & L1 <> L2 implies L1 misses L2

    proof

      assume that

       A1: L1 // L2 and

       A2: L1 <> L2;

      assume not L1 misses L2;

      then

      consider x be object such that

       A3: x in L1 and

       A4: x in L2 by XBOOLE_0: 3;

      reconsider x as Element of ( REAL n) by A3;

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

       A5: L1 = ( Line (x1,x2)) and

       A6: L2 = ( Line (y1,y2)) and

       A7: (x2 - x1) // (y2 - y1) by A1;

      

       A8: (x2 - x1) <> ( 0* n) by A7;

      then x1 <> x2 by Th9;

      then

       A9: L1 is being_line by A5;

      then

      consider x0 such that

       A10: x <> x0 and

       A11: x0 in L1 by EUCLID_4: 14;

      

       A12: (x0 - x) <> ( 0* n) by A10, Th9;

      ex a st (x0 - x) = (a * (x2 - x1)) by A5, A3, A11, Th31;

      then (x0 - x) // (x2 - x1) by A8, A12;

      then

       A13: (x0 - x) // (y2 - y1) by A7, Th33;

      

       A14: (y2 - y1) <> ( 0* n) by A7;

      then y1 <> y2 by Th9;

      then

       A15: L2 is being_line by A6;

      then

      consider y0 such that

       A16: x <> y0 and

       A17: y0 in L2 by EUCLID_4: 14;

      

       A18: (y0 - x) <> ( 0* n) by A16, Th9;

      ex b st (y0 - x) = (b * (y2 - y1)) by A6, A4, A17, Th31;

      then (y0 - x) // (y2 - y1) by A14, A18;

      then

       A19: (x0 - x) // (y0 - x) by A13, Th33;

      

       A20: ( Line (x,x0)) c= ( Line (x,y0))

      proof

        let y be object;

        assume y in ( Line (x,x0));

        then

        consider t such that

         A21: y = (((1 - t) * x) + (t * x0));

        consider a such that

         A22: (x0 - x) = (a * (y0 - x)) by A19;

        y = (((1 * x) + ( - (t * x))) + (t * x0)) by A21, Th11

        .= ((x + ( - (t * x))) + (t * x0)) by EUCLID_4: 3

        .= (x + ((t * x0) + ( - (t * x)))) by RVSUM_1: 15

        .= (x + (t * (x0 - x))) by Th12;

        

        then y = (x + ((t * a) * (y0 - x))) by A22, EUCLID_4: 4

        .= (x + (((t * a) * y0) + ( - ((t * a) * x)))) by Th12

        .= ((x + ( - ((t * a) * x))) + ((t * a) * y0)) by RVSUM_1: 15

        .= (((1 * x) + ( - ((t * a) * x))) + ((t * a) * y0)) by EUCLID_4: 3

        .= (((1 - (t * a)) * x) + ((t * a) * y0)) by Th11;

        hence thesis;

      end;

      

       A23: ( Line (x,y0)) c= ( Line (x,x0))

      proof

        let y be object;

        assume y in ( Line (x,y0));

        then

        consider t such that

         A24: y = (((1 - t) * x) + (t * y0));

        consider a such that

         A25: (y0 - x) = (a * (x0 - x)) by A19, Def1;

        y = (((1 * x) + ( - (t * x))) + (t * y0)) by A24, Th11

        .= ((x + ( - (t * x))) + (t * y0)) by EUCLID_4: 3

        .= (x + ((t * y0) + ( - (t * x)))) by RVSUM_1: 15

        .= (x + (t * (y0 - x))) by Th12;

        

        then y = (x + ((t * a) * (x0 - x))) by A25, EUCLID_4: 4

        .= (x + (((t * a) * x0) + ( - ((t * a) * x)))) by Th12

        .= ((x + ( - ((t * a) * x))) + ((t * a) * x0)) by RVSUM_1: 15

        .= (((1 * x) + ( - ((t * a) * x))) + ((t * a) * x0)) by EUCLID_4: 3

        .= (((1 - (t * a)) * x) + ((t * a) * x0)) by Th11;

        hence thesis;

      end;

      

       A26: L2 = ( Line (x,y0)) by A4, A15, A16, A17, Th30;

      L1 = ( Line (x,x0)) by A3, A9, A10, A11, Th30;

      hence contradiction by A2, A26, A20, A23, XBOOLE_0:def 10;

    end;

    theorem :: EUCLIDLP:72

    

     Th72: L is being_line implies ex L0 st x in L0 & L0 // L

    proof

      assume L is being_line;

      then

      consider y0, y1 such that

       A1: y0 <> y1 and

       A2: L = ( Line (y0,y1));

      set x9 = (x + (y1 - y0));

      reconsider L0 = ( Line (x,x9)) as Element of ( line_of_REAL n) by Th47;

      take L0;

      

       A3: (y1 - y0) <> ( 0* n) by A1, Th9;

      

       A4: (x9 - x) = (y1 - y0) by Th6;

      then (x9 - x) = (1 * (y1 - y0)) by EUCLID_4: 3;

      then (x9 - x) // (y1 - y0) by A4, A3;

      hence thesis by A2, EUCLID_4: 9;

    end;

    theorem :: EUCLIDLP:73

    for x, L st ( not x in L) & L is being_line holds ex L0 st x in L0 & L0 // L & L0 <> L

    proof

      let x, L;

      assume that

       A1: not x in L and

       A2: L is being_line;

      ex L0 st x in L0 & L0 // L by A2, Th72;

      hence thesis by A1;

    end;

    theorem :: EUCLIDLP:74

    

     Th74: for x0, x1, y0, y1, L1, L2 st x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1 & L1 _|_ L2 holds (x1 - x0) _|_ (y1 - y0)

    proof

      let x0, x1, y0, y1, L1, L2;

      assume that

       A1: x0 in L1 & x1 in L1 and

       A2: x0 <> x1 and

       A3: y0 in L2 & y1 in L2 and

       A4: y0 <> y1 and

       A5: L1 _|_ L2;

      consider x2, x3, y2, y3 such that

       A6: L1 = ( Line (x2,x3)) and

       A7: L2 = ( Line (y2,y3)) and

       A8: (x3 - x2) _|_ (y3 - y2) by A5;

      consider s such that

       A9: (x1 - x0) = (s * (x3 - x2)) by A1, A6, Th31;

      ((x3 - x2),(y3 - y2)) are_orthogonal by A8;

      then

       A10: |((x3 - x2), (y3 - y2))| = 0 by RVSUM_1:def 17;

      consider t such that

       A11: (y1 - y0) = (t * (y3 - y2)) by A3, A7, Th31;

       |((x1 - x0), (y1 - y0))| = (s * |((x3 - x2), (y1 - y0))|) by A9, EUCLID_4: 21

      .= (s * (t * |((x3 - x2), (y3 - y2))|)) by A11, EUCLID_4: 22

      .= 0 by A10;

      then

       A12: ((x1 - x0),(y1 - y0)) are_orthogonal by RVSUM_1:def 17;

      (x1 - x0) <> ( 0* n) & (y1 - y0) <> ( 0* n) by A2, A4, Th9;

      hence thesis by A12;

    end;

    theorem :: EUCLIDLP:75

    

     Th75: for L1, L2 st L1 _|_ L2 holds L1 <> L2

    proof

      let L1, L2;

      assume

       A1: L1 _|_ L2;

      now

        per cases ;

          case

           A2: L1 misses L2;

          ex x st x in L1 by Th52;

          hence thesis by A2, Th49;

        end;

          case L1 meets L2;

          then

          consider x0 such that

           A3: x0 in L1 and

           A4: x0 in L2 by Th49;

          L1 is being_line by A1, Th67;

          then

          consider x1 such that

           A5: x1 <> x0 and

           A6: x1 in L1 by Th53;

          

           A7: (x1 - x0) <> ( 0* n) by A5, Th9;

          L2 is being_line by A1, Th67;

          then

          consider x2 such that

           A8: x2 <> x0 and

           A9: x2 in L2 by Th53;

          

           A10: (x2 - x0) <> ( 0* n) by A8, Th9;

          

           A11: (x1 - x0) _|_ (x2 - x0) by A1, A3, A4, A5, A6, A8, A9, Th74;

           not x1 in L2

          proof

            assume x1 in L2;

            then ex a st (x1 - x0) = (a * (x2 - x0)) by A4, A8, A9, Th70;

            then (x1 - x0) // (x2 - x0) by A7, A10;

            hence contradiction by A11, Lm3, Th45;

          end;

          hence thesis by A6;

        end;

      end;

      hence thesis;

    end;

    theorem :: EUCLIDLP:76

    

     Th76: for x1, x2, L st L is being_line & L = ( Line (x1,x2)) holds x1 <> x2

    proof

      let x1, x2, L;

      assume that

       A1: L is being_line and

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

      consider y1, y2 such that

       A3: y1 <> y2 and

       A4: L = ( Line (y1,y2)) by A1;

      y1 in L & y2 in L by A4, EUCLID_4: 9;

      then

      consider a such that

       A5: (y2 - y1) = (a * (x2 - x1)) by A2, Th31;

      thus x1 <> x2

      proof

        assume x1 = x2;

        

        then (y2 - y1) = (a * ( 0* n)) by A5, Th2

        .= ( 0* n) by EUCLID_4: 2;

        hence contradiction by A3, Th9;

      end;

    end;

    theorem :: EUCLIDLP:77

    

     Th77: x0 in L1 & x1 in L1 & x0 <> x1 & y0 in L2 & y1 in L2 & y0 <> y1 & L1 // L2 implies (x1 - x0) // (y1 - y0)

    proof

      assume that

       A1: x0 in L1 & x1 in L1 and

       A2: x0 <> x1 and

       A3: y0 in L2 & y1 in L2 and

       A4: y0 <> y1 and

       A5: L1 // L2;

      consider x2, x3, y2, y3 such that

       A6: L1 = ( Line (x2,x3)) and

       A7: L2 = ( Line (y2,y3)) and

       A8: (x3 - x2) // (y3 - y2) by A5;

      consider t such that

       A9: (y1 - y0) = (t * (y3 - y2)) by A3, A7, Th31;

      

       A10: (x1 - x0) <> ( 0* n) by A2, Th9;

      

       A11: (y1 - y0) <> ( 0* n) by A4, Th9;

      then

       A12: t <> 0 by A9, EUCLID_4: 3;

      consider s such that

       A13: (x1 - x0) = (s * (x3 - x2)) by A1, A6, Th31;

      consider a such that

       A14: (x3 - x2) = (a * (y3 - y2)) by A8;

      (x1 - x0) = ((s * a) * (y3 - y2)) by A13, A14, EUCLID_4: 4

      .= ((s * a) * (1 * (y3 - y2))) by EUCLID_4: 3

      .= ((s * a) * (((1 / t) * t) * (y3 - y2))) by A12, XCMPLX_1: 106

      .= ((s * a) * ((1 / t) * (t * (y3 - y2)))) by EUCLID_4: 4

      .= (((s * a) * (1 / t)) * (t * (y3 - y2))) by EUCLID_4: 4

      .= (((s * a) / t) * (y1 - y0)) by A9, XCMPLX_1: 99;

      hence thesis by A10, A11;

    end;

    theorem :: EUCLIDLP:78

    ((x2 - x1),(x3 - x1)) are_lindependent2 & y2 in ( Line (x1,x2)) & y3 in ( Line (x1,x3)) & L1 = ( Line (x2,x3)) & L2 = ( Line (y2,y3)) implies (L1 // L2 iff ex a st a <> 0 & (y2 - x1) = (a * (x2 - x1)) & (y3 - x1) = (a * (x3 - x1)))

    proof

      assume that

       A1: ((x2 - x1),(x3 - x1)) are_lindependent2 and

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

       A3: y3 in ( Line (x1,x3)) and

       A4: L1 = ( Line (x2,x3)) and

       A5: L2 = ( Line (y2,y3));

      thus L1 // L2 implies ex a st a <> 0 & (y2 - x1) = (a * (x2 - x1)) & (y3 - x1) = (a * (x3 - x1))

      proof

        assume

         A6: L1 // L2;

        then L1 is being_line by Th66;

        then

         A7: x2 <> x3 by A4, Th76;

        L2 is being_line by A6, Th66;

        then

         A8: y2 <> y3 by A5, Th76;

        

         A9: y2 in L2 & y3 in L2 by A5, EUCLID_4: 9;

        consider t such that

         A10: y3 = (((1 - t) * x1) + (t * x3)) by A3;

        x2 in L1 & x3 in L1 by A4, EUCLID_4: 9;

        then

         A11: (y3 - y2) // (x3 - x2) by A6, A7, A8, A9, Th77;

        then

        consider a such that

         A12: (y3 - y2) = (a * (x3 - x2));

        take a;

        consider s such that

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

        

         A14: ( 0* n) = ((y3 - y2) - (a * (x3 - x2))) by A12, Th9

        .= ((((((1 - t) * x1) + (t * x3)) - ((1 - s) * x1)) - (s * x2)) - (a * (x3 - x2))) by A13, A10, RVSUM_1: 39

        .= ((((((1 * x1) + ( - (t * x1))) + (t * x3)) - ((1 - s) * x1)) - (s * x2)) - (a * (x3 - x2))) by Th11

        .= ((((((1 * x1) + ( - (t * x1))) + (t * x3)) - ((1 * x1) + ( - (s * x1)))) - (s * x2)) - (a * (x3 - x2))) by Th11

        .= (((((((1 * x1) + ( - (t * x1))) + (t * x3)) - (1 * x1)) - ( - (s * x1))) - (s * x2)) - (a * (x3 - x2))) by RVSUM_1: 39

        .= (((((((1 * x1) + ( - (t * x1))) + ( - (1 * x1))) + (t * x3)) + (s * x1)) - (s * x2)) - (a * (x3 - x2))) by RVSUM_1: 15

        .= (((((((1 * x1) + ( - (1 * x1))) + ( - (t * x1))) + (t * x3)) + (s * x1)) - (s * x2)) - (a * (x3 - x2))) by RVSUM_1: 15

        .= (((((( 0* n) + ( - (t * x1))) + (t * x3)) + (s * x1)) - (s * x2)) - (a * (x3 - x2))) by Th2

        .= ((((( - (t * x1)) + (t * x3)) + (s * x1)) - (s * x2)) - (a * (x3 - x2))) by EUCLID_4: 1

        .= ((((t * (x3 - x1)) + (s * x1)) + ( - (s * x2))) - (a * (x3 - x2))) by Th12

        .= ((((t * (x3 - x1)) - (s * x2)) + (s * x1)) - (a * (x3 - x2))) by RVSUM_1: 15

        .= (((t * (x3 - x1)) - ((s * x2) - (s * x1))) - (a * (x3 - x2))) by Th4

        .= (((t * (x3 - x1)) - (s * (x2 - x1))) - (a * (x3 - x2))) by Th12

        .= (((t * (x3 - x1)) - (s * (x2 - x1))) - (a * ((x3 - ( 0* n)) - x2))) by RVSUM_1: 32

        .= (((t * (x3 - x1)) - (s * (x2 - x1))) - (a * ((x3 - (x1 - x1)) - x2))) by Th2

        .= (((t * (x3 - x1)) - (s * (x2 - x1))) - (a * (((x3 - x1) + x1) + ( - x2)))) by Th4

        .= (((t * (x3 - x1)) - (s * (x2 - x1))) - (a * ((x3 - x1) + (( - x2) + x1)))) by RVSUM_1: 15

        .= (((t * (x3 - x1)) - (s * (x2 - x1))) - ((a * (x3 - x1)) + (a * (( - x2) + x1)))) by EUCLID_4: 6

        .= ((((t * (x3 - x1)) - (s * (x2 - x1))) - (a * (x3 - x1))) - (a * (( - x2) + x1))) by RVSUM_1: 39

        .= (((t * (x3 - x1)) - ((a * (x3 - x1)) + (s * (x2 - x1)))) - (a * (( - x2) + x1))) by RVSUM_1: 39

        .= ((((t * (x3 - x1)) - (a * (x3 - x1))) - (s * (x2 - x1))) - (a * (( - x2) + x1))) by RVSUM_1: 39

        .= ((((t - a) * (x3 - x1)) - (s * (x2 - x1))) - (a * (( - x2) + x1))) by Th11

        .= ((((t - a) * (x3 - x1)) - (s * (x2 - x1))) - ((a * ( - x2)) + (a * x1))) by EUCLID_4: 6

        .= ((((t - a) * (x3 - x1)) - (s * (x2 - x1))) - (( - (a * x2)) + (a * x1))) by Th3

        .= (((((t - a) * (x3 - x1)) - (s * (x2 - x1))) - ( - (a * x2))) - (a * x1)) by RVSUM_1: 39

        .= ((((t - a) * (x3 - x1)) - (s * (x2 - x1))) + ((a * x2) + ( - (a * x1)))) by RVSUM_1: 15

        .= ((((t - a) * (x3 - x1)) - (s * (x2 - x1))) + (a * (x2 - x1))) by Th12

        .= (((t - a) * (x3 - x1)) - ((s * (x2 - x1)) - (a * (x2 - x1)))) by Th4

        .= (((t - a) * (x3 - x1)) + ( - ((s - a) * (x2 - x1)))) by Th11

        .= (((t - a) * (x3 - x1)) + (( - (s - a)) * (x2 - x1))) by Th3

        .= (((t - a) * (x3 - x1)) + ((a - s) * (x2 - x1)));

        then (t - a) = 0 by A1;

        

        then

         A15: (y3 - x1) = ((((1 * x1) + ( - (a * x1))) + (a * x3)) - x1) by A10, Th11

        .= (((x1 + ( - (a * x1))) + (a * x3)) - x1) by EUCLID_4: 3

        .= (((( - (a * x1)) + (a * x3)) + x1) - x1) by RVSUM_1: 15

        .= ((( - (a * x1)) + (a * x3)) + (x1 - x1)) by Th5

        .= ((( - (a * x1)) + (a * x3)) + ( 0* n)) by Th2

        .= (( - (a * x1)) + (a * x3)) by EUCLID_4: 1

        .= (a * (x3 - x1)) by Th12;

        (a - s) = 0 by A1, A14;

        

        then

         A16: (y2 - x1) = ((((1 * x1) + ( - (a * x1))) + (a * x2)) - x1) by A13, Th11

        .= (((x1 + ( - (a * x1))) + (a * x2)) - x1) by EUCLID_4: 3

        .= (((( - (a * x1)) + (a * x2)) + x1) - x1) by RVSUM_1: 15

        .= ((( - (a * x1)) + (a * x2)) + (x1 - x1)) by Th5

        .= ((( - (a * x1)) + (a * x2)) + ( 0* n)) by Th2

        .= (( - (a * x1)) + (a * x2)) by EUCLID_4: 1

        .= (a * (x2 - x1)) by Th12;

        (y3 - y2) <> ( 0* n) by A11;

        hence thesis by A12, A16, A15, EUCLID_4: 3;

      end;

      now

        assume ex a st a <> 0 & (y2 - x1) = (a * (x2 - x1)) & (y3 - x1) = (a * (x3 - x1));

        then

        consider a such that

         A17: a <> 0 and

         A18: (y2 - x1) = (a * (x2 - x1)) and

         A19: (y3 - x1) = (a * (x3 - x1));

        take a;

        take x2;

        take x3;

        take y2;

        take y3;

        x2 <> x3 by A1, Th37;

        then

         A20: (x3 - x2) <> ( 0* n) by Th9;

        

         A21: (y3 - y2) = ((x1 + (a * (x3 - x1))) - y2) by A19, Th6

        .= (((a * (x3 - x1)) + x1) - (x1 + (a * (x2 - x1)))) by A18, Th6

        .= ((((a * (x3 - x1)) + x1) - x1) - (a * (x2 - x1))) by RVSUM_1: 39

        .= (((a * (x3 - x1)) + (x1 - x1)) - (a * (x2 - x1))) by Th5

        .= (((a * (x3 - x1)) + ( 0* n)) - (a * (x2 - x1))) by Th2

        .= ((a * (x3 - x1)) - (a * (x2 - x1))) by EUCLID_4: 1

        .= (((a * x3) + ( - (a * x1))) - (a * (x2 - x1))) by Th12

        .= (((a * x3) + ( - (a * x1))) - (( - (a * x1)) + (a * x2))) by Th12

        .= ((((a * x3) + ( - (a * x1))) - ( - (a * x1))) - (a * x2)) by RVSUM_1: 39

        .= (((a * x3) + (( - (a * x1)) - ( - (a * x1)))) - (a * x2)) by Th5

        .= (((a * x3) + ( 0* n)) - (a * x2)) by Th2

        .= ((a * x3) - (a * x2)) by EUCLID_4: 1

        .= (a * (x3 - x2)) by Th12;

        then (y3 - y2) <> ( 0* n) by A17, A20, EUCLID_4: 5;

        then (y3 - y2) // (x3 - x2) by A21, A20;

        hence L1 // L2 by A4, A5;

      end;

      hence thesis;

    end;

    theorem :: EUCLIDLP:79

    

     Th79: for L1, L2 st L1 is being_line & L2 is being_line & L1 <> L2 holds ex x st x in L1 & not x in L2

    proof

      let L1, L2;

      assume that

       A1: L1 is being_line and

       A2: L2 is being_line;

      consider x1, x2 such that

       A3: x1 <> x2 and

       A4: L1 = ( Line (x1,x2)) by A1;

      assume

       A5: L1 <> L2;

      now

        per cases by A2, A3, A4, A5, Th30;

          case

           A6: not x1 in L2;

          set x = x1;

          thus x in L1 & not x in L2 by A4, A6, EUCLID_4: 9;

        end;

          case

           A7: not x2 in L2;

          set x = x2;

          thus x in L1 & not x in L2 by A4, A7, EUCLID_4: 9;

        end;

      end;

      hence thesis;

    end;

    theorem :: EUCLIDLP:80

    

     Th80: for x, L1, L2 st L1 _|_ L2 holds ex L0 st x in L0 & L0 _|_ L2 & L0 // L1

    proof

      let x, L1, L2;

      assume

       A1: L1 _|_ L2;

      then L1 is being_line by Th67;

      then

      consider L0 such that

       A2: x in L0 & L0 // L1 by Th72;

      take L0;

      thus thesis by A1, A2, Th61;

    end;

    theorem :: EUCLIDLP:81

    

     Th81: for x, L1, L2 st x in L2 & L1 _|_ L2 holds ex x0 st x <> x0 & x0 in L1 & not x0 in L2

    proof

      let x, L1, L2;

      assume that

       A1: x in L2 and

       A2: L1 _|_ L2;

      L1 is being_line & L2 is being_line by A2, Th67;

      then ex x0 st x0 in L1 & not x0 in L2 by A2, Th75, Th79;

      hence thesis by A1;

    end;

    definition

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

      :: EUCLIDLP:def9

      func plane (x1,x2,x3) -> Subset of ( REAL n) equals { x where x be Element of ( REAL n) : ex a1,a2,a3 be Real st ((a1 + a2) + a3) = 1 & x = (((a1 * x1) + (a2 * x2)) + (a3 * x3)) };

      correctness

      proof

        set A = { x where x be Element of ( REAL n) : ex a1,a2,a3 be Real st ((a1 + a2) + a3) = 1 & x = (((a1 * x1) + (a2 * x2)) + (a3 * x3)) };

        A c= ( REAL n)

        proof

          let x be object;

          assume x in A;

          then ex x9 be Element of ( REAL n) st x = x9 & ex a1,a2,a3 be Real st ((a1 + a2) + a3) = 1 & x9 = (((a1 * x1) + (a2 * x2)) + (a3 * x3));

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

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

      cluster ( plane (x1,x2,x3)) -> non empty;

      coherence

      proof

        

         A1: ( 0 * x3) = ( 0* n) by EUCLID_4: 3;

        

         A2: ((1 + 0 ) + 0 ) = 1;

        (1 * x1) = x1 & ( 0 * x2) = ( 0* n) by EUCLID_4: 3;

        

        then (((1 * x1) + ( 0 * x2)) + ( 0 * x3)) = (x1 + ( 0* n)) by A1, EUCLID_4: 1

        .= x1 by EUCLID_4: 1;

        then x1 in ( plane (x1,x2,x3)) by A2;

        hence thesis;

      end;

    end

    definition

      let n;

      let A be Subset of ( REAL n);

      :: EUCLIDLP:def10

      attr A is being_plane means ex x1, x2, x3 st ((x2 - x1),(x3 - x1)) are_lindependent2 & A = ( plane (x1,x2,x3));

    end

    theorem :: EUCLIDLP:82

    

     Th82: x1 in ( plane (x1,x2,x3)) & x2 in ( plane (x1,x2,x3)) & x3 in ( plane (x1,x2,x3))

    proof

      

       A1: ( 0 * x3) = ( 0* n) by EUCLID_4: 3;

      (1 * x1) = x1 & ( 0 * x2) = ( 0* n) by EUCLID_4: 3;

      

      then

       A2: (((1 * x1) + ( 0 * x2)) + ( 0 * x3)) = (x1 + ( 0* n)) by A1, EUCLID_4: 1

      .= x1 by EUCLID_4: 1;

      

       A3: ( 0 * x3) = ( 0* n) by EUCLID_4: 3;

      

       A4: (1 * x3) = x3 by EUCLID_4: 3;

      ( 0 * x1) = ( 0* n) & ( 0 * x2) = ( 0* n) by EUCLID_4: 3;

      

      then

       A5: ((( 0 * x1) + ( 0 * x2)) + (1 * x3)) = (( 0* n) + x3) by A4, EUCLID_4: 1

      .= x3 by EUCLID_4: 1;

      ( 0 * x1) = ( 0* n) & (1 * x2) = x2 by EUCLID_4: 3;

      

      then

       A6: ((( 0 * x1) + (1 * x2)) + ( 0 * x3)) = (x2 + ( 0* n)) by A3, EUCLID_4: 1

      .= x2 by EUCLID_4: 1;

      (( 0 + 0 ) + 1) = 1;

      hence thesis by A2, A6, A5;

    end;

    theorem :: EUCLIDLP:83

    

     Th83: x1 in ( plane (y1,y2,y3)) & x2 in ( plane (y1,y2,y3)) & x3 in ( plane (y1,y2,y3)) implies ( plane (x1,x2,x3)) c= ( plane (y1,y2,y3))

    proof

      assume that

       A1: x1 in ( plane (y1,y2,y3)) and

       A2: x2 in ( plane (y1,y2,y3)) and

       A3: x3 in ( plane (y1,y2,y3));

      ex x29 be Element of ( REAL n) st x2 = x29 & ex a21,a22,a23 be Real st ((a21 + a22) + a23) = 1 & x29 = (((a21 * y1) + (a22 * y2)) + (a23 * y3)) by A2;

      then

      consider a21,a22,a23 be Real such that

       A4: ((a21 + a22) + a23) = 1 and

       A5: x2 = (((a21 * y1) + (a22 * y2)) + (a23 * y3));

      ex x19 be Element of ( REAL n) st x1 = x19 & ex a11,a12,a13 be Real st ((a11 + a12) + a13) = 1 & x19 = (((a11 * y1) + (a12 * y2)) + (a13 * y3)) by A1;

      then

      consider a11,a12,a13 be Real such that

       A6: ((a11 + a12) + a13) = 1 and

       A7: x1 = (((a11 * y1) + (a12 * y2)) + (a13 * y3));

      let x be object;

      assume x in ( plane (x1,x2,x3));

      then ex x9 be Element of ( REAL n) st x = x9 & ex b1,b2,b3 be Real st ((b1 + b2) + b3) = 1 & x9 = (((b1 * x1) + (b2 * x2)) + (b3 * x3));

      then

      consider b1,b2,b3 be Real such that

       A8: ((b1 + b2) + b3) = 1 and

       A9: x = (((b1 * x1) + (b2 * x2)) + (b3 * x3));

      ex x39 be Element of ( REAL n) st x3 = x39 & ex a31,a32,a33 be Real st ((a31 + a32) + a33) = 1 & x39 = (((a31 * y1) + (a32 * y2)) + (a33 * y3)) by A3;

      then

      consider a31,a32,a33 be Real such that

       A10: ((a31 + a32) + a33) = 1 and

       A11: x3 = (((a31 * y1) + (a32 * y2)) + (a33 * y3));

      

       A12: (((((b1 * a11) + (b2 * a21)) + (b3 * a31)) + (((b1 * a12) + (b2 * a22)) + (b3 * a32))) + (((b1 * a13) + (b2 * a23)) + (b3 * a33))) = (((b1 * ((a11 + a12) + a13)) + (b2 * ((a21 + a22) + a23))) + (b3 * ((a31 + a32) + a33)))

      .= 1 by A6, A4, A10, A8;

      x = ((((((b1 * a11) * y1) + ((b1 * a12) * y2)) + ((b1 * a13) * y3)) + (b2 * (((a21 * y1) + (a22 * y2)) + (a23 * y3)))) + (b3 * (((a31 * y1) + (a32 * y2)) + (a33 * y3)))) by A7, A5, A11, A9, Th22

      .= ((((((b1 * a11) * y1) + ((b1 * a12) * y2)) + ((b1 * a13) * y3)) + ((((b2 * a21) * y1) + ((b2 * a22) * y2)) + ((b2 * a23) * y3))) + (b3 * (((a31 * y1) + (a32 * y2)) + (a33 * y3)))) by Th22

      .= ((((((b1 * a11) * y1) + ((b1 * a12) * y2)) + ((b1 * a13) * y3)) + ((((b2 * a21) * y1) + ((b2 * a22) * y2)) + ((b2 * a23) * y3))) + ((((b3 * a31) * y1) + ((b3 * a32) * y2)) + ((b3 * a33) * y3))) by Th22

      .= ((((((b1 * a11) + (b2 * a21)) * y1) + (((b1 * a12) + (b2 * a22)) * y2)) + (((b1 * a13) + (b2 * a23)) * y3)) + ((((b3 * a31) * y1) + ((b3 * a32) * y2)) + ((b3 * a33) * y3))) by Th24

      .= ((((((b1 * a11) + (b2 * a21)) + (b3 * a31)) * y1) + ((((b1 * a12) + (b2 * a22)) + (b3 * a32)) * y2)) + ((((b1 * a13) + (b2 * a23)) + (b3 * a33)) * y3)) by Th24;

      hence thesis by A12;

    end;

    theorem :: EUCLIDLP:84

    for A be Subset of ( REAL n), x, x1, x2, x3 st x in ( plane (x1,x2,x3)) & ex c1,c2,c3 be Real st ((c1 + c2) + c3) = 0 & x = (((c1 * x1) + (c2 * x2)) + (c3 * x3)) holds ( 0* n) in ( plane (x1,x2,x3))

    proof

      let A be Subset of ( REAL n), x, x1, x2, x3;

      assume that

       A1: x in ( plane (x1,x2,x3)) and

       A2: ex c1,c2,c3 be Real st ((c1 + c2) + c3) = 0 & x = (((c1 * x1) + (c2 * x2)) + (c3 * x3));

      consider c1,c2,c3 be Real such that

       A3: ((c1 + c2) + c3) = 0 and

       A4: x = (((c1 * x1) + (c2 * x2)) + (c3 * x3)) by A2;

      ex x9 be Element of ( REAL n) st x = x9 & ex a1,a2,a3 be Real st ((a1 + a2) + a3) = 1 & x9 = (((a1 * x1) + (a2 * x2)) + (a3 * x3)) by A1;

      then

      consider a1,a2,a3 be Real such that

       A5: ((a1 + a2) + a3) = 1 and

       A6: x = (((a1 * x1) + (a2 * x2)) + (a3 * x3));

      

       A7: (((a1 + ( - c1)) + (a2 + ( - c2))) + (a3 + ( - c3))) = 1 by A5, A3;

      ( 0* n) = (x - x) by Th2

      .= ((((a1 * x1) + (a2 * x2)) + (a3 * x3)) + (((( - c1) * x1) + (( - c2) * x2)) + (( - c3) * x3))) by A6, A4, Th14

      .= ((((a1 + ( - c1)) * x1) + ((a2 + ( - c2)) * x2)) + ((a3 + ( - c3)) * x3)) by Th24;

      hence thesis by A7;

    end;

    theorem :: EUCLIDLP:85

    

     Th85: y1 in ( plane (x1,x2,x3)) & y2 in ( plane (x1,x2,x3)) implies ( Line (y1,y2)) c= ( plane (x1,x2,x3))

    proof

      assume that

       A1: y1 in ( plane (x1,x2,x3)) and

       A2: y2 in ( plane (x1,x2,x3));

      consider y29 be Element of ( REAL n) such that

       A3: y2 = y29 and

       A4: ex a21,a22,a23 be Real st ((a21 + a22) + a23) = 1 & y29 = (((a21 * x1) + (a22 * x2)) + (a23 * x3)) by A2;

      consider y19 be Element of ( REAL n) such that

       A5: y1 = y19 and

       A6: ex a11,a12,a13 be Real st ((a11 + a12) + a13) = 1 & y19 = (((a11 * x1) + (a12 * x2)) + (a13 * x3)) by A1;

      ( Line (y1,y2)) c= ( plane (x1,x2,x3))

      proof

        let x be object;

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

        then

        consider t such that

         A7: x = (((1 - t) * y1) + (t * y2));

        consider a21,a22,a23 be Real such that

         A8: ((a21 + a22) + a23) = 1 and

         A9: y29 = (((a21 * x1) + (a22 * x2)) + (a23 * x3)) by A4;

        consider a11,a12,a13 be Real such that

         A10: ((a11 + a12) + a13) = 1 and

         A11: y19 = (((a11 * x1) + (a12 * x2)) + (a13 * x3)) by A6;

        

         A12: (((((1 - t) * a11) + (t * a21)) + (((1 - t) * a12) + (t * a22))) + (((1 - t) * a13) + (t * a23))) = (((1 - t) * ((a11 + a12) + a13)) + (t * ((a21 + a22) + a23)))

        .= ((1 - t) + t) by A10, A8

        .= 1;

        x = ((((((1 - t) * a11) * x1) + (((1 - t) * a12) * x2)) + (((1 - t) * a13) * x3)) + (t * (((a21 * x1) + (a22 * x2)) + (a23 * x3)))) by A5, A3, A7, A11, A9, Th22

        .= ((((((1 - t) * a11) * x1) + (((1 - t) * a12) * x2)) + (((1 - t) * a13) * x3)) + ((((t * a21) * x1) + ((t * a22) * x2)) + ((t * a23) * x3))) by Th22

        .= ((((((1 - t) * a11) + (t * a21)) * x1) + ((((1 - t) * a12) + (t * a22)) * x2)) + ((((1 - t) * a13) + (t * a23)) * x3)) by Th24;

        hence thesis by A12;

      end;

      hence thesis;

    end;

    theorem :: EUCLIDLP:86

    for A be Subset of ( REAL n), x st A is being_plane & x in A & ex a st a <> 1 & (a * x) in A holds ( 0* n) in A

    proof

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

      assume that

       A1: A is being_plane and

       A2: x in A and

       A3: ex a st a <> 1 & (a * x) in A;

      consider a such that

       A4: a <> 1 and

       A5: (a * x) in A by A3;

      

       A6: (1 - a) <> 0 by A4;

      

       A7: ((1 - (1 / (1 - a))) + ((1 / (1 - a)) * a)) = ((1 - (1 / (1 - a))) + (a / (1 - a))) by XCMPLX_1: 99

      .= (1 + (( - (1 / (1 - a))) + (a / (1 - a))))

      .= (1 + ((( - 1) / (1 - a)) + (a / (1 - a)))) by XCMPLX_1: 187

      .= (1 + ((( - 1) + a) / (1 - a))) by XCMPLX_1: 62

      .= (1 + (( - (( - a) - ( - 1))) / (1 - a)))

      .= (1 + ( - ((1 - a) / (1 - a)))) by XCMPLX_1: 187

      .= (1 - ((1 - a) / (1 - a)))

      .= (1 - 1) by A6, XCMPLX_1: 60

      .= 0 ;

      ( 0* n) = ( 0 * x) by EUCLID_4: 3

      .= (((1 - (1 / (1 - a))) * x) + (((1 / (1 - a)) * a) * x)) by A7, EUCLID_4: 7

      .= (((1 - (1 / (1 - a))) * x) + ((1 / (1 - a)) * (a * x))) by EUCLID_4: 4;

      then

       A8: ( 0* n) in ( Line (x,(a * x)));

      ex x1, x2, x3 st ((x2 - x1),(x3 - x1)) are_lindependent2 & A = ( plane (x1,x2,x3)) by A1;

      then ( Line (x,(a * x))) c= A by A2, A5, Th85;

      hence thesis by A8;

    end;

    theorem :: EUCLIDLP:87

    x in ( plane (x1,x2,x3)) & x = (((a1 * x1) + (a2 * x2)) + (a3 * x3)) implies ((a1 + a2) + a3) = 1 or ( 0* n) in ( plane (x1,x2,x3))

    proof

      assume that

       A1: x in ( plane (x1,x2,x3)) and

       A2: x = (((a1 * x1) + (a2 * x2)) + (a3 * x3)) and

       A3: not ((a1 + a2) + a3) = 1;

      ex x9 be Element of ( REAL n) st x = x9 & ex a19,a29,a39 be Real st ((a19 + a29) + a39) = 1 & x9 = (((a19 * x1) + (a29 * x2)) + (a39 * x3)) by A1;

      then

      consider a19,a29,a39 be Real such that

       A4: ((a19 + a29) + a39) = 1 and

       A5: x = (((a19 * x1) + (a29 * x2)) + (a39 * x3));

      

       A6: (((a1 - a19) + (a2 - a29)) + (a3 - a39)) <> 0 by A3, A4;

      set t = (((a1 - a19) + (a2 - a29)) + (a3 - a39));

      

       A7: ((((a1 - a19) / t) + ((a2 - a29) / t)) + ((a3 - a39) / t)) = ((((a1 - a19) + (a2 - a29)) + (a3 - a39)) / t) by XCMPLX_1: 63

      .= 1 by A6, XCMPLX_1: 60;

      

       A8: ( 0* n) = ((((a1 * x1) + (a2 * x2)) + (a3 * x3)) - (((a19 * x1) + (a29 * x2)) + (a39 * x3))) by A2, A5, Th2

      .= ((((a1 - a19) * x1) + ((a2 - a29) * x2)) + ((a3 - a39) * x3)) by Th26;

      ( 0* n) = ((1 / t) * ( 0* n)) by EUCLID_4: 2

      .= (((((1 / t) * (a1 - a19)) * x1) + (((1 / t) * (a2 - a29)) * x2)) + (((1 / t) * (a3 - a39)) * x3)) by A8, Th22

      .= (((((a1 - a19) / t) * x1) + (((1 / t) * (a2 - a29)) * x2)) + (((1 / t) * (a3 - a39)) * x3)) by XCMPLX_1: 99

      .= (((((a1 - a19) / t) * x1) + (((a2 - a29) / t) * x2)) + (((1 / t) * (a3 - a39)) * x3)) by XCMPLX_1: 99

      .= (((((a1 - a19) / t) * x1) + (((a2 - a29) / t) * x2)) + (((a3 - a39) / t) * x3)) by XCMPLX_1: 99;

      hence thesis by A7;

    end;

    theorem :: EUCLIDLP:88

    

     Th88: x in ( plane (x1,x2,x3)) iff ex a1, a2, a3 st ((a1 + a2) + a3) = 1 & x = (((a1 * x1) + (a2 * x2)) + (a3 * x3))

    proof

      thus x in ( plane (x1,x2,x3)) implies ex a1, a2, a3 st ((a1 + a2) + a3) = 1 & x = (((a1 * x1) + (a2 * x2)) + (a3 * x3))

      proof

        assume x in ( plane (x1,x2,x3));

        then ex x9 be Element of ( REAL n) st x = x9 & ex a19,a29,a39 be Real st ((a19 + a29) + a39) = 1 & x9 = (((a19 * x1) + (a29 * x2)) + (a39 * x3));

        hence thesis;

      end;

      thus thesis;

    end;

    theorem :: EUCLIDLP:89

    ((x2 - x1),(x3 - x1)) are_lindependent2 & ((a1 + a2) + a3) = 1 & x = (((a1 * x1) + (a2 * x2)) + (a3 * x3)) & ((b1 + b2) + b3) = 1 & x = (((b1 * x1) + (b2 * x2)) + (b3 * x3)) implies a1 = b1 & a2 = b2 & a3 = b3

    proof

      assume

       A1: ((x2 - x1),(x3 - x1)) are_lindependent2 ;

      assume that

       A2: ((a1 + a2) + a3) = 1 and

       A3: x = (((a1 * x1) + (a2 * x2)) + (a3 * x3)) and

       A4: ((b1 + b2) + b3) = 1 and

       A5: x = (((b1 * x1) + (b2 * x2)) + (b3 * x3));

      a1 = ((1 - a2) - a3) by A2;

      

      then x = (((((1 * x1) - (a2 * x1)) - (a3 * x1)) + (a2 * x2)) + (a3 * x3)) by A3, Th13

      .= ((((x1 + ( - (a2 * x1))) - (a3 * x1)) + (a2 * x2)) + (a3 * x3)) by EUCLID_4: 3

      .= ((((x1 + ( - (a2 * x1))) + (a2 * x2)) + ( - (a3 * x1))) + (a3 * x3)) by RVSUM_1: 15

      .= (((x1 + ((a2 * x2) + ( - (a2 * x1)))) + ( - (a3 * x1))) + (a3 * x3)) by RVSUM_1: 15

      .= ((x1 + ((a2 * x2) + ( - (a2 * x1)))) + ((a3 * x3) + ( - (a3 * x1)))) by RVSUM_1: 15

      .= ((x1 + ((a2 * x2) + (a2 * ( - x1)))) + ((a3 * x3) + ( - (a3 * x1)))) by Th3

      .= ((x1 + ((a2 * x2) + (a2 * ( - x1)))) + ((a3 * x3) + (a3 * ( - x1)))) by Th3

      .= ((x1 + (a2 * (x2 + ( - x1)))) + ((a3 * x3) + (a3 * ( - x1)))) by EUCLID_4: 6

      .= ((x1 + (a2 * (x2 - x1))) + (a3 * (x3 - x1))) by EUCLID_4: 6;

      then

       A6: (x - x1) = ((a2 * (x2 - x1)) + (a3 * (x3 - x1))) by Th7;

      x = (((((1 - b2) - b3) * x1) + (b2 * x2)) + (b3 * x3)) by A4, A5

      .= (((((1 * x1) - (b2 * x1)) - (b3 * x1)) + (b2 * x2)) + (b3 * x3)) by Th13

      .= ((((x1 + ( - (b2 * x1))) - (b3 * x1)) + (b2 * x2)) + (b3 * x3)) by EUCLID_4: 3

      .= ((((x1 + ( - (b2 * x1))) + (b2 * x2)) + ( - (b3 * x1))) + (b3 * x3)) by RVSUM_1: 15

      .= (((x1 + ((b2 * x2) + ( - (b2 * x1)))) + ( - (b3 * x1))) + (b3 * x3)) by RVSUM_1: 15

      .= ((x1 + ((b2 * x2) + ( - (b2 * x1)))) + ((b3 * x3) + ( - (b3 * x1)))) by RVSUM_1: 15

      .= ((x1 + ((b2 * x2) + (b2 * ( - x1)))) + ((b3 * x3) + ( - (b3 * x1)))) by Th3

      .= ((x1 + ((b2 * x2) + (b2 * ( - x1)))) + ((b3 * x3) + (b3 * ( - x1)))) by Th3

      .= ((x1 + (b2 * (x2 + ( - x1)))) + ((b3 * x3) + (b3 * ( - x1)))) by EUCLID_4: 6

      .= ((x1 + (b2 * (x2 - x1))) + (b3 * (x3 - x1))) by EUCLID_4: 6;

      then ((a2 * (x2 - x1)) + (a3 * (x3 - x1))) = ((b2 * (x2 - x1)) + (b3 * (x3 - x1))) by A6, Th7;

      then a2 = b2 & a3 = b3 by A1, Th35;

      hence thesis by A2, A4;

    end;

    definition

      let n;

      :: EUCLIDLP:def11

      func plane_of_REAL n -> Subset-Family of ( REAL n) equals { P where P be Subset of ( REAL n) : ex x1,x2,x3 be Element of ( REAL n) st P = ( plane (x1,x2,x3)) };

      correctness

      proof

        set A = { P where P be Subset of ( REAL n) : ex x1,x2,x3 be Element of ( REAL n) st P = ( plane (x1,x2,x3)) };

        A c= ( bool ( REAL n))

        proof

          let P be object;

          assume P in A;

          then ex P9 be Subset of ( REAL n) st P = P9 & ex x1,x2,x3 be Element of ( REAL n) st P9 = ( plane (x1,x2,x3));

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let n;

      cluster ( plane_of_REAL n) -> non empty;

      coherence

      proof

        reconsider P = ( plane (( 0* n),( 1* n),( 1* n))) as Subset of ( REAL n);

        P in ( plane_of_REAL n);

        hence thesis;

      end;

    end

    theorem :: EUCLIDLP:90

    

     Th90: ( plane (x1,x2,x3)) in ( plane_of_REAL n);

    reserve P,P0,P1,P2 for Element of ( plane_of_REAL n);

    theorem :: EUCLIDLP:91

    

     Th91: x1 in P & x2 in P & x3 in P implies ( plane (x1,x2,x3)) c= P

    proof

      P in ( plane_of_REAL n);

      then

       A1: ex P9 be Subset of ( REAL n) st P = P9 & ex y1,y2,y3 be Element of ( REAL n) st P9 = ( plane (y1,y2,y3));

      assume x1 in P & x2 in P & x3 in P;

      hence thesis by A1, Th83;

    end;

    theorem :: EUCLIDLP:92

    

     Th92: x1 in P & x2 in P & x3 in P & ((x2 - x1),(x3 - x1)) are_lindependent2 implies P = ( plane (x1,x2,x3))

    proof

      assume that

       A1: x1 in P and

       A2: x2 in P and

       A3: x3 in P and

       A4: ((x2 - x1),(x3 - x1)) are_lindependent2 ;

      P in ( plane_of_REAL n);

      then ex P9 be Subset of ( REAL n) st P = P9 & ex y1,y2,y3 be Element of ( REAL n) st P9 = ( plane (y1,y2,y3));

      then

      consider y1,y2,y3 be Element of ( REAL n) such that

       A5: P = ( plane (y1,y2,y3));

      ex x9 be Element of ( REAL n) st x2 = x9 & ex a19,a29,a39 be Real st ((a19 + a29) + a39) = 1 & x9 = (((a19 * y1) + (a29 * y2)) + (a39 * y3)) by A2, A5;

      then

      consider a21,a22,a23 be Real such that

       A6: ((a21 + a22) + a23) = 1 & x2 = (((a21 * y1) + (a22 * y2)) + (a23 * y3));

      ex x9 be Element of ( REAL n) st x1 = x9 & ex a19,a29,a39 be Real st ((a19 + a29) + a39) = 1 & x9 = (((a19 * y1) + (a29 * y2)) + (a39 * y3)) by A1, A5;

      then

      consider a11,a12,a13 be Real such that

       A7: ((a11 + a12) + a13) = 1 & x1 = (((a11 * y1) + (a12 * y2)) + (a13 * y3));

      ex x9 be Element of ( REAL n) st x3 = x9 & ex a19,a29,a39 be Real st ((a19 + a29) + a39) = 1 & x9 = (((a19 * y1) + (a29 * y2)) + (a39 * y3)) by A3, A5;

      then

      consider a31,a32,a33 be Real such that

       A8: ((a31 + a32) + a33) = 1 & x3 = (((a31 * y1) + (a32 * y2)) + (a33 * y3));

      x3 = ((y1 + (a32 * (y2 - y1))) + (a33 * (y3 - y1))) by A8, Th27;

      

      then

       A9: (x3 - x1) = (((y1 + (a32 * (y2 - y1))) + (a33 * (y3 - y1))) + ( - ((y1 + (a12 * (y2 - y1))) + (a13 * (y3 - y1))))) by A7, Th27

      .= (((y1 + (a32 * (y2 - y1))) + (a33 * (y3 - y1))) + ((( - y1) + ( - (a12 * (y2 - y1)))) + ( - (a13 * (y3 - y1))))) by Th8

      .= (((y1 + ( - y1)) + ((a32 * (y2 - y1)) + ( - (a12 * (y2 - y1))))) + ((a33 * (y3 - y1)) + ( - (a13 * (y3 - y1))))) by Th17

      .= ((( 0* n) + ((a32 * (y2 - y1)) + ( - (a12 * (y2 - y1))))) + ((a33 * (y3 - y1)) + ( - (a13 * (y3 - y1))))) by Th2

      .= ((( 0* n) + ((a32 - a12) * (y2 - y1))) + ((a33 * (y3 - y1)) + ( - (a13 * (y3 - y1))))) by Th11

      .= ((( 0* n) + ((a32 - a12) * (y2 - y1))) + ((a33 - a13) * (y3 - y1))) by Th11

      .= (((a32 - a12) * (y2 - y1)) + ((a33 - a13) * (y3 - y1))) by EUCLID_4: 1;

      

       A10: x1 = ((y1 + (a12 * (y2 - y1))) + (a13 * (y3 - y1))) by A7, Th27;

      

      then (x2 - x1) = (((y1 + (a22 * (y2 - y1))) + (a23 * (y3 - y1))) + ( - ((y1 + (a12 * (y2 - y1))) + (a13 * (y3 - y1))))) by A6, Th27

      .= (((y1 + (a22 * (y2 - y1))) + (a23 * (y3 - y1))) + ((( - y1) + ( - (a12 * (y2 - y1)))) + ( - (a13 * (y3 - y1))))) by Th8

      .= (((y1 + ( - y1)) + ((a22 * (y2 - y1)) + ( - (a12 * (y2 - y1))))) + ((a23 * (y3 - y1)) + ( - (a13 * (y3 - y1))))) by Th17

      .= ((( 0* n) + ((a22 * (y2 - y1)) + ( - (a12 * (y2 - y1))))) + ((a23 * (y3 - y1)) + ( - (a13 * (y3 - y1))))) by Th2

      .= ((( 0* n) + ((a22 - a12) * (y2 - y1))) + ((a23 * (y3 - y1)) + ( - (a13 * (y3 - y1))))) by Th11

      .= ((( 0* n) + ((a22 - a12) * (y2 - y1))) + ((a23 - a13) * (y3 - y1))) by Th11

      .= (((a22 - a12) * (y2 - y1)) + ((a23 - a13) * (y3 - y1))) by EUCLID_4: 1;

      then

      consider c1,c2,d1,d2 be Real such that

       A11: (y2 - y1) = ((c1 * (x2 - x1)) + (c2 * (x3 - x1))) & (y3 - y1) = ((d1 * (x2 - x1)) + (d2 * (x3 - x1))) by A4, A9, Th36;

      

       A12: x1 = (y1 + ((a12 * (y2 - y1)) + (a13 * (y3 - y1)))) by A10, RVSUM_1: 15;

      now

        let y be object;

        assume y in P;

        then ex x9 be Element of ( REAL n) st y = x9 & ex a19,a29,a39 be Real st ((a19 + a29) + a39) = 1 & x9 = (((a19 * y1) + (a29 * y2)) + (a39 * y3)) by A5;

        then

        consider b1,b2,b3 be Real such that

         A13: ((b1 + b2) + b3) = 1 & y = (((b1 * y1) + (b2 * y2)) + (b3 * y3));

        y = ((y1 + (b2 * (y2 - y1))) + (b3 * (y3 - y1))) by A13, Th27

        .= (((x1 - ((a12 * (y2 - y1)) + (a13 * (y3 - y1)))) + (b2 * (y2 - y1))) + (b3 * (y3 - y1))) by A12, Th6

        .= ((((x1 - (a12 * (y2 - y1))) - (a13 * (y3 - y1))) + (b2 * (y2 - y1))) + (b3 * (y3 - y1))) by RVSUM_1: 39

        .= ((((x1 + ( - (a12 * (y2 - y1)))) + (b2 * (y2 - y1))) + ( - (a13 * (y3 - y1)))) + (b3 * (y3 - y1))) by RVSUM_1: 15

        .= (((x1 + (( - (a12 * (y2 - y1))) + (b2 * (y2 - y1)))) + ( - (a13 * (y3 - y1)))) + (b3 * (y3 - y1))) by RVSUM_1: 15

        .= ((x1 + (( - (a12 * (y2 - y1))) + (b2 * (y2 - y1)))) + (( - (a13 * (y3 - y1))) + (b3 * (y3 - y1)))) by RVSUM_1: 15

        .= ((x1 + ((b2 - a12) * (y2 - y1))) + (( - (a13 * (y3 - y1))) + (b3 * (y3 - y1)))) by Th11

        .= ((x1 + ((b2 - a12) * (y2 - y1))) + ((b3 - a13) * (y3 - y1))) by Th11

        .= ((x1 + (((b2 - a12) * (c1 * (x2 - x1))) + ((b2 - a12) * (c2 * (x3 - x1))))) + ((b3 - a13) * ((d1 * (x2 - x1)) + (d2 * (x3 - x1))))) by A11, EUCLID_4: 6

        .= ((x1 + (((b2 - a12) * (c1 * (x2 - x1))) + ((b2 - a12) * (c2 * (x3 - x1))))) + (((b3 - a13) * (d1 * (x2 - x1))) + ((b3 - a13) * (d2 * (x3 - x1))))) by EUCLID_4: 6

        .= ((x1 + ((((b2 - a12) * c1) * (x2 - x1)) + ((b2 - a12) * (c2 * (x3 - x1))))) + (((b3 - a13) * (d1 * (x2 - x1))) + ((b3 - a13) * (d2 * (x3 - x1))))) by EUCLID_4: 4

        .= ((x1 + ((((b2 - a12) * c1) * (x2 - x1)) + (((b2 - a12) * c2) * (x3 - x1)))) + (((b3 - a13) * (d1 * (x2 - x1))) + ((b3 - a13) * (d2 * (x3 - x1))))) by EUCLID_4: 4

        .= ((x1 + ((((b2 - a12) * c1) * (x2 - x1)) + (((b2 - a12) * c2) * (x3 - x1)))) + ((((b3 - a13) * d1) * (x2 - x1)) + ((b3 - a13) * (d2 * (x3 - x1))))) by EUCLID_4: 4

        .= ((x1 + ((((b2 - a12) * c1) * (x2 - x1)) + (((b2 - a12) * c2) * (x3 - x1)))) + ((((b3 - a13) * d1) * (x2 - x1)) + (((b3 - a13) * d2) * (x3 - x1)))) by EUCLID_4: 4

        .= (((x1 + (((b2 - a12) * c1) * (x2 - x1))) + (((b2 - a12) * c2) * (x3 - x1))) + ((((b3 - a13) * d1) * (x2 - x1)) + (((b3 - a13) * d2) * (x3 - x1)))) by RVSUM_1: 15

        .= ((((x1 + (((b2 - a12) * c1) * (x2 - x1))) + (((b2 - a12) * c2) * (x3 - x1))) + (((b3 - a13) * d1) * (x2 - x1))) + (((b3 - a13) * d2) * (x3 - x1))) by RVSUM_1: 15

        .= ((((x1 + (((b2 - a12) * c1) * (x2 - x1))) + (((b3 - a13) * d1) * (x2 - x1))) + (((b2 - a12) * c2) * (x3 - x1))) + (((b3 - a13) * d2) * (x3 - x1))) by RVSUM_1: 15

        .= (((x1 + ((((b2 - a12) * c1) * (x2 - x1)) + (((b3 - a13) * d1) * (x2 - x1)))) + (((b2 - a12) * c2) * (x3 - x1))) + (((b3 - a13) * d2) * (x3 - x1))) by RVSUM_1: 15

        .= ((x1 + ((((b2 - a12) * c1) * (x2 - x1)) + (((b3 - a13) * d1) * (x2 - x1)))) + ((((b2 - a12) * c2) * (x3 - x1)) + (((b3 - a13) * d2) * (x3 - x1)))) by RVSUM_1: 15

        .= ((x1 + ((((b2 - a12) * c1) + ((b3 - a13) * d1)) * (x2 - x1))) + ((((b2 - a12) * c2) * (x3 - x1)) + (((b3 - a13) * d2) * (x3 - x1)))) by EUCLID_4: 7

        .= ((x1 + ((((b2 - a12) * c1) + ((b3 - a13) * d1)) * (x2 - x1))) + ((((b2 - a12) * c2) + ((b3 - a13) * d2)) * (x3 - x1))) by EUCLID_4: 7;

        then ex a be Real st y = (((a * x1) + ((((b2 - a12) * c1) + ((b3 - a13) * d1)) * x2)) + ((((b2 - a12) * c2) + ((b3 - a13) * d2)) * x3)) & ((a + (((b2 - a12) * c1) + ((b3 - a13) * d1))) + (((b2 - a12) * c2) + ((b3 - a13) * d2))) = 1 by Th28;

        hence y in ( plane (x1,x2,x3));

      end;

      then

       A14: P c= ( plane (x1,x2,x3));

      ( plane (x1,x2,x3)) c= P by A1, A2, A3, A5, Th83;

      hence thesis by A14, XBOOLE_0:def 10;

    end;

    theorem :: EUCLIDLP:93

    P1 is being_plane & P1 c= P2 implies P1 = P2

    proof

      assume that

       A1: P1 is being_plane and

       A2: P1 c= P2;

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

       A3: ((x2 - x1),(x3 - x1)) are_lindependent2 & P1 = ( plane (x1,x2,x3)) by A1;

      

       A4: x3 in ( plane (x1,x2,x3)) by Th82;

      x1 in ( plane (x1,x2,x3)) & x2 in ( plane (x1,x2,x3)) by Th82;

      hence thesis by A2, A3, A4, Th92;

    end;

    theorem :: EUCLIDLP:94

    ( Line (x1,x2)) c= ( plane (x1,x2,x3)) & ( Line (x2,x3)) c= ( plane (x1,x2,x3)) & ( Line (x3,x1)) c= ( plane (x1,x2,x3))

    proof

      

       A1: x3 in ( plane (x1,x2,x3)) by Th82;

      x1 in ( plane (x1,x2,x3)) & x2 in ( plane (x1,x2,x3)) by Th82;

      hence thesis by A1, Th85;

    end;

    theorem :: EUCLIDLP:95

    

     Th95: x1 in P & x2 in P implies ( Line (x1,x2)) c= P

    proof

      P in ( plane_of_REAL n);

      then

       A1: ex P9 be Subset of ( REAL n) st P = P9 & ex y1,y2,y3 be Element of ( REAL n) st P9 = ( plane (y1,y2,y3));

      assume x1 in P & x2 in P;

      hence thesis by A1, Th85;

    end;

    definition

      let n be Nat, L1,L2 be Element of ( line_of_REAL n);

      :: EUCLIDLP:def12

      pred L1,L2 are_coplane means ex x1,x2,x3 be Element of ( REAL n) st L1 c= ( plane (x1,x2,x3)) & L2 c= ( plane (x1,x2,x3));

    end

    theorem :: EUCLIDLP:96

    

     Th96: (L1,L2) are_coplane iff ex P st L1 c= P & L2 c= P

    proof

      thus (L1,L2) are_coplane implies ex P st L1 c= P & L2 c= P

      proof

        assume (L1,L2) are_coplane ;

        then

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

         A1: L1 c= ( plane (x1,x2,x3)) & L2 c= ( plane (x1,x2,x3));

        set P = ( plane (x1,x2,x3));

        take P;

        thus thesis by A1, Th90;

      end;

      now

        assume ex P st L1 c= P & L2 c= P;

        then

        consider P such that

         A2: L1 c= P & L2 c= P;

        P in ( plane_of_REAL n);

        then ex P9 be Subset of ( REAL n) st P = P9 & ex x1,x2,x3 be Element of ( REAL n) st P9 = ( plane (x1,x2,x3));

        hence (L1,L2) are_coplane by A2;

      end;

      hence thesis;

    end;

    theorem :: EUCLIDLP:97

    

     Th97: L1 // L2 implies (L1,L2) are_coplane

    proof

      assume L1 // L2;

      then

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

       A1: L1 = ( Line (x1,x2)) and

       A2: L2 = ( Line (y1,y2)) and

       A3: (x2 - x1) // (y2 - y1);

      consider a such that a <> 0 and

       A4: (x2 - x1) = (a * (y2 - y1)) by A3, Th32;

      

       A5: ((1 + ( - a)) + a) = 1;

      y1 in ( plane (x1,y1,y2)) & y2 in ( plane (x1,y1,y2)) by Th82;

      then

       A6: L2 c= ( plane (x1,y1,y2)) by A2, Th85;

      x2 = (x1 + (a * (y2 - y1))) by A4, Th6

      .= ((1 * x1) + (a * (y2 - y1))) by EUCLID_4: 3

      .= ((1 * x1) + ((a * y2) + (( - a) * y1))) by Th12

      .= (((1 * x1) + (( - a) * y1)) + (a * y2)) by RVSUM_1: 15;

      then

       A7: x2 in ( plane (x1,y1,y2)) by A5;

      x1 in ( plane (x1,y1,y2)) by Th82;

      then L1 c= ( plane (x1,y1,y2)) by A1, A7, Th85;

      hence thesis by A6;

    end;

    theorem :: EUCLIDLP:98

    

     Th98: L1 is being_line & L2 is being_line & (L1,L2) are_coplane & L1 misses L2 implies ex P st L1 c= P & L2 c= P & P is being_plane

    proof

      assume that

       A1: L1 is being_line and

       A2: L2 is being_line and

       A3: (L1,L2) are_coplane ;

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

       A4: L1 c= ( plane (x1,x2,x3)) & L2 c= ( plane (x1,x2,x3)) by A3;

      consider y2, y3 such that y2 <> y3 and

       A5: L2 = ( Line (y2,y3)) by A2;

      consider y0, y1 such that

       A6: y0 <> y1 and

       A7: L1 = ( Line (y0,y1)) by A1;

      

       A8: (y0 - y1) <> ( 0* n) by A6, Th9;

      set P = ( plane (x1,x2,x3));

      

       A9: y2 in L2 by A5, EUCLID_4: 9;

      consider y be Element of ( REAL n) such that

       A10: y in ( Line (y0,y1)) and

       A11: ((y0 - y1),(y2 - y)) are_orthogonal by Th43;

      assume L1 misses L2;

      then

       A12: y <> y2 by A7, A9, A10, XBOOLE_0: 3;

      then (y2 - y) <> ( 0* n) by Th9;

      then

       A13: (y0 - y1) _|_ (y2 - y) by A11, A8;

      consider y9 be Element of ( REAL n) such that

       A14: y <> y9 and

       A15: y9 in L1 by A1, EUCLID_4: 14;

      take P;

      y in ( Line (y,y2)) & y2 in ( Line (y,y2)) by EUCLID_4: 9;

      then

       A16: P in ( plane_of_REAL n) & ((y9 - y),(y2 - y)) are_lindependent2 by A7, A10, A12, A13, A14, A15, Th40, Th45;

      then P = ( plane (y,y9,y2)) by A4, A7, A9, A10, A15, Th92;

      hence thesis by A4, A16;

    end;

    theorem :: EUCLIDLP:99

    

     Th99: ex P st x in P & L c= P

    proof

      L in ( line_of_REAL n);

      then

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

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

      take P = ( plane (x,x1,x2));

      x1 in P & x2 in P by Th82;

      hence thesis by A1, Th82, Th85, Th90;

    end;

    theorem :: EUCLIDLP:100

    

     Th100: ( not x in L) & L is being_line implies ex P st x in P & L c= P & P is being_plane

    proof

      consider P be Element of ( plane_of_REAL n) such that

       A1: x in P & L c= P by Th99;

      assume ( not x in L) & L is being_line;

      then

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

       A2: L = ( Line (x1,x2)) and

       A3: ((x - x1),(x2 - x1)) are_lindependent2 by Th55;

      take P;

      x1 in L & x2 in L by A2, EUCLID_4: 9;

      then P = ( plane (x1,x,x2)) by A1, A3, Th92;

      hence thesis by A1, A3;

    end;

    theorem :: EUCLIDLP:101

    

     Th101: x in P & L c= P & ( not x in L) & L is being_line implies P is being_plane

    proof

      assume

       A1: x in P & L c= P;

      assume ( not x in L) & L is being_line;

      then

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

       A2: L = ( Line (x1,x2)) and

       A3: ((x - x1),(x2 - x1)) are_lindependent2 by Th55;

      x1 in L & x2 in L by A2, EUCLID_4: 9;

      then P = ( plane (x1,x,x2)) by A1, A3, Th92;

      hence thesis by A3;

    end;

    theorem :: EUCLIDLP:102

    

     Th102: ( not x in L) & L is being_line & x in P0 & L c= P0 & x in P1 & L c= P1 implies P0 = P1

    proof

      assume that

       A1: ( not x in L) & L is being_line and

       A2: x in P0 & L c= P0 and

       A3: x in P1 & L c= P1;

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

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

       A5: ((x - x1),(x2 - x1)) are_lindependent2 by A1, Th55;

      

       A6: x1 in L & x2 in L by A4, EUCLID_4: 9;

      then P0 = ( plane (x1,x,x2)) by A2, A5, Th92;

      hence thesis by A3, A5, A6, Th92;

    end;

    theorem :: EUCLIDLP:103

    L1 is being_line & L2 is being_line & (L1,L2) are_coplane & L1 <> L2 implies ex P st L1 c= P & L2 c= P & P is being_plane

    proof

      assume that

       A1: L1 is being_line and

       A2: L2 is being_line & (L1,L2) are_coplane & L1 <> L2;

      (ex P st L1 c= P & L2 c= P) & ex x st x in L2 & not x in L1 by A1, A2, Th79, Th96;

      hence thesis by A1, Th101;

    end;

    theorem :: EUCLIDLP:104

    for L1, L2 st L1 is being_line & L2 is being_line & L1 <> L2 & L1 meets L2 holds ex P st L1 c= P & L2 c= P & P is being_plane

    proof

      let L1, L2;

      assume that

       A1: L1 is being_line and

       A2: L2 is being_line and

       A3: L1 <> L2 and

       A4: L1 meets L2;

      consider x such that

       A5: x in L1 and

       A6: not x in L2 by A1, A2, A3, Th79;

      

       A7: ex P st x in P & L2 c= P & P is being_plane by A2, A6, Th100;

      consider y such that

       A8: y in L1 and

       A9: y in L2 by A4, Th49;

      L1 = ( Line (x,y)) by A1, A5, A6, A8, A9, Th30;

      hence thesis by A7, A9, Th95;

    end;

    theorem :: EUCLIDLP:105

    L1 is being_line & L2 is being_line & L1 <> L2 & L1 c= P1 & L2 c= P1 & L1 c= P2 & L2 c= P2 implies P1 = P2

    proof

      assume that

       A1: L1 is being_line and

       A2: L2 is being_line and

       A3: L1 <> L2 and

       A4: L1 c= P1 & L2 c= P1 and

       A5: L1 c= P2 & L2 c= P2;

      consider x such that

       A6: x in L1 and

       A7: not x in L2 by A1, A2, A3, Th79;

      consider x1, x2 such that

       A8: L2 = ( Line (x1,x2)) and

       A9: ((x - x1),(x2 - x1)) are_lindependent2 by A2, A7, Th55;

      

       A10: x1 in L2 & x2 in L2 by A8, EUCLID_4: 9;

      then P2 = ( plane (x1,x,x2)) by A5, A6, A9, Th92;

      hence thesis by A4, A6, A9, A10, Th92;

    end;

    theorem :: EUCLIDLP:106

    

     Th106: L1 // L2 & L1 <> L2 implies ex P st L1 c= P & L2 c= P & P is being_plane

    proof

      assume that

       A1: L1 // L2 and

       A2: L1 <> L2;

      

       A3: L2 is being_line by A1, Th66;

      (L1,L2) are_coplane & L1 is being_line by A1, Th66, Th97;

      hence thesis by A1, A2, A3, Th71, Th98;

    end;

    theorem :: EUCLIDLP:107

    

     Th107: L1 _|_ L2 & L1 meets L2 implies ex P st P is being_plane & L1 c= P & L2 c= P

    proof

      assume that

       A1: L1 _|_ L2 and

       A2: L1 meets L2;

      consider x1 such that

       A3: x1 in L1 and

       A4: x1 in L2 by A2, Th49;

      L1 is being_line by A1, Th67;

      then

      consider x2 such that

       A5: x2 <> x1 & x2 in L1 by Th53;

      

       A6: L1 = ( Line (x1,x2)) by A3, A5, Th64;

      L2 is being_line by A1, Th67;

      then

      consider x3 such that

       A7: x3 <> x1 & x3 in L2 by Th53;

      reconsider P = ( plane (x1,x2,x3)) as Subset of ( REAL n);

      take P;

      

       A8: x1 in P & x2 in P by Th82;

      

       A9: x3 in P by Th82;

      

       A10: L2 = ( Line (x1,x3)) by A4, A7, Th64;

      ((x2 - x1),(x3 - x1)) are_lindependent2 by A1, A3, A4, A5, A7, Th45, Th74;

      hence thesis by A6, A10, A8, A9, Th85, Th90;

    end;

    theorem :: EUCLIDLP:108

    

     Th108: L0 c= P & L1 c= P & L2 c= P & x in L0 & x in L1 & x in L2 & L0 _|_ L2 & L1 _|_ L2 implies L0 = L1

    proof

      assume that

       A1: L0 c= P and

       A2: L1 c= P and

       A3: L2 c= P and

       A4: x in L0 and

       A5: x in L1 and

       A6: x in L2;

      

       A7: L1 meets L0 by A4, A5, Th49;

      assume that

       A8: L0 _|_ L2 and

       A9: L1 _|_ L2;

      consider x0 such that

       A10: x <> x0 and

       A11: x0 in L0 and not x0 in L2 by A6, A8, Th81;

      L1 is being_line by A9, Th67;

      then

      consider x1 such that

       A12: x1 <> x and

       A13: x1 in L1 by Th53;

      consider x2 such that

       A14: x <> x2 and

       A15: x2 in L2 and not x2 in L1 by A5, A9, Th81;

      

       A16: (x0 - x) _|_ (x2 - x) by A4, A6, A8, A10, A11, A14, A15, Th74;

      then P = ( plane (x,x0,x2)) by A1, A3, A4, A11, A15, Th45, Th92;

      then

      consider a1, a2, a3 such that

       A17: ((a1 + a2) + a3) = 1 & x1 = (((a1 * x) + (a2 * x0)) + (a3 * x2)) by A2, A13, Th88;

      ((x0 - x),(x2 - x)) are_orthogonal by A16;

      then

       A18: |((x0 - x), (x2 - x))| = 0 by RVSUM_1:def 17;

      

       A19: (x1 - x) = (( - x) + ((x + (a2 * (x0 - x))) + (a3 * (x2 - x)))) by A17, Th27

      .= (( - x) + (x + ((a2 * (x0 - x)) + (a3 * (x2 - x))))) by RVSUM_1: 15

      .= ((( - x) + x) + ((a2 * (x0 - x)) + (a3 * (x2 - x)))) by RVSUM_1: 15

      .= (( 0* n) + ((a2 * (x0 - x)) + (a3 * (x2 - x)))) by Th2

      .= ((a2 * (x0 - x)) + (a3 * (x2 - x))) by EUCLID_4: 1;

      (x2 - x) <> ( 0* n) by A14, Th9;

      then

       A20: |((x2 - x), (x2 - x))| <> 0 by EUCLID_4: 17;

      (x1 - x) _|_ (x2 - x) by A5, A6, A9, A14, A15, A12, A13, Th74;

      then ((x1 - x),(x2 - x)) are_orthogonal ;

      

      then 0 = |(((a2 * (x0 - x)) + (a3 * (x2 - x))), (x2 - x))| by A19, RVSUM_1:def 17

      .= ( |((a2 * (x0 - x)), (x2 - x))| + |((a3 * (x2 - x)), (x2 - x))|) by EUCLID_4: 20

      .= ((a2 * |((x0 - x), (x2 - x))|) + |((a3 * (x2 - x)), (x2 - x))|) by EUCLID_4: 21

      .= (a3 * |((x2 - x), (x2 - x))|) by A18, EUCLID_4: 21;

      

      then

       A21: (x1 - x) = ((a2 * (x0 - x)) + ( 0 * (x2 - x))) by A19, A20, XCMPLX_1: 6

      .= ((a2 * (x0 - x)) + ( 0* n)) by EUCLID_4: 3

      .= (a2 * (x0 - x)) by EUCLID_4: 1;

      

       A22: (x0 - x) <> ( 0* n) by A10, Th9;

      (x1 - x) <> ( 0* n) by A12, Th9;

      then

       A23: (x1 - x) // (x0 - x) by A21, A22;

      

       A24: L1 = ( Line (x,x1)) by A5, A12, A13, Th64;

      L0 = ( Line (x,x0)) by A4, A10, A11, Th64;

      then L1 // L0 by A24, A23;

      hence thesis by A7, Th71;

    end;

    theorem :: EUCLIDLP:109

    

     Th109: (L1,L2) are_coplane & L1 _|_ L2 implies L1 meets L2

    proof

      assume

       A1: (L1,L2) are_coplane ;

      assume

       A2: L1 _|_ L2;

      then

       A3: L2 is being_line by Th67;

      L1 is being_line by A2, Th67;

      then

      consider x0 such that

       A4: x0 in L1 and

       A5: not x0 in L2 by A2, A3, Th75, Th79;

      consider L such that

       A6: x0 in L and

       A7: L _|_ L2 and

       A8: L meets L2 by A3, A5, Th62;

      consider x such that

       A9: x in L and

       A10: x in L2 by A8, Th49;

      x in L1

      proof

        

         A11: L1 meets L by A4, A6, Th49;

        consider P such that P is being_plane and

         A12: L c= P & L2 c= P by A7, A8, Th107;

        consider P0 such that

         A13: L1 c= P0 & L2 c= P0 by A1, Th96;

        

         A14: P = P0 by A3, A4, A5, A6, A13, A12, Th102;

        consider L0 such that

         A15: x in L0 and

         A16: L0 _|_ L2 and

         A17: L0 // L1 by A2, Th80;

        assume

         A18: not x in L1;

        then

        consider P1 such that

         A19: L0 c= P1 and

         A20: L1 c= P1 and P1 is being_plane by A15, A17, Th106;

        L1 is being_line by A17, Th66;

        then P = P1 by A10, A18, A13, A14, A15, A19, A20, Th102;

        then L = L0 by A7, A9, A10, A12, A15, A16, A19, Th108;

        hence contradiction by A18, A15, A17, A11, Th71;

      end;

      hence thesis by A10, Th49;

    end;

    theorem :: EUCLIDLP:110

    

     Th110: L1 c= P & L2 c= P & L1 _|_ L2 & x in P & L0 // L2 & x in L0 implies L0 c= P & L0 _|_ L1

    proof

      assume that

       A1: L1 c= P & L2 c= P and

       A2: L1 _|_ L2 and

       A3: x in P;

      (L1,L2) are_coplane by A1, Th96;

      then L1 meets L2 by A2, Th109;

      then

      consider x0 such that

       A4: x0 in L1 and

       A5: x0 in L2 by Th49;

      L2 is being_line by A2, Th67;

      then

      consider x1 such that

       A6: x1 <> x0 and

       A7: x1 in L2 by Th53;

      

       A8: ( plane (x,x1,x0)) c= P by A1, A3, A4, A7, Th91;

      assume that

       A9: L0 // L2 and

       A10: x in L0;

      L0 is being_line by A9, Th66;

      then

      consider x2 such that

       A11: x2 <> x & x2 in L0 by Th53;

      consider a such that a <> 0 and

       A12: (x2 - x) = (a * (x1 - x0)) by A9, A10, A5, A6, A7, A11, Th32, Th77;

      

       A13: ((1 + a) + ( - a)) = 1;

      x2 = (x + (a * (x1 - x0))) by A12, Th6

      .= ((1 * x) + (a * (x1 - x0))) by EUCLID_4: 3

      .= ((1 * x) + ((a * x1) + (( - a) * x0))) by Th12

      .= (((1 * x) + (a * x1)) + (( - a) * x0)) by RVSUM_1: 15;

      then

       A14: x2 in ( plane (x,x1,x0)) by A13;

      L0 = ( Line (x2,x)) by A10, A11, Th64;

      hence thesis by A2, A3, A9, A14, A8, Th61, Th95;

    end;

    theorem :: EUCLIDLP:111

    

     Th111: L c= P & L1 c= P & L2 c= P & L _|_ L1 & L _|_ L2 implies L1 // L2

    proof

      assume that

       A1: L c= P and

       A2: L1 c= P and

       A3: L2 c= P;

      assume that

       A4: L _|_ L1 and

       A5: L _|_ L2;

      (L,L2) are_coplane by A1, A3, Th96;

      then L meets L2 by A5, Th109;

      then

      consider x2 such that

       A6: x2 in L and

       A7: x2 in L2 by Th49;

      

       A8: L1 is being_line by A4, Th67;

      (L,L1) are_coplane by A1, A2, Th96;

      then L meets L1 by A4, Th109;

      then

      consider x1 such that

       A9: x1 in L and

       A10: x1 in L1 by Th49;

      

       A11: L2 is being_line by A5, Th67;

      now

        per cases ;

          case x1 = x2;

          hence thesis by A1, A2, A3, A4, A5, A9, A10, A7, A8, Th65, Th108;

        end;

          case

           A12: x1 <> x2;

          then (x1 - x2) <> ( 0* n) by Th9;

          then

           A13: |((x1 - x2), (x1 - x2))| <> 0 by EUCLID_4: 17;

          consider x such that

           A14: x <> x2 and

           A15: x in L2 by A11, Th53;

          

           A16: L2 = ( Line (x2,x)) by A7, A14, A15, Th64;

          consider x0 such that

           A17: x0 <> x1 and

           A18: x0 in L1 by A8, Th53;

          

           A19: L1 = ( Line (x0,x1)) by A10, A17, A18, Th64;

          

           A20: (x0 - x1) _|_ (x2 - x1) by A4, A9, A10, A6, A12, A17, A18, Th74;

          then ((x0 - x1),(x2 - x1)) are_orthogonal ;

          then

           A21: |((x0 - x1), (x2 - x1))| = 0 by RVSUM_1:def 17;

          P = ( plane (x1,x0,x2)) by A1, A2, A9, A6, A18, A20, Th45, Th92;

          then

          consider a1, a3, a2 such that

           A22: ((a1 + a3) + a2) = 1 and

           A23: x = (((a1 * x1) + (a3 * x0)) + (a2 * x2)) by A3, A15, Th88;

          

           A24: ((a2 + a1) + a3) = 1 by A22;

          

           A25: (x - x2) = (( - x2) + (((a2 * x2) + (a1 * x1)) + (a3 * x0))) by A23, RVSUM_1: 15

          .= (( - x2) + ((x2 + (a1 * (x1 - x2))) + (a3 * (x0 - x2)))) by A24, Th27

          .= (( - x2) + (x2 + ((a1 * (x1 - x2)) + (a3 * (x0 - x2))))) by RVSUM_1: 15

          .= ((( - x2) + x2) + ((a1 * (x1 - x2)) + (a3 * (x0 - x2)))) by RVSUM_1: 15

          .= (( 0* n) + ((a1 * (x1 - x2)) + (a3 * (x0 - x2)))) by Th2

          .= ((a1 * (x1 - x2)) + (a3 * (x0 - x2))) by EUCLID_4: 1;

          

           A26: |((x0 - x1), (x1 - x2))| = |((x0 - x1), ((( - 1) * x2) + ( - ( - x1))))|

          .= |((x0 - x1), (( - 1) * (x2 + ( - x1))))| by EUCLID_4: 6

          .= (( - 1) * |((x0 - x1), (x2 - x1))|) by EUCLID_4: 22

          .= 0 by A21;

          

           A27: (x0 - x2) = (x0 - (( 0* n) + x2)) by EUCLID_4: 1

          .= (x0 - ((x1 - x1) + x2)) by Th2

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

          .= (((x0 - x1) + x1) - x2) by Th4

          .= ((x0 - x1) + (x1 - x2)) by Th5;

          (x - x2) _|_ (x1 - x2) by A5, A9, A6, A7, A12, A14, A15, Th74;

          then ((x - x2),(x1 - x2)) are_orthogonal ;

          

          then 0 = |(((a1 * (x1 - x2)) + (a3 * (x0 - x2))), (x1 - x2))| by A25, RVSUM_1:def 17

          .= ( |((a1 * (x1 - x2)), (x1 - x2))| + |((a3 * (x0 - x2)), (x1 - x2))|) by EUCLID_4: 20

          .= ((a1 * |((x1 - x2), (x1 - x2))|) + |((a3 * (x0 - x2)), (x1 - x2))|) by EUCLID_4: 21

          .= ((a1 * |((x1 - x2), (x1 - x2))|) + (a3 * |((x0 - x2), (x1 - x2))|)) by EUCLID_4: 21

          .= ((a1 * |((x1 - x2), (x1 - x2))|) + (a3 * ( |((x0 - x1), (x1 - x2))| + |((x1 - x2), (x1 - x2))|))) by A27, EUCLID_4: 20

          .= ((a1 + a3) * |((x1 - x2), (x1 - x2))|) by A26;

          then (a1 + a3) = 0 by A13, XCMPLX_1: 6;

          then a3 = ( - a1);

          

          then

           A28: (x - x2) = (a1 * ((x1 + ( - x2)) - (x0 - x2))) by A25, Th12

          .= (a1 * ((x1 - x0) + (( - x2) - ( - x2)))) by Th18

          .= (a1 * ((x1 - x0) + ( 0* n))) by Th2

          .= (a1 * (x1 - x0)) by EUCLID_4: 1;

          

           A29: (x1 - x0) <> ( 0* n) by A17, Th9;

          (x - x2) <> ( 0* n) by A14, Th9;

          then (x - x2) // (x1 - x0) by A28, A29;

          hence thesis by A19, A16;

        end;

      end;

      hence thesis;

    end;

    theorem :: EUCLIDLP:112

    

     Th112: L0 c= P & L1 c= P & L2 c= P & L0 // L1 & L1 // L2 & L0 <> L1 & L meets L0 & L meets L1 implies L meets L2

    proof

      assume that

       A1: L0 c= P & L1 c= P and

       A2: L2 c= P and

       A3: L0 // L1 and

       A4: L1 // L2 and

       A5: L0 <> L1;

      

       A6: L1 is being_line by A3, Th66;

      assume that

       A7: L meets L0 and

       A8: L meets L1;

      consider x0 such that

       A9: x0 in L and

       A10: x0 in L0 by A7, Th49;

      

       A11: L0 misses L1 by A3, A5, Th71;

      then not x0 in L1 by A10, Th49;

      then

      consider L9 be Element of ( line_of_REAL n) such that

       A12: x0 in L9 and

       A13: L9 _|_ L1 and

       A14: L9 meets L1 by A6, Th62;

      consider y1 such that

       A15: y1 in L9 and

       A16: y1 in L1 by A14, Th49;

      

       A17: x0 <> y1 by A10, A11, A16, Th49;

      then

       A18: L9 = ( Line (x0,y1)) by A12, A15, Th64;

      then L9 c= P by A1, A10, A16, Th95;

      then (L9,L2) are_coplane by A2, Th96;

      then

       A19: L9 meets L2 by A4, A13, Th61, Th109;

      then

      consider y2 such that

       A20: y2 in L9 and

       A21: y2 in L2 by Th49;

      consider a such that

       A22: (y2 - x0) = (a * (y1 - x0)) by A12, A15, A17, A20, Th70;

      L2 is being_line by A4, Th66;

      then

      consider x2 such that

       A23: x2 <> y2 & x2 in L2 by Th53;

      consider x1 such that

       A24: x1 in L and

       A25: x1 in L1 by A8, Th49;

      x0 <> x1 by A10, A25, A11, Th49;

      then

       A26: L = ( Line (x0,x1)) by A9, A24, Th64;

      

       A27: L2 = ( Line (y2,x2)) by A21, A23, Th64;

      now

        per cases ;

          case x1 = y1;

          hence thesis by A9, A24, A17, A18, A19, Th64;

        end;

          case

           A28: x1 <> y1;

          set x = (((1 - a) * x0) + (a * x1));

          consider b such that

           A29: b <> 0 and

           A30: (x2 - y2) = (b * (x1 - y1)) by A4, A25, A16, A21, A23, A28, Th32, Th77;

          

           A31: (x1 - y1) = (1 * (x1 - y1)) by EUCLID_4: 3

          .= (((1 / b) * b) * (x1 - y1)) by A29, XCMPLX_1: 87

          .= ((1 / b) * (x2 - y2)) by A30, EUCLID_4: 4;

          x = (((1 * x0) + ( - (a * x0))) + (a * x1)) by Th11

          .= ((x0 + ( - (a * x0))) + (a * x1)) by EUCLID_4: 3

          .= (((a * x1) + ( - (a * x0))) + x0) by RVSUM_1: 15

          .= ((a * (x1 - x0)) + x0) by Th12

          .= ((a * ((x1 + ( 0* n)) + ( - x0))) + x0) by EUCLID_4: 1

          .= ((a * ((x1 + (( - y1) + y1)) + ( - x0))) + x0) by Th2

          .= ((a * (((x1 + ( - y1)) + y1) + ( - x0))) + x0) by RVSUM_1: 15

          .= ((a * ((x1 - y1) + (y1 + ( - x0)))) + x0) by RVSUM_1: 15

          .= (((a * ((1 / b) * (x2 - y2))) + (a * (y1 - x0))) + x0) by A31, EUCLID_4: 6

          .= ((((a * (1 / b)) * (x2 - y2)) + (a * (y1 - x0))) + x0) by EUCLID_4: 4

          .= ((((a / b) * (x2 - y2)) + (a * (y1 - x0))) + x0) by XCMPLX_1: 99

          .= (((a / b) * (x2 - y2)) + ((y2 + ( - x0)) + x0)) by A22, RVSUM_1: 15

          .= (((a / b) * (x2 - y2)) + (y2 + (( - x0) + x0))) by RVSUM_1: 15

          .= (((a / b) * (x2 - y2)) + (y2 + ( 0* n))) by Th2

          .= (((a / b) * (x2 - y2)) + y2) by EUCLID_4: 1

          .= ((((a / b) * x2) + ( - ((a / b) * y2))) + y2) by Th12

          .= ((y2 + ( - ((a / b) * y2))) + ((a / b) * x2)) by RVSUM_1: 15

          .= (((1 * y2) + ( - ((a / b) * y2))) + ((a / b) * x2)) by EUCLID_4: 3

          .= (((1 - (a / b)) * y2) + ((a / b) * x2)) by Th11;

          then

           A32: x in L2 by A27;

          x in L by A26;

          hence thesis by A32, Th49;

        end;

      end;

      hence thesis;

    end;

    theorem :: EUCLIDLP:113

    

     Th113: (L1,L2) are_coplane & L1 is being_line & L2 is being_line & L1 misses L2 implies L1 // L2

    proof

      assume that

       A1: (L1,L2) are_coplane and

       A2: L1 is being_line and

       A3: L2 is being_line;

      assume

       A4: L1 misses L2;

      then

      consider x such that

       A5: x in L1 and

       A6: not x in L2 by Th63;

      consider P such that

       A7: L1 c= P and

       A8: L2 c= P by A1, Th96;

      consider L9 be Element of ( line_of_REAL n) such that

       A9: x in L9 and

       A10: L9 _|_ L2 and

       A11: L9 meets L2 by A3, A6, Th62;

      consider x2 such that

       A12: x2 in L9 and

       A13: x2 in L2 by A11, Th49;

      consider L0 such that

       A14: x in L0 and

       A15: L0 _|_ L9 and

       A16: L0 // L2 by A10, Th80;

      L9 = ( Line (x2,x)) by A6, A9, A12, A13, Th64;

      then

       A17: L9 c= P by A5, A7, A8, A13, Th95;

      then

       A18: L0 c= P by A8, A9, A10, A14, A16, Th110;

      

       A19: L9 is being_line by A15, Th67;

      consider x1 such that

       A20: x1 <> x and

       A21: x1 in L1 by A2, Th53;

      

       A22: L1 = ( Line (x,x1)) by A5, A20, A21, Th64;

      

       A23: L0 meets L1 by A5, A14, Th49;

      L1 = L0

      proof

        

         A24: not x1 in L9 by A4, A9, A11, A20, A22, Th64;

        then

        consider L such that

         A25: x1 in L and

         A26: L9 _|_ L and

         A27: L9 meets L by A19, Th62;

        

         A28: L meets L1 by A21, A25, Th49;

        assume L1 <> L0;

        then

         A29: L <> L0 by A14, A20, A22, A25, Th64;

        consider x9 be Element of ( REAL n) such that

         A30: x9 in L9 and

         A31: x9 in L by A27, Th49;

        L = ( Line (x9,x1)) by A24, A25, A30, A31, Th64;

        then

         A32: L c= P by A7, A17, A21, A30, Th95;

        then L // L0 by A17, A15, A18, A26, Th111;

        hence contradiction by A4, A8, A16, A18, A23, A32, A29, A28, Th112;

      end;

      hence thesis by A16;

    end;

    theorem :: EUCLIDLP:114

    x1 in P & x2 in P & y1 in P & y2 in P & ((x2 - x1),(y2 - y1)) are_lindependent2 implies ( Line (x1,x2)) meets ( Line (y1,y2))

    proof

      reconsider L1 = ( Line (x1,x2)), L2 = ( Line (y1,y2)) as Element of ( line_of_REAL n) by Th47;

      assume that

       A1: x1 in P & x2 in P & y1 in P & y2 in P and

       A2: ((x2 - x1),(y2 - y1)) are_lindependent2 ;

      

       A3: x1 in L1 & x2 in L1 by EUCLID_4: 9;

      L1 c= P & L2 c= P by A1, Th95;

      then

       A4: (L1,L2) are_coplane by Th96;

      

       A5: y1 in L2 & y2 in L2 by EUCLID_4: 9;

      (y2 - y1) <> ( 0* n) by A2, Lm2;

      then

       A6: y2 <> y1 by Th9;

      then

       A7: L2 is being_line;

      (x2 - x1) <> ( 0* n) by A2, Lm2;

      then

       A8: x2 <> x1 by Th9;

      then

       A9: L1 is being_line;

      L1 meets L2

      proof

        assume L1 misses L2;

        then L1 // L2 by A4, A9, A7, Th113;

        hence contradiction by A2, A8, A6, A3, A5, Lm3, Th77;

      end;

      hence thesis;

    end;