analmetr.miz



    begin

    reserve V for RealLinearSpace;

    reserve u,u1,u2,v,v1,v2,w,w1,y for VECTOR of V;

    reserve a,a1,a2,b,b1,b2,c1,c2 for Real;

    reserve x,z for set;

    

     Lm1: v1 = ((b1 * w) + (b2 * y)) & v2 = ((c1 * w) + (c2 * y)) implies (v1 + v2) = (((b1 + c1) * w) + ((b2 + c2) * y)) & (v1 - v2) = (((b1 - c1) * w) + ((b2 - c2) * y))

    proof

      assume

       A1: v1 = ((b1 * w) + (b2 * y)) & v2 = ((c1 * w) + (c2 * y));

      

      hence (v1 + v2) = ((((b1 * w) + (b2 * y)) + (c1 * w)) + (c2 * y)) by RLVECT_1:def 3

      .= ((((b1 * w) + (c1 * w)) + (b2 * y)) + (c2 * y)) by RLVECT_1:def 3

      .= ((((b1 + c1) * w) + (b2 * y)) + (c2 * y)) by RLVECT_1:def 6

      .= (((b1 + c1) * w) + ((b2 * y) + (c2 * y))) by RLVECT_1:def 3

      .= (((b1 + c1) * w) + ((b2 + c2) * y)) by RLVECT_1:def 6;

      

      thus (v1 - v2) = (((b1 * w) + (b2 * y)) + (( - (c1 * w)) + ( - (c2 * y)))) by A1, RLVECT_1: 31

      .= (((b1 * w) + (b2 * y)) + ((c1 * ( - w)) + ( - (c2 * y)))) by RLVECT_1: 25

      .= (((b1 * w) + (b2 * y)) + ((c1 * ( - w)) + (c2 * ( - y)))) by RLVECT_1: 25

      .= (((b1 * w) + (b2 * y)) + ((( - c1) * w) + (c2 * ( - y)))) by RLVECT_1: 24

      .= (((b1 * w) + (b2 * y)) + ((( - c1) * w) + (( - c2) * y))) by RLVECT_1: 24

      .= ((((b1 * w) + (b2 * y)) + (( - c1) * w)) + (( - c2) * y)) by RLVECT_1:def 3

      .= ((((b1 * w) + (( - c1) * w)) + (b2 * y)) + (( - c2) * y)) by RLVECT_1:def 3

      .= ((((b1 + ( - c1)) * w) + (b2 * y)) + (( - c2) * y)) by RLVECT_1:def 6

      .= (((b1 + ( - c1)) * w) + ((b2 * y) + (( - c2) * y))) by RLVECT_1:def 3

      .= (((b1 - c1) * w) + ((b2 + ( - c2)) * y)) by RLVECT_1:def 6

      .= (((b1 - c1) * w) + ((b2 - c2) * y));

    end;

    

     Lm2: for w, y holds (( 0 * w) + ( 0 * y)) = ( 0. V)

    proof

      let w, y;

      

      thus (( 0 * w) + ( 0 * y)) = (( 0. V) + ( 0 * y)) by RLVECT_1: 10

      .= (( 0. V) + ( 0. V)) by RLVECT_1: 10

      .= ( 0. V) by RLVECT_1: 4;

    end;

    

     Lm3: v = ((b1 * w) + (b2 * y)) implies (a * v) = (((a * b1) * w) + ((a * b2) * y))

    proof

      assume v = ((b1 * w) + (b2 * y));

      

      hence (a * v) = ((a * (b1 * w)) + (a * (b2 * y))) by RLVECT_1:def 5

      .= (((a * b1) * w) + (a * (b2 * y))) by RLVECT_1:def 7

      .= (((a * b1) * w) + ((a * b2) * y)) by RLVECT_1:def 7;

    end;

    definition

      let V;

      let w, y;

      :: ANALMETR:def1

      pred Gen w,y means

      : Def1: (for u holds ex a1, a2 st u = ((a1 * w) + (a2 * y))) & for a1, a2 st ((a1 * w) + (a2 * y)) = ( 0. V) holds a1 = 0 & a2 = 0 ;

    end

    definition

      let V;

      let u, v, w, y;

      :: ANALMETR:def2

      pred u,v are_Ort_wrt w,y means

      : Def2: ex a1, a2, b1, b2 st u = ((a1 * w) + (a2 * y)) & v = ((b1 * w) + (b2 * y)) & ((a1 * b1) + (a2 * b2)) = 0 ;

    end

    

     Lm4: Gen (w,y) & ((a1 * w) + (a2 * y)) = ((b1 * w) + (b2 * y)) implies a1 = b1 & a2 = b2

    proof

      assume that

       A1: Gen (w,y) and

       A2: ((a1 * w) + (a2 * y)) = ((b1 * w) + (b2 * y));

      ( 0. V) = (((a1 * w) + (a2 * y)) - ((b1 * w) + (b2 * y))) by A2, RLVECT_1: 15

      .= (((a1 - b1) * w) + ((a2 - b2) * y)) by Lm1;

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

      hence thesis;

    end;

    theorem :: ANALMETR:1

    

     Th1: for w, y st Gen (w,y) holds ((u,v) are_Ort_wrt (w,y) iff for a1, a2, b1, b2 st u = ((a1 * w) + (a2 * y)) & v = ((b1 * w) + (b2 * y)) holds ((a1 * b1) + (a2 * b2)) = 0 )

    proof

      let w, y such that

       A1: Gen (w,y);

      hereby

        assume (u,v) are_Ort_wrt (w,y);

        then

        consider a1, a2, b1, b2 such that

         A2: u = ((a1 * w) + (a2 * y)) and

         A3: v = ((b1 * w) + (b2 * y)) and

         A4: ((a1 * b1) + (a2 * b2)) = 0 ;

        let a19,a29,b19,b29 be Real;

        assume that

         A5: u = ((a19 * w) + (a29 * y)) and

         A6: v = ((b19 * w) + (b29 * y));

        

         A7: b1 = b19 by A1, A3, A6, Lm4;

        a1 = a19 & a2 = a29 by A1, A2, A5, Lm4;

        hence 0 = ((a19 * b19) + (a29 * b29)) by A1, A3, A4, A6, A7, Lm4;

      end;

      consider a1, a2 such that

       A8: u = ((a1 * w) + (a2 * y)) by A1;

      consider b1, b2 such that

       A9: v = ((b1 * w) + (b2 * y)) by A1;

      assume for a1, a2, b1, b2 st u = ((a1 * w) + (a2 * y)) & v = ((b1 * w) + (b2 * y)) holds ((a1 * b1) + (a2 * b2)) = 0 ;

      then ((a1 * b1) + (a2 * b2)) = 0 by A8, A9;

      hence thesis by A8, A9;

    end;

    

     Lm5: Gen (w,y) implies w <> ( 0. V) & y <> ( 0. V)

    proof

      assume

       A1: Gen (w,y);

      thus w <> ( 0. V)

      proof

        assume w = ( 0. V);

        

        then ( 0. V) = (1 * w) by RLVECT_1:def 8

        .= ((1 * w) + ( 0. V)) by RLVECT_1: 4

        .= ((1 * w) + ( 0 * y)) by RLVECT_1: 10;

        hence contradiction by A1;

      end;

      thus y <> ( 0. V)

      proof

        assume y = ( 0. V);

        

        then ( 0. V) = (1 * y) by RLVECT_1:def 8

        .= (( 0. V) + (1 * y)) by RLVECT_1: 4

        .= (( 0 * w) + (1 * y)) by RLVECT_1: 10;

        hence contradiction by A1;

      end;

    end;

    theorem :: ANALMETR:2

    (w,y) are_Ort_wrt (w,y)

    proof

      

       A1: y = (( 0. V) + y) by RLVECT_1: 4

      .= (( 0. V) + (1 * y)) by RLVECT_1:def 8

      .= (( 0 * w) + (1 * y)) by RLVECT_1: 10;

      

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

      w = (w + ( 0. V)) by RLVECT_1: 4

      .= ((1 * w) + ( 0. V)) by RLVECT_1:def 8

      .= ((1 * w) + ( 0 * y)) by RLVECT_1: 10;

      hence thesis by A1, A2;

    end;

    theorem :: ANALMETR:3

    

     Th3: ex V st ex w, y st Gen (w,y) by Def1, FUNCSDOM: 23;

    theorem :: ANALMETR:4

    (u,v) are_Ort_wrt (w,y) implies (v,u) are_Ort_wrt (w,y);

    theorem :: ANALMETR:5

    

     Th5: Gen (w,y) implies for u, v holds (u,( 0. V)) are_Ort_wrt (w,y) & (( 0. V),v) are_Ort_wrt (w,y)

    proof

      assume

       A1: Gen (w,y);

      let u, v;

      consider a1, a2 such that

       A2: u = ((a1 * w) + (a2 * y)) by A1;

      consider b1, b2 such that

       A3: v = ((b1 * w) + (b2 * y)) by A1;

      

       A4: ( 0. V) = (( 0. V) + ( 0. V)) by RLVECT_1: 4

      .= (( 0 * w) + ( 0. V)) by RLVECT_1: 10

      .= (( 0 * w) + ( 0 * y)) by RLVECT_1: 10;

      ((a1 * 0 ) + (a2 * 0 )) = 0 ;

      hence (u,( 0. V)) are_Ort_wrt (w,y) by A2, A4;

      (( 0 * b1) + ( 0 * b2)) = 0 ;

      hence thesis by A3, A4;

    end;

    theorem :: ANALMETR:6

    

     Th6: (u,v) are_Ort_wrt (w,y) implies ((a * u),(b * v)) are_Ort_wrt (w,y)

    proof

      assume (u,v) are_Ort_wrt (w,y);

      then

      consider a1, a2, b1, b2 such that

       A1: u = ((a1 * w) + (a2 * y)) and

       A2: v = ((b1 * w) + (b2 * y)) and

       A3: ((a1 * b1) + (a2 * b2)) = 0 ;

      

       A4: (b * v) = ((b * (b1 * w)) + (b * (b2 * y))) by A2, RLVECT_1:def 5

      .= (((b * b1) * w) + (b * (b2 * y))) by RLVECT_1:def 7

      .= (((b * b1) * w) + ((b * b2) * y)) by RLVECT_1:def 7;

      

       A5: (((a * a1) * (b * b1)) + ((a * a2) * (b * b2))) = ((b * a) * ((a1 * b1) + (a2 * b2)))

      .= 0 by A3;

      (a * u) = ((a * (a1 * w)) + (a * (a2 * y))) by A1, RLVECT_1:def 5

      .= (((a * a1) * w) + (a * (a2 * y))) by RLVECT_1:def 7

      .= (((a * a1) * w) + ((a * a2) * y)) by RLVECT_1:def 7;

      hence thesis by A4, A5;

    end;

    theorem :: ANALMETR:7

    

     Th7: (u,v) are_Ort_wrt (w,y) implies ((a * u),v) are_Ort_wrt (w,y) & (u,(b * v)) are_Ort_wrt (w,y)

    proof

      

       A1: v = (1 * v) & u = (1 * u) by RLVECT_1:def 8;

      assume (u,v) are_Ort_wrt (w,y);

      hence thesis by A1, Th6;

    end;

    theorem :: ANALMETR:8

    

     Th8: Gen (w,y) implies for u holds ex v st (u,v) are_Ort_wrt (w,y) & v <> ( 0. V)

    proof

      assume

       A1: Gen (w,y);

      let u;

      consider a1, a2 such that

       A2: u = ((a1 * w) + (a2 * y)) by A1;

       A3:

      now

        set v = ((a2 * w) + (( - a1) * y));

        assume

         A4: u <> ( 0. V);

        take v;

        ((a1 * a2) + (a2 * ( - a1))) = 0 ;

        hence (u,v) are_Ort_wrt (w,y) by A2;

        v <> ( 0. V)

        proof

          assume v = ( 0. V);

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

          

          then u = (( 0 * w) + ( 0. V)) by A2, RLVECT_1: 10

          .= ( 0 * w) by RLVECT_1: 4

          .= ( 0. V) by RLVECT_1: 10;

          hence contradiction by A4;

        end;

        hence v <> ( 0. V);

      end;

      now

        assume

         A5: u = ( 0. V);

        take v = w;

        thus (u,v) are_Ort_wrt (w,y) by A1, A5, Th5;

        thus v <> ( 0. V) by A1, Lm5;

      end;

      hence thesis by A3;

    end;

    theorem :: ANALMETR:9

    

     Th9: Gen (w,y) & (v,u1) are_Ort_wrt (w,y) & (v,u2) are_Ort_wrt (w,y) & v <> ( 0. V) implies ex a, b st (a * u1) = (b * u2) & (a <> 0 or b <> 0 )

    proof

      assume that

       A1: Gen (w,y) and

       A2: (v,u1) are_Ort_wrt (w,y) and

       A3: (v,u2) are_Ort_wrt (w,y) and

       A4: v <> ( 0. V);

      consider a1, a2, b1, b2 such that

       A5: v = ((a1 * w) + (a2 * y)) and

       A6: u1 = ((b1 * w) + (b2 * y)) and

       A7: ((a1 * b1) + (a2 * b2)) = 0 by A2;

      consider a19,a29,c1,c2 be Real such that

       A8: v = ((a19 * w) + (a29 * y)) and

       A9: u2 = ((c1 * w) + (c2 * y)) and

       A10: ((a19 * c1) + (a29 * c2)) = 0 by A3;

      

       A11: a2 = a29 by A1, A5, A8, Lm4;

      

       A12: a1 = a19 by A1, A5, A8, Lm4;

       A13:

      now

        assume

         A14: a1 = 0 ;

        then

         A15: a2 <> 0 by A4, A5, Lm2;

        then c2 = 0 by A10, A12, A11, A14, XCMPLX_1: 6;

        then u2 = ((c1 * w) + ( 0. V)) by A9, RLVECT_1: 10;

        then

         A16: u2 = (c1 * w) by RLVECT_1: 4;

        b2 = 0 by A7, A14, A15, XCMPLX_1: 6;

        then

         A17: u1 = ((b1 * w) + ( 0. V)) by A6, RLVECT_1: 10;

        then

         A18: u1 = (b1 * w) by RLVECT_1: 4;

         A19:

        now

          assume b1 = 0 ;

          

          then (1 * u1) = ( 0 * w) by A18, RLVECT_1:def 8

          .= ( 0. V) by RLVECT_1: 10

          .= ( 0 * u2) by RLVECT_1: 10;

          hence thesis;

        end;

        (c1 * u1) = (c1 * (b1 * w)) by A17, RLVECT_1: 4

        .= ((b1 * c1) * w) by RLVECT_1:def 7

        .= (b1 * u2) by A16, RLVECT_1:def 7;

        hence thesis by A19;

      end;

      now

        

         A20: (c2 * ((( - a2) * b2) * (a1 " ))) = (b2 * ((( - a2) * c2) * (a1 " )));

        assume

         A21: a1 <> 0 ;

        

         A22: b1 = (1 * b1)

        .= ((a1 * (a1 " )) * b1) by A21, XCMPLX_0:def 7

        .= ((a1 * b1) * (a1 " ))

        .= ((( - a2) * b2) * (a1 " )) by A7;

        

         A23: c1 = (1 * c1)

        .= ((a1 * (a1 " )) * c1) by A21, XCMPLX_0:def 7

        .= ((a1 * c1) * (a1 " ))

        .= ((( - a2) * c2) * (a1 " )) by A1, A5, A8, A10, A11, Lm4;

        then

         A24: (b2 * u2) = (((b2 * ((( - a2) * c2) * (a1 " ))) * w) + ((b2 * c2) * y)) by A9, Lm3;

         A25:

        now

          assume

           A26: c2 <> 0 or b2 <> 0 ;

          take a = c2, b = b2;

          thus (a * u1) = (b * u2) & (a <> 0 or b <> 0 ) by A6, A22, A24, A20, A26, Lm3;

        end;

        now

          assume b2 = 0 & c2 = 0 ;

          then (1 * u1) = (1 * u2) by A6, A9, A22, A23;

          hence thesis;

        end;

        hence thesis by A25;

      end;

      hence thesis by A13;

    end;

    theorem :: ANALMETR:10

    

     Th10: Gen (w,y) & (u,v1) are_Ort_wrt (w,y) & (u,v2) are_Ort_wrt (w,y) implies (u,(v1 + v2)) are_Ort_wrt (w,y) & (u,(v1 - v2)) are_Ort_wrt (w,y)

    proof

      assume that

       A1: Gen (w,y) and

       A2: (u,v1) are_Ort_wrt (w,y) and

       A3: (u,v2) are_Ort_wrt (w,y);

      consider a1, a2, b1, b2 such that

       A4: u = ((a1 * w) + (a2 * y)) and

       A5: v1 = ((b1 * w) + (b2 * y)) and

       A6: ((a1 * b1) + (a2 * b2)) = 0 by A2;

      consider a19,a29,c1,c2 be Real such that

       A7: u = ((a19 * w) + (a29 * y)) and

       A8: v2 = ((c1 * w) + (c2 * y)) and

       A9: ((a19 * c1) + (a29 * c2)) = 0 by A3;

      

       A10: a1 = a19 & a2 = a29 by A1, A4, A7, Lm4;

      then

       A11: ((a1 * (b1 + c1)) + (a2 * (b2 + c2))) = 0 by A6, A9;

      

       A12: ((a1 * (b1 - c1)) + (a2 * (b2 - c2))) = 0 by A6, A9, A10;

      (v1 + v2) = (((b1 + c1) * w) + ((b2 + c2) * y)) by A5, A8, Lm1;

      hence (u,(v1 + v2)) are_Ort_wrt (w,y) by A4, A11;

      (v1 - v2) = (((b1 - c1) * w) + ((b2 - c2) * y)) by A5, A8, Lm1;

      hence thesis by A4, A12;

    end;

    theorem :: ANALMETR:11

    

     Th11: Gen (w,y) & (u,u) are_Ort_wrt (w,y) implies u = ( 0. V)

    proof

       A1:

      now

        let a such that

         A2: a <> 0 ;

         0 < a implies 0 < (a * a) by XREAL_1: 129;

        hence 0 < (a * a) by A2, XREAL_1: 130;

      end;

      assume that

       A3: Gen (w,y) and

       A4: (u,u) are_Ort_wrt (w,y);

      consider a1, a2, b1, b2 such that

       A5: u = ((a1 * w) + (a2 * y)) and

       A6: u = ((b1 * w) + (b2 * y)) and

       A7: ((a1 * b1) + (a2 * b2)) = 0 by A4;

      

       A8: a1 = b1 & a2 = b2 by A3, A5, A6, Lm4;

      

       A9: a2 = 0

      proof

        assume a2 <> 0 ;

        then 0 < (a2 * a2) by A1;

        hence contradiction by A7, A8, XREAL_1: 29, XREAL_1: 63;

      end;

      a1 = 0

      proof

        assume a1 <> 0 ;

        then 0 < (a1 * a1) by A1;

        hence contradiction by A7, A8, XREAL_1: 29, XREAL_1: 63;

      end;

      

      hence u = (( 0 * w) + ( 0. V)) by A5, A9, RLVECT_1: 10

      .= ( 0 * w) by RLVECT_1: 4

      .= ( 0. V) by RLVECT_1: 10;

    end;

    theorem :: ANALMETR:12

    

     Th12: Gen (w,y) & (u,(u1 - u2)) are_Ort_wrt (w,y) & (u1,(u2 - u)) are_Ort_wrt (w,y) implies (u2,(u - u1)) are_Ort_wrt (w,y)

    proof

      assume that

       A1: Gen (w,y) and

       A2: (u,(u1 - u2)) are_Ort_wrt (w,y) and

       A3: (u1,(u2 - u)) are_Ort_wrt (w,y);

      consider a1, a2 such that

       A4: u = ((a1 * w) + (a2 * y)) by A1;

      consider c1, c2 such that

       A5: u2 = ((c1 * w) + (c2 * y)) by A1;

      consider b1, b2 such that

       A6: u1 = ((b1 * w) + (b2 * y)) by A1;

      

       A7: (u - u1) = (((a1 - b1) * w) + ((a2 - b2) * y)) by A4, A6, Lm1;

      (u2 - u) = (((c1 - a1) * w) + ((c2 - a2) * y)) by A4, A5, Lm1;

      then

       A8: ((b1 * (c1 - a1)) + (b2 * (c2 - a2))) = 0 by A1, A3, A6, Th1;

      (u1 - u2) = (((b1 - c1) * w) + ((b2 - c2) * y)) by A6, A5, Lm1;

      then ((a1 * (b1 - c1)) + (a2 * (b2 - c2))) = 0 by A1, A2, A4, Th1;

      then 0 = ((c1 * (a1 - b1)) + (c2 * (a2 - b2))) by A8;

      hence thesis by A5, A7;

    end;

    theorem :: ANALMETR:13

    

     Th13: Gen (w,y) & u <> ( 0. V) implies ex a st ((v - (a * u)),u) are_Ort_wrt (w,y)

    proof

      assume that

       A1: Gen (w,y) and

       A2: u <> ( 0. V);

      consider a1, a2 such that

       A3: u = ((a1 * w) + (a2 * y)) by A1;

      consider b1, b2 such that

       A4: v = ((b1 * w) + (b2 * y)) by A1;

      set a = (((b1 * a1) + (b2 * a2)) * (((a1 * a1) + (a2 * a2)) " ));

      (a * u) = (((a * a1) * w) + ((a * a2) * y)) by A3, Lm3;

      then

       A5: (v - (a * u)) = (((b1 - (a * a1)) * w) + ((b2 - (a * a2)) * y)) by A4, Lm1;

      

       A6: (((b1 - (a * a1)) * a1) + ((b2 - (a * a2)) * a2)) = (((a1 * b1) + (a2 * b2)) + (( - 1) * ((a1 * (a * a1)) + (a2 * (a * a2)))));

      

       A7: ((a1 * a1) + (a2 * a2)) <> 0 by A1, A2, Th11, A3, Def2;

      (( - 1) * ((a1 * (a * a1)) + (a2 * (a * a2)))) = (( - 1) * (((b1 * a1) + (b2 * a2)) * ((((a1 * a1) + (a2 * a2)) " ) * ((a1 * a1) + (a2 * a2)))))

      .= (( - 1) * (((b1 * a1) + (b2 * a2)) * 1)) by A7, XCMPLX_0:def 7

      .= ( - ((a1 * b1) + (a2 * b2)));

      then ((v - (a * u)),u) are_Ort_wrt (w,y) by A3, A5, A6;

      hence thesis;

    end;

    theorem :: ANALMETR:14

    

     Th14: ((u,v) // (u1,v1) or (u,v) // (v1,u1)) iff ex a, b st (a * (v - u)) = (b * (v1 - u1)) & (a <> 0 or b <> 0 )

    proof

       A1:

      now

        let w,y,w1,y1 be VECTOR of V;

        given a, b such that

         A2: (a * (y - w)) = (b * (y1 - w1)) & a = 0 and

         A3: b <> 0 ;

        ( 0. V) = (b * (y1 - w1)) by A2, RLVECT_1: 10;

        then (y1 - w1) = ( 0. V) by A3, RLVECT_1: 11;

        then y1 = w1 by RLVECT_1: 21;

        hence (w,y) // (w1,y1) by ANALOAF: 9;

      end;

       A4:

      now

        let w,y,w1,y1 be VECTOR of V;

        given a, b such that

         A5: (a * (y - w)) = (b * (y1 - w1)) and

         A6: 0 < a and

         A7: b < 0 ;

        

         A8: (a * (y - w)) = (b * ( - (w1 - y1))) by A5, RLVECT_1: 33

        .= (( - b) * (w1 - y1)) by RLVECT_1: 24;

         0 < ( - b) by A7, XREAL_1: 58;

        hence (w,y) // (y1,w1) by A6, A8, ANALOAF:def 1;

      end;

       A9:

      now

        given a, b such that

         A10: (a * (v - u)) = (b * (v1 - u1)) and

         A11: a <> 0 or b <> 0 ;

         A12:

        now

           A13:

          now

            assume a < 0 & b < 0 ;

            then

             A14: 0 < ( - a) & 0 < ( - b) by XREAL_1: 58;

            (( - a) * (u - v)) = (a * ( - (u - v))) by RLVECT_1: 24

            .= (b * (v1 - u1)) by A10, RLVECT_1: 33

            .= (b * ( - (u1 - v1))) by RLVECT_1: 33

            .= (( - b) * (u1 - v1)) by RLVECT_1: 24;

            then (v,u) // (v1,u1) by A14, ANALOAF:def 1;

            hence (u,v) // (u1,v1) or (u,v) // (v1,u1) by ANALOAF: 12;

          end;

           A15:

          now

            assume a < 0 & 0 < b;

            then (u1,v1) // (v,u) by A4, A10;

            then (v,u) // (u1,v1) by ANALOAF: 12;

            hence (u,v) // (u1,v1) or (u,v) // (v1,u1) by ANALOAF: 12;

          end;

          assume

           A16: a <> 0 & b <> 0 ;

           0 < a & b < 0 implies ((u,v) // (u1,v1) or (u,v) // (v1,u1)) by A4, A10;

          hence (u,v) // (u1,v1) or (u,v) // (v1,u1) by A10, A16, A15, A13, ANALOAF:def 1;

        end;

        now

          assume b = 0 ;

          then (u1,v1) // (u,v) by A1, A10, A11;

          hence (u,v) // (u1,v1) or (u,v) // (v1,u1) by ANALOAF: 12;

        end;

        hence (u,v) // (u1,v1) or (u,v) // (v1,u1) by A1, A10, A12;

      end;

       A17:

      now

        let w,y,w1,y1 be VECTOR of V such that

         A18: (w,y) // (w1,y1);

         A19:

        now

          assume w = y;

          

          then (1 * (y - w)) = ( 0. V) by RLVECT_1: 10, RLVECT_1: 15

          .= ( 0 * (y1 - w1)) by RLVECT_1: 10;

          hence ex a, b st (a * (y - w)) = (b * (y1 - w1)) & (a <> 0 or b <> 0 );

        end;

         A20:

        now

          assume w1 = y1;

          

          then (1 * (y1 - w1)) = ( 0. V) by RLVECT_1: 10, RLVECT_1: 15

          .= ( 0 * (y - w)) by RLVECT_1: 10;

          hence ex a, b st (a * (y - w)) = (b * (y1 - w1)) & (a <> 0 or b <> 0 );

        end;

        (ex a, b st 0 < a & 0 < b & (a * (y - w)) = (b * (y1 - w1))) implies ex a, b st (a * (y - w)) = (b * (y1 - w1)) & (a <> 0 or b <> 0 );

        hence ex a, b st (a * (y - w)) = (b * (y1 - w1)) & (a <> 0 or b <> 0 ) by A18, A19, A20, ANALOAF:def 1;

      end;

      now

        assume (u,v) // (v1,u1);

        then

        consider a, b such that

         A21: (a * (v - u)) = (b * (u1 - v1)) and

         A22: a <> 0 or b <> 0 by A17;

        

         A23: a <> 0 or ( - b) <> 0 by A22;

        (( - b) * (v1 - u1)) = (b * ( - (v1 - u1))) by RLVECT_1: 24

        .= (a * (v - u)) by A21, RLVECT_1: 33;

        hence ex a, b st (a * (v - u)) = (b * (v1 - u1)) & (a <> 0 or b <> 0 ) by A23;

      end;

      hence thesis by A17, A9;

    end;

    theorem :: ANALMETR:15

    

     Th15: [ [u, v], [u1, v1]] in ( lambda ( DirPar V)) iff ex a, b st (a * (v - u)) = (b * (v1 - u1)) & (a <> 0 or b <> 0 )

    proof

       [ [u, v], [u1, v1]] in ( lambda ( DirPar V)) iff [ [u, v], [u1, v1]] in ( DirPar V) or [ [u, v], [v1, u1]] in ( DirPar V) by DIRAF:def 1;

      then [ [u, v], [u1, v1]] in ( lambda ( DirPar V)) iff ((u,v) // (u1,v1) or (u,v) // (v1,u1)) by ANALOAF: 22;

      hence thesis by Th14;

    end;

    definition

      let V;

      let u, u1, v, v1, w, y;

      :: ANALMETR:def3

      pred u,u1,v,v1 are_Ort_wrt w,y means ((u1 - u),(v1 - v)) are_Ort_wrt (w,y);

    end

    definition

      let V;

      let w, y;

      :: ANALMETR:def4

      func Orthogonality (V,w,y) -> Relation of [:the carrier of V, the carrier of V:] means

      : Def4: for x,z be object holds [x, z] in it iff ex u, u1, v, v1 st x = [u, u1] & z = [v, v1] & (u,u1,v,v1) are_Ort_wrt (w,y);

      existence

      proof

        defpred P[ object, object] means ex u, u1, v, v1 st $1 = [u, u1] & $2 = [v, v1] & (u,u1,v,v1) are_Ort_wrt (w,y);

        set VV = [:the carrier of V, the carrier of V:];

        consider P be Relation of VV, VV such that

         A1: for x,z be object holds [x, z] in P iff x in VV & z in VV & P[x, z] from RELSET_1:sch 1;

        take P;

        let x,z be object;

        thus [x, z] in P implies ex u, u1, v, v1 st x = [u, u1] & z = [v, v1] & (u,u1,v,v1) are_Ort_wrt (w,y) by A1;

        assume ex u, u1, v, v1 st x = [u, u1] & z = [v, v1] & (u,u1,v,v1) are_Ort_wrt (w,y);

        hence thesis by A1;

      end;

      uniqueness

      proof

        let P,Q be Relation of [:the carrier of V, the carrier of V:] such that

         A2: for x,z be object holds [x, z] in P iff ex u, u1, v, v1 st x = [u, u1] & z = [v, v1] & (u,u1,v,v1) are_Ort_wrt (w,y) and

         A3: for x,z be object holds [x, z] in Q iff ex u, u1, v, v1 st x = [u, u1] & z = [v, v1] & (u,u1,v,v1) are_Ort_wrt (w,y);

        for x,z be object holds [x, z] in P iff [x, z] in Q

        proof

          let x,z be object;

           [x, z] in P iff ex u, u1, v, v1 st x = [u, u1] & z = [v, v1] & (u,u1,v,v1) are_Ort_wrt (w,y) by A2;

          hence thesis by A3;

        end;

        hence thesis by RELAT_1:def 2;

      end;

    end

    reserve p,p1,q,q1 for Element of ( Lambda ( OASpace V));

    theorem :: ANALMETR:16

    

     Th16: the carrier of ( Lambda ( OASpace V)) = the carrier of V

    proof

      ( Lambda ( OASpace V)) = AffinStruct (# the carrier of ( OASpace V), ( lambda the CONGR of ( OASpace V)) #) & ( OASpace V) = AffinStruct (# the carrier of V, ( DirPar V) #) by ANALOAF:def 4, DIRAF:def 2;

      hence thesis;

    end;

    theorem :: ANALMETR:17

    

     Th17: the CONGR of ( Lambda ( OASpace V)) = ( lambda ( DirPar V))

    proof

      ( Lambda ( OASpace V)) = AffinStruct (# the carrier of ( OASpace V), ( lambda the CONGR of ( OASpace V)) #) & ( OASpace V) = AffinStruct (# the carrier of V, ( DirPar V) #) by ANALOAF:def 4, DIRAF:def 2;

      hence thesis;

    end;

    theorem :: ANALMETR:18

    p = u & q = v & p1 = u1 & q1 = v1 implies ((p,q) // (p1,q1) iff ex a, b st (a * (v - u)) = (b * (v1 - u1)) & (a <> 0 or b <> 0 ))

    proof

      assume

       A1: p = u & q = v & p1 = u1 & q1 = v1;

      hereby

        assume (p,q) // (p1,q1);

        then [ [p, q], [p1, q1]] in the CONGR of ( Lambda ( OASpace V)) by ANALOAF:def 2;

        then [ [u, v], [u1, v1]] in ( lambda ( DirPar V)) by A1, Th17;

        hence ex a, b st (a * (v - u)) = (b * (v1 - u1)) & (a <> 0 or b <> 0 ) by Th15;

      end;

      given a, b such that

       A2: (a * (v - u)) = (b * (v1 - u1)) & (a <> 0 or b <> 0 );

       [ [u, v], [u1, v1]] in ( lambda ( DirPar V)) by A2, Th15;

      then [ [p, q], [p1, q1]] in the CONGR of ( Lambda ( OASpace V)) by A1, Th17;

      hence thesis by ANALOAF:def 2;

    end;

    definition

      struct ( 1-sorted) OrtStr (# the carrier -> set,

the orthogonality -> Relation of [: the carrier, the carrier:] #)

       attr strict strict;

    end

    definition

      struct ( AffinStruct, OrtStr) ParOrtStr (# the carrier -> set,

the CONGR, orthogonality -> Relation of [: the carrier, the carrier:] #)

       attr strict strict;

    end

    registration

      cluster non empty for ParOrtStr;

      existence

      proof

        set A = the non empty set, C = the Relation of [:A, A:];

        take ParOrtStr (# A, C, C #);

        thus the carrier of ParOrtStr (# A, C, C #) is non empty;

      end;

    end

    registration

      cluster non empty for OrtStr;

      existence

      proof

        set A = the non empty set, C = the Relation of [:A, A:];

        take OrtStr (# A, C #);

        thus the carrier of OrtStr (# A, C #) is non empty;

      end;

    end

    reserve POS for non empty ParOrtStr;

    definition

      let POS be OrtStr;

      let a,b,c,d be Element of POS;

      :: ANALMETR:def5

      pred a,b _|_ c,d means [ [a, b], [c, d]] in the orthogonality of POS;

    end

    definition

      let V, w, y;

      :: ANALMETR:def6

      func AMSpace (V,w,y) -> strict ParOrtStr equals ParOrtStr (# the carrier of V, ( lambda ( DirPar V)), ( Orthogonality (V,w,y)) #);

      correctness ;

    end

    registration

      let V, w, y;

      cluster ( AMSpace (V,w,y)) -> non empty;

      coherence ;

    end

    theorem :: ANALMETR:19

    the carrier of ( AMSpace (V,w,y)) = the carrier of V & the CONGR of ( AMSpace (V,w,y)) = ( lambda ( DirPar V)) & the orthogonality of ( AMSpace (V,w,y)) = ( Orthogonality (V,w,y));

    definition

      ::$Canceled

    end

    registration

      let POS;

      cluster the AffinStruct of POS -> non empty;

      coherence ;

    end

    theorem :: ANALMETR:20

    

     Th20: the AffinStruct of ( AMSpace (V,w,y)) = ( Lambda ( OASpace V))

    proof

      set Y = ( OASpace V);

      the carrier of ( Lambda Y) = the carrier of V by Th16;

      hence thesis by Th17;

    end;

    reserve p,p1,p2,q,q1,r,r1,r2 for Element of ( AMSpace (V,w,y));

    theorem :: ANALMETR:21

    

     Th21: p = u & p1 = u1 & q = v & q1 = v1 implies ((p,q) _|_ (p1,q1) iff (u,v,u1,v1) are_Ort_wrt (w,y))

    proof

      assume

       A1: p = u & p1 = u1 & q = v & q1 = v1;

      hereby

        assume (p,q) _|_ (p1,q1);

        then

        consider u9,v9,u19,v19 be VECTOR of V such that

         A2: [u, v] = [u9, v9] and

         A3: [u1, v1] = [u19, v19] and

         A4: (u9,v9,u19,v19) are_Ort_wrt (w,y) by A1, Def4;

        

         A5: u1 = u19 by A3, XTUPLE_0: 1;

        u = u9 & v = v9 by A2, XTUPLE_0: 1;

        hence (u,v,u1,v1) are_Ort_wrt (w,y) by A3, A4, A5, XTUPLE_0: 1;

      end;

      assume (u,v,u1,v1) are_Ort_wrt (w,y);

      hence thesis by A1, Def4;

    end;

    theorem :: ANALMETR:22

    

     Th22: p = u & q = v & p1 = u1 & q1 = v1 implies ((p,q) // (p1,q1) iff ex a, b st (a * (v - u)) = (b * (v1 - u1)) & (a <> 0 or b <> 0 ))

    proof

      assume

       A1: p = u & q = v & p1 = u1 & q1 = v1;

      hereby

        assume (p,q) // (p1,q1);

        then [ [p, q], [p1, q1]] in the CONGR of ( AMSpace (V,w,y)) by ANALOAF:def 2;

        hence ex a, b st (a * (v - u)) = (b * (v1 - u1)) & (a <> 0 or b <> 0 ) by A1, Th15;

      end;

      given a, b such that

       A2: (a * (v - u)) = (b * (v1 - u1)) & (a <> 0 or b <> 0 );

       [ [u, v], [u1, v1]] in ( lambda ( DirPar V)) by A2, Th15;

      hence thesis by A1, ANALOAF:def 2;

    end;

    theorem :: ANALMETR:23

    

     Th23: (p,q) _|_ (p1,q1) implies (p1,q1) _|_ (p,q)

    proof

      reconsider u = p, v = q, u1 = p1, v1 = q1 as Element of V;

      assume (p,q) _|_ (p1,q1);

      then (u,v,u1,v1) are_Ort_wrt (w,y) by Th21;

      then ((v - u),(v1 - u1)) are_Ort_wrt (w,y);

      then ((v1 - u1),(v - u)) are_Ort_wrt (w,y);

      then (u1,v1,u,v) are_Ort_wrt (w,y);

      hence thesis by Th21;

    end;

    theorem :: ANALMETR:24

    

     Th24: (p,q) _|_ (p1,q1) implies (p,q) _|_ (q1,p1)

    proof

      reconsider u = p, v = q, u1 = p1, v1 = q1 as Element of V;

      assume (p,q) _|_ (p1,q1);

      then (u,v,u1,v1) are_Ort_wrt (w,y) by Th21;

      then ((v - u),(v1 - u1)) are_Ort_wrt (w,y);

      then

       A1: ((v - u),(( - 1) * (v1 - u1))) are_Ort_wrt (w,y) by Th7;

      (( - 1) * (v1 - u1)) = ( - (v1 - u1)) by RLVECT_1: 16

      .= (u1 - v1) by RLVECT_1: 33;

      then (u,v,v1,u1) are_Ort_wrt (w,y) by A1;

      hence thesis by Th21;

    end;

    theorem :: ANALMETR:25

    

     Th25: Gen (w,y) implies for p, q, r holds (p,q) _|_ (r,r)

    proof

      assume

       A1: Gen (w,y);

      let p, q, r;

      reconsider u = p, v = q, u1 = r as Element of V;

      (u1 - u1) = ( 0. V) by RLVECT_1: 15;

      then ((v - u),(u1 - u1)) are_Ort_wrt (w,y) by A1, Th5;

      then (u,v,u1,u1) are_Ort_wrt (w,y);

      hence thesis by Th21;

    end;

    theorem :: ANALMETR:26

    

     Th26: (p,p1) _|_ (q,q1) & (p,p1) // (r,r1) implies p = p1 or (q,q1) _|_ (r,r1)

    proof

      assume that

       A1: (p,p1) _|_ (q,q1) and

       A2: (p,p1) // (r,r1);

      reconsider u = p, v = p1, u1 = q, v1 = q1, u2 = r, v2 = r1 as Element of V;

      consider a, b such that

       A3: (a * (v - u)) = (b * (v2 - u2)) and

       A4: a <> 0 or b <> 0 by A2, Th22;

      assume

       A5: p <> p1;

      b <> 0

      proof

        assume

         A6: b = 0 ;

        then (a * (v - u)) = ( 0. V) by A3, RLVECT_1: 10;

        then (v - u) = ( 0. V) by A4, A6, RLVECT_1: 11;

        hence contradiction by A5, RLVECT_1: 21;

      end;

      

      then

       A7: (v2 - u2) = ((b " ) * (a * (v - u))) by A3, ANALOAF: 5

      .= (((b " ) * a) * (v - u)) by RLVECT_1:def 7;

      (u,v,u1,v1) are_Ort_wrt (w,y) by A1, Th21;

      then ((v - u),(v1 - u1)) are_Ort_wrt (w,y);

      then ((v2 - u2),(v1 - u1)) are_Ort_wrt (w,y) by A7, Th7;

      then ((v1 - u1),(v2 - u2)) are_Ort_wrt (w,y);

      then (u1,v1,u2,v2) are_Ort_wrt (w,y);

      hence thesis by Th21;

    end;

    theorem :: ANALMETR:27

    

     Th27: Gen (w,y) implies for p, q, r holds ex r1 st (p,q) _|_ (r,r1) & r <> r1

    proof

      assume

       A1: Gen (w,y);

      let p, q, r;

      reconsider u = p, v = q, u1 = r as Element of V;

      consider v2 such that

       A2: ((v - u),v2) are_Ort_wrt (w,y) and

       A3: v2 <> ( 0. V) by A1, Th8;

      set v1 = (u1 + v2);

      reconsider r1 = v1 as Element of ( AMSpace (V,w,y));

      

       A4: (v1 - u1) = (v2 + (u1 - u1)) by RLVECT_1:def 3

      .= (v2 + ( 0. V)) by RLVECT_1: 15

      .= v2 by RLVECT_1: 4;

      then (u,v,u1,v1) are_Ort_wrt (w,y) by A2;

      then

       A5: (p,q) _|_ (r,r1) by Th21;

      r <> r1 by A3, A4, RLVECT_1: 15;

      hence thesis by A5;

    end;

    theorem :: ANALMETR:28

    

     Th28: Gen (w,y) & (p,p1) _|_ (q,q1) & (p,p1) _|_ (r,r1) implies p = p1 or (q,q1) // (r,r1)

    proof

      assume that

       A1: Gen (w,y) and

       A2: (p,p1) _|_ (q,q1) and

       A3: (p,p1) _|_ (r,r1);

      reconsider u = p, v = p1, u1 = q, v1 = q1, u2 = r, v2 = r1 as Element of V;

      (u,v,u2,v2) are_Ort_wrt (w,y) by A3, Th21;

      then

       A4: ((v - u),(v2 - u2)) are_Ort_wrt (w,y);

      assume p <> p1;

      then

       A5: (v - u) <> ( 0. V) by RLVECT_1: 21;

      (u,v,u1,v1) are_Ort_wrt (w,y) by A2, Th21;

      then ((v - u),(v1 - u1)) are_Ort_wrt (w,y);

      then ex a, b st (a * (v1 - u1)) = (b * (v2 - u2)) & (a <> 0 or b <> 0 ) by A1, A4, A5, Th9;

      hence thesis by Th22;

    end;

    theorem :: ANALMETR:29

    

     Th29: Gen (w,y) & (p,q) _|_ (r,r1) & (p,q) _|_ (r,r2) implies (p,q) _|_ (r1,r2)

    proof

      assume that

       A1: Gen (w,y) and

       A2: (p,q) _|_ (r,r1) and

       A3: (p,q) _|_ (r,r2);

      reconsider u = p, v = q, w1 = r, v1 = r1, v2 = r2 as Element of V;

      (u,v,w1,v2) are_Ort_wrt (w,y) by A3, Th21;

      then

       A4: ((v - u),(v2 - w1)) are_Ort_wrt (w,y);

      

       A5: ((v2 - w1) - (v1 - w1)) = (v2 - ((v1 - w1) + w1)) by RLVECT_1: 27

      .= (v2 - (v1 - (w1 - w1))) by RLVECT_1: 29

      .= (v2 - (v1 - ( 0. V))) by RLVECT_1: 15

      .= (v2 - v1) by RLVECT_1: 13;

      (u,v,w1,v1) are_Ort_wrt (w,y) by A2, Th21;

      then ((v - u),(v1 - w1)) are_Ort_wrt (w,y);

      then ((v - u),((v2 - w1) - (v1 - w1))) are_Ort_wrt (w,y) by A1, A4, Th10;

      then (u,v,v1,v2) are_Ort_wrt (w,y) by A5;

      hence thesis by Th21;

    end;

    theorem :: ANALMETR:30

    

     Th30: Gen (w,y) & (p,q) _|_ (p,q) implies p = q

    proof

      assume that

       A1: Gen (w,y) and

       A2: (p,q) _|_ (p,q);

      reconsider u = p, v = q as Element of V;

      (u,v,u,v) are_Ort_wrt (w,y) by A2, Th21;

      then ((v - u),(v - u)) are_Ort_wrt (w,y);

      then (v - u) = ( 0. V) by A1, Th11;

      hence thesis by RLVECT_1: 21;

    end;

    theorem :: ANALMETR:31

     Gen (w,y) & (p,q) _|_ (p1,p2) & (p1,q) _|_ (p2,p) implies (p2,q) _|_ (p,p1)

    proof

      assume that

       A1: Gen (w,y) and

       A2: (p,q) _|_ (p1,p2) and

       A3: (p1,q) _|_ (p2,p);

      reconsider u = p, v = q, u1 = p1, u2 = p2 as Element of V;

      (u,v,u1,u2) are_Ort_wrt (w,y) by A2, Th21;

      then

       A4: ((v - u),(u2 - u1)) are_Ort_wrt (w,y);

      (u1,v,u2,u) are_Ort_wrt (w,y) by A3, Th21;

      then

       A5: ((v - u1),(u - u2)) are_Ort_wrt (w,y);

       A6:

      now

        let u, v, w;

        

        thus ((u - v) - (u - w)) = ((w - u) + (u - v)) by RLVECT_1: 33

        .= (w - v) by ANALOAF: 1;

      end;

      then

       A7: ((v - u) - (v - u1)) = (u1 - u);

      ((v - u1) - (v - u2)) = (u2 - u1) & ((v - u2) - (v - u)) = (u - u2) by A6;

      then ((v - u2),((v - u) - (v - u1))) are_Ort_wrt (w,y) by A1, A4, A5, Th12;

      then (u2,v,u,u1) are_Ort_wrt (w,y) by A7;

      hence thesis by Th21;

    end;

    theorem :: ANALMETR:32

    

     Th32: Gen (w,y) & p <> p1 implies for q holds ex q1 st (p,p1) // (p,q1) & (p,p1) _|_ (q1,q)

    proof

      assume that

       A1: Gen (w,y) and

       A2: p <> p1;

      let q;

      reconsider u = p, v = q, u1 = p1 as Element of V;

      (u1 - u) <> ( 0. V) by A2, RLVECT_1: 21;

      then

      consider a such that

       A3: (((v - u) - (a * (u1 - u))),(u1 - u)) are_Ort_wrt (w,y) by A1, Th13;

      set v1 = (u + (a * (u1 - u)));

      reconsider q1 = v1 as Element of ( AMSpace (V,w,y));

      (v - v1) = ((v - u) - (a * (u1 - u))) by RLVECT_1: 27;

      then ((u1 - u),(v - v1)) are_Ort_wrt (w,y) by A3;

      then (u,u1,v1,v) are_Ort_wrt (w,y);

      then

       A4: (p,p1) _|_ (q1,q) by Th21;

      (a * (u1 - u)) = ((a * (u1 - u)) + ( 0. V)) by RLVECT_1: 4

      .= ((a * (u1 - u)) + (u - u)) by RLVECT_1: 15

      .= (v1 - u) by RLVECT_1:def 3

      .= (1 * (v1 - u)) by RLVECT_1:def 8;

      then (p,p1) // (p,q1) by Th22;

      hence thesis by A4;

    end;

    consider V0 be RealLinearSpace such that

     Lm6: ex w,y be VECTOR of V0 st Gen (w,y) by Th3;

    consider w0,y0 be VECTOR of V0 such that

     Lm7: Gen (w0,y0) by Lm6;

     Lm8:

    now

      set X = AffinStruct (# the carrier of ( AMSpace (V0,w0,y0)), the CONGR of ( AMSpace (V0,w0,y0)) #);

      

       A1: X = ( Lambda ( OASpace V0)) by Th20;

      for a,b be Real st ((a * w0) + (b * y0)) = ( 0. V0) holds a = 0 & b = 0 by Lm7;

      then ( OASpace V0) is OAffinSpace by ANALOAF: 26;

      hence AffinStruct (# the carrier of ( AMSpace (V0,w0,y0)), the CONGR of ( AMSpace (V0,w0,y0)) #) is AffinSpace & (for a,b,c,d,p,q,r,s be Element of ( AMSpace (V0,w0,y0)) holds ((a,b) _|_ (a,b) implies a = b) & (a,b) _|_ (c,c) & ((a,b) _|_ (c,d) implies (a,b) _|_ (d,c) & (c,d) _|_ (a,b)) & ((a,b) _|_ (p,q) & (a,b) // (r,s) implies (p,q) _|_ (r,s) or a = b) & ((a,b) _|_ (p,q) & (a,b) _|_ (p,s) implies (a,b) _|_ (q,s))) & (for a,b,c be Element of ( AMSpace (V0,w0,y0)) st a <> b holds ex x be Element of ( AMSpace (V0,w0,y0)) st (a,b) // (a,x) & (a,b) _|_ (x,c)) & for a,b,c be Element of ( AMSpace (V0,w0,y0)) holds ex x be Element of ( AMSpace (V0,w0,y0)) st (a,b) _|_ (c,x) & c <> x by A1, Lm7, Th23, Th24, Th25, Th26, Th27, Th29, Th30, Th32, DIRAF: 41;

    end;

    definition

      let IT be non empty ParOrtStr;

      :: ANALMETR:def8

      attr IT is OrtAfSp-like means

      : Def7: AffinStruct (# the carrier of IT, the CONGR of IT #) is AffinSpace & (for a,b,c,d,p,q,r,s be Element of IT holds ((a,b) _|_ (a,b) implies a = b) & (a,b) _|_ (c,c) & ((a,b) _|_ (c,d) implies (a,b) _|_ (d,c) & (c,d) _|_ (a,b)) & ((a,b) _|_ (p,q) & (a,b) // (r,s) implies (p,q) _|_ (r,s) or a = b) & ((a,b) _|_ (p,q) & (a,b) _|_ (p,s) implies (a,b) _|_ (q,s))) & (for a,b,c be Element of IT st a <> b holds ex x be Element of IT st (a,b) // (a,x) & (a,b) _|_ (x,c)) & for a,b,c be Element of IT holds ex x be Element of IT st (a,b) _|_ (c,x) & c <> x;

    end

    registration

      cluster strict OrtAfSp-like for non empty ParOrtStr;

      existence by Def7, Lm8;

    end

    definition

      mode OrtAfSp is OrtAfSp-like non empty ParOrtStr;

    end

    theorem :: ANALMETR:33

     Gen (w,y) implies ( AMSpace (V,w,y)) is OrtAfSp

    proof

      set POS = ( AMSpace (V,w,y));

      set X = AffinStruct (# the carrier of POS, the CONGR of POS #);

      assume

       A1: Gen (w,y);

      then

       A2: for a,b,c be Element of POS holds ex x be Element of POS st (a,b) _|_ (c,x) & c <> x by Th27;

      

       A3: X = ( Lambda ( OASpace V)) by Th20;

      for a,b be Real st ((a * w) + (b * y)) = ( 0. V) holds a = 0 & b = 0 by A1;

      then ( OASpace V) is OAffinSpace by ANALOAF: 26;

      then

       A4: X is AffinSpace by A3, DIRAF: 41;

      (for a,b,c,d,p,q,r,s be Element of POS holds ((a,b) _|_ (a,b) implies a = b) & (a,b) _|_ (c,c) & ((a,b) _|_ (c,d) implies (a,b) _|_ (d,c) & (c,d) _|_ (a,b)) & ((a,b) _|_ (p,q) & (a,b) // (r,s) implies (p,q) _|_ (r,s) or a = b) & ((a,b) _|_ (p,q) & (a,b) _|_ (p,s) implies (a,b) _|_ (q,s))) & for a,b,c be Element of POS holds a <> b implies ex x be Element of POS st (a,b) // (a,x) & (a,b) _|_ (x,c) by A1, Th23, Th24, Th25, Th26, Th29, Th30, Th32;

      hence thesis by A2, A4, Def7;

    end;

    consider V0 be RealLinearSpace such that

     Lm9: ex w,y be VECTOR of V0 st Gen (w,y) by Th3;

    consider w0,y0 be VECTOR of V0 such that

     Lm10: Gen (w0,y0) by Lm9;

     Lm11:

    now

      set X = AffinStruct (# the carrier of ( AMSpace (V0,w0,y0)), the CONGR of ( AMSpace (V0,w0,y0)) #);

      

       A1: X = ( Lambda ( OASpace V0)) by Th20;

      (for a,b be Real st ((a * w0) + (b * y0)) = ( 0. V0) holds a = 0 & b = 0 ) & for w1 be VECTOR of V0 holds ex a,b be Real st w1 = ((a * w0) + (b * y0)) by Lm10;

      then ( OASpace V0) is OAffinPlane by ANALOAF: 28;

      hence AffinStruct (# the carrier of ( AMSpace (V0,w0,y0)), the CONGR of ( AMSpace (V0,w0,y0)) #) is AffinPlane & (for a,b,c,d,p,q,r,s be Element of ( AMSpace (V0,w0,y0)) holds ((a,b) _|_ (a,b) implies a = b) & (a,b) _|_ (c,c) & ((a,b) _|_ (c,d) implies (a,b) _|_ (d,c) & (c,d) _|_ (a,b)) & ((a,b) _|_ (p,q) & (a,b) // (r,s) implies (p,q) _|_ (r,s) or a = b) & ((a,b) _|_ (p,q) & (a,b) _|_ (r,s) implies (p,q) // (r,s) or a = b)) & for a,b,c be Element of ( AMSpace (V0,w0,y0)) holds ex x be Element of ( AMSpace (V0,w0,y0)) st (a,b) _|_ (c,x) & c <> x by A1, Lm10, Th23, Th24, Th25, Th26, Th27, Th28, Th30, DIRAF: 45;

    end;

    definition

      let IT be non empty ParOrtStr;

      :: ANALMETR:def9

      attr IT is OrtAfPl-like means

      : Def8: AffinStruct (# the carrier of IT, the CONGR of IT #) is AffinPlane & (for a,b,c,d,p,q,r,s be Element of IT holds ((a,b) _|_ (a,b) implies a = b) & (a,b) _|_ (c,c) & ((a,b) _|_ (c,d) implies (a,b) _|_ (d,c) & (c,d) _|_ (a,b)) & ((a,b) _|_ (p,q) & (a,b) // (r,s) implies (p,q) _|_ (r,s) or a = b) & ((a,b) _|_ (p,q) & (a,b) _|_ (r,s) implies (p,q) // (r,s) or a = b)) & for a,b,c be Element of IT holds ex x be Element of IT st (a,b) _|_ (c,x) & c <> x;

    end

    registration

      cluster strict OrtAfPl-like for non empty ParOrtStr;

      existence by Def8, Lm11;

    end

    definition

      mode OrtAfPl is OrtAfPl-like non empty ParOrtStr;

    end

    theorem :: ANALMETR:34

     Gen (w,y) implies ( AMSpace (V,w,y)) is OrtAfPl

    proof

      set POS = ( AMSpace (V,w,y));

      set X = AffinStruct (# the carrier of POS, the CONGR of POS #);

      

       A1: X = ( Lambda ( OASpace V)) by Th20;

      assume

       A2: Gen (w,y);

      then (for a,b be Real st ((a * w) + (b * y)) = ( 0. V) holds a = 0 & b = 0 ) & for w1 holds ex a,b be Real st w1 = ((a * w) + (b * y));

      then ( OASpace V) is OAffinPlane by ANALOAF: 28;

      then

       A3: X is AffinPlane by A1, DIRAF: 45;

      (for a,b,c,d,p,q,r,s be Element of POS holds ((a,b) _|_ (a,b) implies a = b) & (a,b) _|_ (c,c) & ((a,b) _|_ (c,d) implies (a,b) _|_ (d,c) & (c,d) _|_ (a,b)) & ((a,b) _|_ (p,q) & (a,b) // (r,s) implies (p,q) _|_ (r,s) or a = b) & ((a,b) _|_ (p,q) & (a,b) _|_ (r,s) implies (p,q) // (r,s) or a = b)) & for a,b,c be Element of POS holds ex x be Element of POS st (a,b) _|_ (c,x) & c <> x by A2, Th23, Th24, Th25, Th26, Th27, Th28, Th30;

      hence thesis by A3, Def8;

    end;

    theorem :: ANALMETR:35

    for x be set holds (x is Element of POS iff x is Element of the AffinStruct of POS);

    theorem :: ANALMETR:36

    

     Th36: for a,b,c,d be Element of POS, a9,b9,c9,d9 be Element of the AffinStruct of POS st a = a9 & b = b9 & c = c9 & d = d9 holds ((a,b) // (c,d) iff (a9,b9) // (c9,d9))

    proof

      set AF = the AffinStruct of POS;

      let a,b,c,d be Element of POS, a9,b9,c9,d9 be Element of the AffinStruct of POS such that

       A1: a = a9 & b = b9 & c = c9 & d = d9;

      hereby

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

        then [ [a9, b9], [c9, d9]] in the CONGR of AF by A1, ANALOAF:def 2;

        hence (a9,b9) // (c9,d9) by ANALOAF:def 2;

      end;

      assume (a9,b9) // (c9,d9);

      then [ [a, b], [c, d]] in the CONGR of POS by A1, ANALOAF:def 2;

      hence thesis by ANALOAF:def 2;

    end;

    registration

      let POS be OrtAfSp;

      cluster the AffinStruct of POS -> AffinSpace-like non trivial;

      correctness by Def7;

    end

    registration

      let POS be OrtAfPl;

      cluster the AffinStruct of POS -> 2-dimensional AffinSpace-like non trivial;

      correctness by Def8;

    end

    theorem :: ANALMETR:37

    

     Th37: for POS be OrtAfPl holds POS is OrtAfSp

    proof

      let POS be OrtAfPl;

      for a,b,c,d,p,q,r,s be Element of POS holds ((a,b) _|_ (p,q) & (a,b) _|_ (p,s) implies (a,b) _|_ (q,s))

      proof

        let a,b,c,d,p,q,r,s be Element of POS such that

         A1: (a,b) _|_ (p,q) and

         A2: (a,b) _|_ (p,s);

         A3:

        now

          reconsider p9 = p, q9 = q, s9 = s as Element of the AffinStruct of POS;

          assume that

           A4: a <> b and

           A5: p <> q;

          (p,q) // (p,s) by A1, A2, A4, Def8;

          then (p9,q9) // (p9,s9) by Th36;

          then (q9,p9) // (q9,s9) by DIRAF: 40;

          then (p9,q9) // (q9,s9) by AFF_1: 4;

          then

           A6: (p,q) // (q,s) by Th36;

          (p,q) _|_ (a,b) by A1, Def8;

          hence thesis by A5, A6, Def8;

        end;

        now

          assume a = b;

          then (q,s) _|_ (a,b) by Def8;

          hence thesis by Def8;

        end;

        hence thesis by A2, A3;

      end;

      then

       A7: for a,b,c,d,p,q,r,s be Element of POS holds ((a,b) _|_ (a,b) implies a = b) & (a,b) _|_ (c,c) & ((a,b) _|_ (c,d) implies (a,b) _|_ (d,c) & (c,d) _|_ (a,b)) & ((a,b) _|_ (p,q) & (a,b) // (r,s) implies (p,q) _|_ (r,s) or a = b) & ((a,b) _|_ (p,q) & (a,b) _|_ (p,s) implies (a,b) _|_ (q,s)) by Def8;

      

       A8: for a,b,c be Element of POS st a <> b holds ex x be Element of POS st (a,b) // (a,x) & (a,b) _|_ (x,c)

      proof

        let a,b,c be Element of POS such that

         A9: a <> b;

        consider y be Element of POS such that

         A10: (a,b) _|_ (c,y) and

         A11: c <> y by Def8;

        reconsider a9 = a, b9 = b, c9 = c, y9 = y as Element of the AffinStruct of POS;

         not (a9,b9) // (c9,y9)

        proof

          assume not thesis;

          then (a,b) // (c,y) by Th36;

          then (c,y) _|_ (c,y) by A9, A10, Def8;

          hence contradiction by A11, Def8;

        end;

        then

        consider x9 be Element of the AffinStruct of POS such that

         A12: LIN (a9,b9,x9) and

         A13: LIN (c9,y9,x9) by AFF_1: 60;

        reconsider x = x9 as Element of POS;

        (c9,y9) // (c9,x9) by A13, AFF_1:def 1;

        then

         A14: (c,y) // (c,x) by Th36;

        (c,y) _|_ (a,b) by A10, Def8;

        then (a,b) _|_ (c,x) by A11, A14, Def8;

        then

         A15: (a,b) _|_ (x,c) by Def8;

        (a9,b9) // (a9,x9) by A12, AFF_1:def 1;

        then (a,b) // (a,x) by Th36;

        hence thesis by A15;

      end;

       the AffinStruct of POS = AffinStruct (# the carrier of POS, the CONGR of POS #) & for a,b,c be Element of POS holds ex x be Element of POS st (a,b) _|_ (c,x) & c <> x by Def8;

      hence thesis by A8, A7, Def7;

    end;

    registration

      cluster OrtAfPl-like -> OrtAfSp-like for non empty ParOrtStr;

      coherence by Th37;

    end

    theorem :: ANALMETR:38

    for POS be OrtAfSp st the AffinStruct of POS is AffinPlane holds POS is OrtAfPl

    proof

      let POS be OrtAfSp such that

       A1: the AffinStruct of POS is AffinPlane;

       A2:

      now

        let a,b,c,d,p,q,r,s be Element of POS;

        thus ((a,b) _|_ (a,b) implies a = b) & (a,b) _|_ (c,c) & ((a,b) _|_ (c,d) implies (a,b) _|_ (d,c) & (c,d) _|_ (a,b)) & ((a,b) _|_ (p,q) & (a,b) // (r,s) implies (p,q) _|_ (r,s) or a = b) by Def7;

        thus (a,b) _|_ (p,q) & (a,b) _|_ (r,s) implies (p,q) // (r,s) or a = b

        proof

          reconsider a9 = a, b9 = b, p9 = p, q9 = q, r9 = r, s9 = s as Element of the AffinStruct of POS;

          assume that

           A3: (a,b) _|_ (p,q) and

           A4: (a,b) _|_ (r,s);

          

           A5: (p,q) _|_ (a,b) by A3, Def7;

          

           A6: (r,s) _|_ (a,b) by A4, Def7;

          assume

           A7: not thesis;

          then

           A8: not (p9,q9) // (r9,s9) by Th36;

          then

           A9: p9 <> q9 by AFF_1: 3;

          consider x9 be Element of the AffinStruct of POS such that

           A10: LIN (p9,q9,x9) and

           A11: LIN (r9,s9,x9) by A1, A8, AFF_1: 60;

          reconsider x = x9 as Element of POS;

          

           A12: r9 <> s9 by A8, AFF_1: 3;

           LIN (s9,r9,x9) by A11, AFF_1: 6;

          then (s9,r9) // (s9,x9) by AFF_1:def 1;

          then

           A13: (r9,s9) // (x9,s9) by AFF_1: 4;

          then (r,s) // (x,s) by Th36;

          then (a,b) _|_ (x,s) by A12, A6, Def7;

          then

           A14: (x,s) _|_ (a,b) by Def7;

           LIN (q9,p9,x9) by A10, AFF_1: 6;

          then (q9,p9) // (q9,x9) by AFF_1:def 1;

          then (p9,q9) // (x9,q9) by AFF_1: 4;

          then (p,q) // (x,q) by Th36;

          then

           A15: (a,b) _|_ (x,q) by A9, A5, Def7;

           A16:

          now

            consider y9 be Element of the AffinStruct of POS such that

             A17: (a9,b9) // (q9,y9) & q9 <> y9 by DIRAF: 40;

            assume that

             A18: x <> q and

             A19: x <> s;

             not (q9,y9) // (x9,s9)

            proof

              assume not thesis;

              then (q9,y9) // (r9,s9) by A13, A19, AFF_1: 5;

              then (r9,s9) // (a9,b9) by A17, AFF_1: 5;

              then (r,s) // (a,b) by Th36;

              then (a,b) _|_ (a,b) by A12, A6, Def7;

              hence contradiction by A7, Def7;

            end;

            then

            consider z9 be Element of the AffinStruct of POS such that

             A20: LIN (q9,y9,z9) and

             A21: LIN (x9,s9,z9) by A1, AFF_1: 60;

            reconsider z = z9 as Element of POS;

            (q9,y9) // (q9,z9) by A20, AFF_1:def 1;

            then (a9,b9) // (q9,z9) by A17, AFF_1: 5;

            then

             A22: (a,b) // (q,z) by Th36;

            

             A23: (x9,s9) // (x9,z9) by A21, AFF_1:def 1;

            then (x,s) // (x,z) by Th36;

            then (a,b) _|_ (x,z) by A14, A19, Def7;

            then (a,b) _|_ (q,z) by A15, Def7;

            then (q,z) _|_ (q,z) by A7, A22, Def7;

            then (x9,s9) // (x9,q9) by A23, Def7;

            then

             A24: LIN (x9,s9,q9) by AFF_1:def 1;

             LIN (x9,s9,x9) & LIN (x9,q9,p9) by A10, AFF_1: 6, AFF_1: 7;

            then LIN (x9,s9,p9) by A18, A24, AFF_1: 11;

            then (x9,s9) // (p9,q9) by A24, AFF_1: 10;

            then (p9,q9) // (r9,s9) by A13, A19, AFF_1: 5;

            hence contradiction by A7, Th36;

          end;

          (r9,s9) // (r9,x9) by A11, AFF_1:def 1;

          then

           A25: (r9,s9) // (x9,r9) by AFF_1: 4;

          then (r,s) // (x,r) by Th36;

          then (a,b) _|_ (x,r) by A12, A6, Def7;

          then

           A26: (x,r) _|_ (a,b) by Def7;

           A27:

          now

            consider y9 be Element of the AffinStruct of POS such that

             A28: (a9,b9) // (q9,y9) & q9 <> y9 by DIRAF: 40;

            assume that

             A29: x <> q and

             A30: x <> r;

             not (q9,y9) // (x9,r9)

            proof

              assume not thesis;

              then (q9,y9) // (r9,s9) by A25, A30, AFF_1: 5;

              then (r9,s9) // (a9,b9) by A28, AFF_1: 5;

              then (r,s) // (a,b) by Th36;

              then (a,b) _|_ (a,b) by A12, A6, Def7;

              hence contradiction by A7, Def7;

            end;

            then

            consider z9 be Element of the AffinStruct of POS such that

             A31: LIN (q9,y9,z9) and

             A32: LIN (x9,r9,z9) by A1, AFF_1: 60;

            reconsider z = z9 as Element of POS;

            (q9,y9) // (q9,z9) by A31, AFF_1:def 1;

            then (a9,b9) // (q9,z9) by A28, AFF_1: 5;

            then

             A33: (a,b) // (q,z) by Th36;

            

             A34: (x9,r9) // (x9,z9) by A32, AFF_1:def 1;

            then (x,r) // (x,z) by Th36;

            then (a,b) _|_ (x,z) by A26, A30, Def7;

            then (a,b) _|_ (q,z) by A15, Def7;

            then (q,z) _|_ (q,z) by A7, A33, Def7;

            then (x9,r9) // (x9,q9) by A34, Def7;

            then

             A35: LIN (x9,r9,q9) by AFF_1:def 1;

             LIN (x9,r9,x9) & LIN (x9,q9,p9) by A10, AFF_1: 6, AFF_1: 7;

            then LIN (x9,r9,p9) by A29, A35, AFF_1: 11;

            then (x9,r9) // (p9,q9) by A35, AFF_1: 10;

            then (p9,q9) // (r9,s9) by A25, A30, AFF_1: 5;

            hence contradiction by A7, Th36;

          end;

          (p9,q9) // (p9,x9) by A10, AFF_1:def 1;

          then (p9,q9) // (x9,p9) by AFF_1: 4;

          then (p,q) // (x,p) by Th36;

          then

           A36: (a,b) _|_ (x,p) by A9, A5, Def7;

           A37:

          now

            consider y9 be Element of the AffinStruct of POS such that

             A38: (a9,b9) // (p9,y9) & p9 <> y9 by DIRAF: 40;

            assume that

             A39: x <> p and

             A40: x <> s;

             not (p9,y9) // (x9,s9)

            proof

              assume not thesis;

              then (p9,y9) // (r9,s9) by A13, A40, AFF_1: 5;

              then (r9,s9) // (a9,b9) by A38, AFF_1: 5;

              then (r,s) // (a,b) by Th36;

              then (a,b) _|_ (a,b) by A12, A6, Def7;

              hence contradiction by A7, Def7;

            end;

            then

            consider z9 be Element of the AffinStruct of POS such that

             A41: LIN (p9,y9,z9) and

             A42: LIN (x9,s9,z9) by A1, AFF_1: 60;

            reconsider z = z9 as Element of POS;

            (p9,y9) // (p9,z9) by A41, AFF_1:def 1;

            then (a9,b9) // (p9,z9) by A38, AFF_1: 5;

            then

             A43: (a,b) // (p,z) by Th36;

            

             A44: (x9,s9) // (x9,z9) by A42, AFF_1:def 1;

            then (x,s) // (x,z) by Th36;

            then (a,b) _|_ (x,z) by A14, A40, Def7;

            then (a,b) _|_ (p,z) by A36, Def7;

            then (p,z) _|_ (p,z) by A7, A43, Def7;

            then (x9,s9) // (x9,p9) by A44, Def7;

            then

             A45: LIN (x9,s9,p9) by AFF_1:def 1;

             LIN (x9,s9,x9) & LIN (x9,p9,q9) by A10, AFF_1: 6, AFF_1: 7;

            then LIN (x9,s9,q9) by A39, A45, AFF_1: 11;

            then (x9,s9) // (p9,q9) by A45, AFF_1: 10;

            then (p9,q9) // (r9,s9) by A13, A40, AFF_1: 5;

            hence contradiction by A7, Th36;

          end;

          now

            consider y9 be Element of the AffinStruct of POS such that

             A46: (a9,b9) // (p9,y9) & p9 <> y9 by DIRAF: 40;

            assume that

             A47: x <> p and

             A48: x <> r;

             not (p9,y9) // (x9,r9)

            proof

              assume not thesis;

              then (p9,y9) // (r9,s9) by A25, A48, AFF_1: 5;

              then (r9,s9) // (a9,b9) by A46, AFF_1: 5;

              then (r,s) // (a,b) by Th36;

              then (a,b) _|_ (a,b) by A12, A6, Def7;

              hence contradiction by A7, Def7;

            end;

            then

            consider z9 be Element of the AffinStruct of POS such that

             A49: LIN (p9,y9,z9) and

             A50: LIN (x9,r9,z9) by A1, AFF_1: 60;

            reconsider z = z9 as Element of POS;

            (p9,y9) // (p9,z9) by A49, AFF_1:def 1;

            then (a9,b9) // (p9,z9) by A46, AFF_1: 5;

            then

             A51: (a,b) // (p,z) by Th36;

            

             A52: (x9,r9) // (x9,z9) by A50, AFF_1:def 1;

            then (x,r) // (x,z) by Th36;

            then (a,b) _|_ (x,z) by A26, A48, Def7;

            then (a,b) _|_ (p,z) by A36, Def7;

            then (p,z) _|_ (p,z) by A7, A51, Def7;

            then (x9,r9) // (x9,p9) by A52, Def7;

            then

             A53: LIN (x9,r9,p9) by AFF_1:def 1;

             LIN (x9,r9,x9) & LIN (x9,p9,q9) by A10, AFF_1: 6, AFF_1: 7;

            then LIN (x9,r9,q9) by A47, A53, AFF_1: 11;

            then (x9,r9) // (p9,q9) by A53, AFF_1: 10;

            then (p9,q9) // (r9,s9) by A25, A48, AFF_1: 5;

            hence contradiction by A7, Th36;

          end;

          hence contradiction by A8, A37, A27, A16, AFF_1: 3;

        end;

      end;

      for a,b,c be Element of POS holds ex x be Element of POS st (a,b) _|_ (c,x) & c <> x by Def7;

      hence thesis by A1, A2, Def8;

    end;

    theorem :: ANALMETR:39

    for POS be non empty ParOrtStr holds POS is OrtAfPl-like iff (ex a,b be Element of POS st a <> b) & for a,b,c,d,p,q,r,s be Element of POS holds (a,b) // (b,a) & (a,b) // (c,c) & ((a,b) // (p,q) & (a,b) // (r,s) implies (p,q) // (r,s) or a = b) & ((a,b) // (a,c) implies (b,a) // (b,c)) & (ex x be Element of POS st (a,b) // (c,x) & (a,c) // (b,x)) & (ex x,y,z be Element of POS st not (x,y) // (x,z)) & (ex x be Element of POS st (a,b) // (c,x) & c <> x) & ((a,b) // (b,d) & b <> a implies ex x be Element of POS st (c,b) // (b,x) & (c,a) // (d,x)) & ((a,b) _|_ (a,b) implies a = b) & (a,b) _|_ (c,c) & ((a,b) _|_ (c,d) implies (a,b) _|_ (d,c) & (c,d) _|_ (a,b)) & ((a,b) _|_ (p,q) & (a,b) // (r,s) implies (p,q) _|_ (r,s) or a = b) & ((a,b) _|_ (p,q) & (a,b) _|_ (r,s) implies (p,q) // (r,s) or a = b) & (ex x be Element of POS st (a,b) _|_ (c,x) & c <> x) & ( not (a,b) // (c,d) implies ex x be Element of POS st (a,b) // (a,x) & (c,d) // (c,x))

    proof

      let POS be non empty ParOrtStr;

      set P = the AffinStruct of POS;

      hereby

        assume

         A1: POS is OrtAfPl-like;

        then P is AffinPlane;

        hence ex x,y be Element of POS st x <> y by DIRAF: 46;

        let a,b,c,d,p,q,r,s be Element of POS;

        reconsider a9 = a, b9 = b, c9 = c, d9 = d, p9 = p, q9 = q, r9 = r, s9 = s as Element of P;

        consider x9 be Element of P such that

         A2: (a9,b9) // (c9,x9) & (a9,c9) // (b9,x9) by A1, DIRAF: 46;

        (a9,b9) // (b9,a9) & (a9,b9) // (c9,c9) by A1, DIRAF: 46;

        hence (a,b) // (b,a) & (a,b) // (c,c) by Th36;

        hereby

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

          then (a9,b9) // (p9,q9) & (a9,b9) // (r9,s9) by Th36;

          then (p9,q9) // (r9,s9) or a9 = b9 by A1, DIRAF: 46;

          hence (p,q) // (r,s) or a = b by Th36;

        end;

        hereby

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

          then (a9,b9) // (a9,c9) by Th36;

          then (b9,a9) // (b9,c9) by A1, DIRAF: 46;

          hence (b,a) // (b,c) by Th36;

        end;

        reconsider x = x9 as Element of POS;

        consider x9,y9,z9 be Element of P such that

         A3: not (x9,y9) // (x9,z9) by A1, DIRAF: 46;

        (a,b) // (c,x) & (a,c) // (b,x) by A2, Th36;

        hence ex x be Element of POS st (a,b) // (c,x) & (a,c) // (b,x);

        reconsider x = x9, y = y9, z = z9 as Element of POS;

        consider x9 be Element of P such that

         A4: (a9,b9) // (c9,x9) and

         A5: c9 <> x9 by A1, DIRAF: 46;

         not (x,y) // (x,z) by A3, Th36;

        hence ex x,y,z be Element of POS st not (x,y) // (x,z);

        reconsider x = x9 as Element of POS;

        (a,b) // (c,x) by A4, Th36;

        hence ex x be Element of POS st (a,b) // (c,x) & c <> x by A5;

        hereby

          assume that

           A6: (a,b) // (b,d) and

           A7: b <> a;

          (a9,b9) // (b9,d9) by A6, Th36;

          then

          consider x9 be Element of P such that

           A8: (c9,b9) // (b9,x9) & (c9,a9) // (d9,x9) by A1, A7, DIRAF: 46;

          reconsider x = x9 as Element of POS;

          (c,b) // (b,x) & (c,a) // (d,x) by A8, Th36;

          hence ex x be Element of POS st (c,b) // (b,x) & (c,a) // (d,x);

        end;

        thus ((a,b) _|_ (a,b) implies a = b) & (a,b) _|_ (c,c) & ((a,b) _|_ (c,d) implies (a,b) _|_ (d,c) & (c,d) _|_ (a,b)) & ((a,b) _|_ (p,q) & (a,b) // (r,s) implies (p,q) _|_ (r,s) or a = b) & ((a,b) _|_ (p,q) & (a,b) _|_ (r,s) implies (p,q) // (r,s) or a = b) & ex x be Element of POS st (a,b) _|_ (c,x) & c <> x by A1;

        assume not (a,b) // (c,d);

        then not (a9,b9) // (c9,d9) by Th36;

        then

        consider x9 be Element of P such that

         A9: (a9,b9) // (a9,x9) & (c9,d9) // (c9,x9) by A1, DIRAF: 46;

        reconsider x = x9 as Element of POS;

        (a,b) // (a,x) & (c,d) // (c,x) by A9, Th36;

        hence ex x be Element of POS st (a,b) // (a,x) & (c,d) // (c,x);

      end;

      given a,b be Element of POS such that

       A10: a <> b;

      assume

       A11: for a,b,c,d,p,q,r,s be Element of POS holds (a,b) // (b,a) & (a,b) // (c,c) & ((a,b) // (p,q) & (a,b) // (r,s) implies (p,q) // (r,s) or a = b) & ((a,b) // (a,c) implies (b,a) // (b,c)) & (ex x be Element of POS st (a,b) // (c,x) & (a,c) // (b,x)) & (ex x,y,z be Element of POS st not (x,y) // (x,z)) & (ex x be Element of POS st (a,b) // (c,x) & c <> x) & ((a,b) // (b,d) & b <> a implies ex x be Element of POS st (c,b) // (b,x) & (c,a) // (d,x)) & ((a,b) _|_ (a,b) implies a = b) & (a,b) _|_ (c,c) & ((a,b) _|_ (c,d) implies (a,b) _|_ (d,c) & (c,d) _|_ (a,b)) & ((a,b) _|_ (p,q) & (a,b) // (r,s) implies (p,q) _|_ (r,s) or a = b) & ((a,b) _|_ (p,q) & (a,b) _|_ (r,s) implies (p,q) // (r,s) or a = b) & (ex x be Element of POS st (a,b) _|_ (c,x) & c <> x) & ( not (a,b) // (c,d) implies ex x be Element of POS st (a,b) // (a,x) & (c,d) // (c,x));

       A12:

      now

        let x,y,z be Element of P;

        reconsider x9 = x, y9 = y, z9 = z as Element of POS;

        consider t9 be Element of POS such that

         A13: (x9,z9) // (y9,t9) and

         A14: y9 <> t9 by A11;

        reconsider t = t9 as Element of P;

        (x,z) // (y,t) by A13, Th36;

        hence ex t be Element of P st (x,z) // (y,t) & y <> t by A14;

      end;

       A15:

      now

        let x,y,z,t,u,w be Element of P;

        reconsider a = x, b = y, c = z, d = t, e = u, f = w as Element of POS;

        (a,b) // (b,a) & (a,b) // (c,c) by A11;

        hence (x,y) // (y,x) & (x,y) // (z,z) by Th36;

        thus x <> y & (x,y) // (z,t) & (x,y) // (u,w) implies (z,t) // (u,w)

        proof

          assume that

           A16: x <> y and

           A17: (x,y) // (z,t) & (x,y) // (u,w);

          (a,b) // (c,d) & (a,b) // (e,f) by A17, Th36;

          then (c,d) // (e,f) by A11, A16;

          hence thesis by Th36;

        end;

        thus (x,y) // (x,z) implies (y,x) // (y,z)

        proof

          assume (x,y) // (x,z);

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

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

          hence thesis by Th36;

        end;

      end;

       A18:

      now

        let x,y,z,t be Element of P such that

         A19: not (x,y) // (z,t);

        reconsider x9 = x, y9 = y, z9 = z, t9 = t as Element of POS;

         not (x9,y9) // (z9,t9) by A19, Th36;

        then

        consider u9 be Element of POS such that

         A20: (x9,y9) // (x9,u9) & (z9,t9) // (z9,u9) by A11;

        reconsider u = u9 as Element of P;

        (x,y) // (x,u) & (z,t) // (z,u) by A20, Th36;

        hence ex u be Element of P st (x,y) // (x,u) & (z,t) // (z,u);

      end;

       A21:

      now

        let x,y,z,t be Element of P such that

         A22: (z,x) // (x,t) and

         A23: x <> z;

        reconsider x9 = x, y9 = y, z9 = z, t9 = t as Element of POS;

        (z9,x9) // (x9,t9) by A22, Th36;

        then

        consider u9 be Element of POS such that

         A24: (y9,x9) // (x9,u9) & (y9,z9) // (t9,u9) by A11, A23;

        reconsider u = u9 as Element of P;

        (y,x) // (x,u) & (y,z) // (t,u) by A24, Th36;

        hence ex u be Element of P st (y,x) // (x,u) & (y,z) // (t,u);

      end;

       A25:

      now

        let x,y,z be Element of P;

        reconsider x9 = x, y9 = y, z9 = z as Element of POS;

        consider t9 be Element of POS such that

         A26: (x9,y9) // (z9,t9) & (x9,z9) // (y9,t9) by A11;

        reconsider t = t9 as Element of P;

        (x,y) // (z,t) & (x,z) // (y,t) by A26, Th36;

        hence ex t be Element of P st (x,y) // (z,t) & (x,z) // (y,t);

      end;

      ex x,y,z be Element of P st not (x,y) // (x,z)

      proof

        consider x,y,z be Element of POS such that

         A27: not (x,y) // (x,z) by A11;

        reconsider x9 = x, y9 = y, z9 = z as Element of P;

         not (x9,y9) // (x9,z9) by A27, Th36;

        hence thesis;

      end;

      hence AffinStruct (# the carrier of POS, the CONGR of POS #) is AffinPlane by A10, A15, A12, A25, A21, A18, DIRAF: 46;

      thus for a,b,c,d,p,q,r,s be Element of POS holds ((a,b) _|_ (a,b) implies a = b) & (a,b) _|_ (c,c) & ((a,b) _|_ (c,d) implies (a,b) _|_ (d,c) & (c,d) _|_ (a,b)) & ((a,b) _|_ (p,q) & (a,b) // (r,s) implies (p,q) _|_ (r,s) or a = b) & ((a,b) _|_ (p,q) & (a,b) _|_ (r,s) implies (p,q) // (r,s) or a = b) by A11;

      thus thesis by A11;

    end;

    reserve x,a,b,c,d,p,q,y for Element of POS;

    definition

      let POS;

      let a, b, c;

      :: ANALMETR:def10

      pred LIN a,b,c means (a,b) // (a,c);

    end

    definition

      let POS, a, b;

      :: ANALMETR:def11

      func Line (a,b) -> Subset of POS means

      : Def10: for x be Element of POS holds x in it iff LIN (a,b,x);

      existence

      proof

        defpred P[ set] means for y st y = $1 holds LIN (a,b,y);

        consider X be Subset of POS such that

         A1: for x be set holds x in X iff x in the carrier of POS & P[x] from SUBSET_1:sch 1;

        take X;

        let x be Element of POS;

        thus x in X implies LIN (a,b,x) by A1;

        assume LIN (a,b,x);

        then for y st y = x holds LIN (a,b,y);

        hence thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of POS such that

         A2: for x holds x in X1 iff LIN (a,b,x) and

         A3: for x holds x in X2 iff LIN (a,b,x);

        for x be object holds x in X1 iff x in X2 by A2, A3;

        hence thesis by TARSKI: 2;

      end;

    end

    reserve A,K,M for Subset of POS;

    definition

      let POS;

      let A;

      :: ANALMETR:def12

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

    end

    theorem :: ANALMETR:40

    

     Th40: for POS be OrtAfSp holds for a,b,c be Element of POS, a9,b9,c9 be Element of the AffinStruct of POS st a = a9 & b = b9 & c = c9 holds ( LIN (a,b,c) iff LIN (a9,b9,c9))

    proof

      let POS be OrtAfSp;

      let a,b,c be Element of POS, a9,b9,c9 be Element of the AffinStruct of POS such that

       A1: a = a9 & b = b9 & c = c9;

      hereby

        assume LIN (a,b,c);

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

        then (a9,b9) // (a9,c9) by A1, Th36;

        hence LIN (a9,b9,c9) by AFF_1:def 1;

      end;

      assume LIN (a9,b9,c9);

      then (a9,b9) // (a9,c9) by AFF_1:def 1;

      then (a,b) // (a,c) by A1, Th36;

      hence thesis;

    end;

    theorem :: ANALMETR:41

    

     Th41: for POS be OrtAfSp holds for a,b be Element of POS, a9,b9 be Element of the AffinStruct of POS st a = a9 & b = b9 holds ( Line (a,b)) = ( Line (a9,b9))

    proof

      let POS be OrtAfSp;

      let a,b be Element of POS, a9,b9 be Element of the AffinStruct of POS such that

       A1: a = a9 & b = b9;

      set X = ( Line (a,b)), Y = ( Line (a9,b9));

      now

        let x1 be object;

         A2:

        now

          assume

           A3: x1 in Y;

          then

          reconsider x9 = x1 as Element of the AffinStruct of POS;

          reconsider x = x9 as Element of POS;

           LIN (a9,b9,x9) by A3, AFF_1:def 2;

          then LIN (a,b,x) by A1, Th40;

          hence x1 in X by Def10;

        end;

        now

          assume

           A4: x1 in X;

          then

          reconsider x = x1 as Element of POS;

          reconsider x9 = x as Element of the AffinStruct of POS;

           LIN (a,b,x) by A4, Def10;

          then LIN (a9,b9,x9) by A1, Th40;

          hence x1 in Y by AFF_1:def 2;

        end;

        hence x1 in X iff x1 in Y by A2;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: ANALMETR:42

    for X be set holds X is Subset of POS iff X is Subset of the AffinStruct of POS;

    theorem :: ANALMETR:43

    

     Th43: for POS be OrtAfSp holds for X be Subset of POS, Y be Subset of the AffinStruct of POS st X = Y holds X is being_line iff Y is being_line

    proof

      let POS be OrtAfSp;

      let X be Subset of the carrier of POS, Y be Subset of the AffinStruct of POS such that

       A1: X = Y;

      hereby

        assume X is being_line;

        then

        consider a,b be Element of POS such that

         A2: a <> b and

         A3: X = ( Line (a,b));

        reconsider a9 = a, b9 = b as Element of the AffinStruct of POS;

        Y = ( Line (a9,b9)) by A1, A3, Th41;

        hence Y is being_line by A2, AFF_1:def 3;

      end;

      assume Y is being_line;

      then

      consider a9,b9 be Element of the AffinStruct of POS such that

       A4: a9 <> b9 and

       A5: Y = ( Line (a9,b9)) by AFF_1:def 3;

      reconsider a = a9, b = b9 as Element of POS;

      X = ( Line (a,b)) by A1, A5, Th41;

      hence thesis by A4;

    end;

    definition

      let POS;

      let a, b, K;

      :: ANALMETR:def13

      pred a,b _|_ K means ex p, q st p <> q & K = ( Line (p,q)) & (a,b) _|_ (p,q);

    end

    definition

      let POS;

      let K, M;

      :: ANALMETR:def14

      pred K _|_ M means

      : Def13: ex p, q st p <> q & K = ( Line (p,q)) & (p,q) _|_ M;

    end

    definition

      let POS;

      let K, M;

      :: ANALMETR:def15

      pred K // M means ex a, b, c, d st a <> b & c <> d & K = ( Line (a,b)) & M = ( Line (c,d)) & (a,b) // (c,d);

    end

    theorem :: ANALMETR:44

    

     Th44: ((a,b) _|_ K implies K is being_line) & (K _|_ M implies K is being_line & M is being_line)

    proof

      for a, b, K st (a,b) _|_ K holds K is being_line;

      then K _|_ M implies K is being_line & M is being_line;

      hence thesis;

    end;

    theorem :: ANALMETR:45

    

     Th45: K _|_ M iff ex a, b, c, d st a <> b & c <> d & K = ( Line (a,b)) & M = ( Line (c,d)) & (a,b) _|_ (c,d)

    proof

      hereby

        assume K _|_ M;

        then

        consider a, b such that

         A1: a <> b & K = ( Line (a,b)) and

         A2: (a,b) _|_ M;

        ex c, d st c <> d & M = ( Line (c,d)) & (a,b) _|_ (c,d) by A2;

        hence ex a, b, c, d st a <> b & c <> d & K = ( Line (a,b)) & M = ( Line (c,d)) & (a,b) _|_ (c,d) by A1;

      end;

      given a, b, c, d such that

       A3: a <> b and

       A4: c <> d and

       A5: K = ( Line (a,b)) and

       A6: M = ( Line (c,d)) & (a,b) _|_ (c,d);

      (a,b) _|_ M by A4, A6;

      hence thesis by A3, A5;

    end;

    theorem :: ANALMETR:46

    

     Th46: for POS be OrtAfSp holds for M,N be Subset of POS, M9,N9 be Subset of the AffinStruct of POS st M = M9 & N = N9 holds M // N iff M9 // N9

    proof

      let POS be OrtAfSp;

      let M,N be Subset of POS, M9,N9 be Subset of the AffinStruct of POS such that

       A1: M = M9 & N = N9;

      hereby

        assume M // N;

        then

        consider a,b,c,d be Element of POS such that

         A2: a <> b & c <> d and

         A3: M = ( Line (a,b)) & N = ( Line (c,d)) and

         A4: (a,b) // (c,d);

        reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of the AffinStruct of POS;

        

         A5: (a9,b9) // (c9,d9) by A4, Th36;

        M9 = ( Line (a9,b9)) & N9 = ( Line (c9,d9)) by A1, A3, Th41;

        hence M9 // N9 by A2, A5, AFF_1: 37;

      end;

      assume M9 // N9;

      then

      consider a9,b9,c9,d9 be Element of the AffinStruct of POS such that

       A6: a9 <> b9 & c9 <> d9 and

       A7: (a9,b9) // (c9,d9) and

       A8: M9 = ( Line (a9,b9)) & N9 = ( Line (c9,d9)) by AFF_1: 37;

      reconsider a = a9, b = b9, c = c9, d = d9 as Element of POS;

      

       A9: (a,b) // (c,d) by A7, Th36;

      M = ( Line (a,b)) & N = ( Line (c,d)) by A1, A8, Th41;

      hence thesis by A6, A9;

    end;

    reserve POS for OrtAfSp;

    reserve A,K,M,N for Subset of POS;

    reserve a,b,c,d,p,q,r,s for Element of POS;

    theorem :: ANALMETR:47

    K is being_line implies (a,a) _|_ K

    proof

      assume K is being_line;

      then

      consider p, q such that

       A1: p <> q & K = ( Line (p,q));

      (p,q) _|_ (a,a) by Def7;

      then (a,a) _|_ (p,q) by Def7;

      hence thesis by A1;

    end;

    theorem :: ANALMETR:48

    (a,b) _|_ K & ((a,b) // (c,d) or (c,d) // (a,b)) & a <> b implies (c,d) _|_ K

    proof

      assume that

       A1: (a,b) _|_ K and

       A2: (a,b) // (c,d) or (c,d) // (a,b) and

       A3: a <> b;

      reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of the AffinStruct of POS;

      consider p, q such that

       A4: p <> q & K = ( Line (p,q)) and

       A5: (a,b) _|_ (p,q) by A1;

      (a9,b9) // (c9,d9) or (c9,d9) // (a9,b9) by A2, Th36;

      then (a9,b9) // (c9,d9) by AFF_1: 4;

      then (a,b) // (c,d) by Th36;

      then (p,q) _|_ (c,d) by A3, A5, Def7;

      then (c,d) _|_ (p,q) by Def7;

      hence thesis by A4;

    end;

    theorem :: ANALMETR:49

    (a,b) _|_ K implies (b,a) _|_ K

    proof

      assume (a,b) _|_ K;

      then

      consider p, q such that

       A1: p <> q & K = ( Line (p,q)) and

       A2: (a,b) _|_ (p,q);

      (p,q) _|_ (a,b) by A2, Def7;

      then (p,q) _|_ (b,a) by Def7;

      then (b,a) _|_ (p,q) by Def7;

      hence thesis by A1;

    end;

    definition

      let POS;

      let K,M be Subset of POS;

      :: original: //

      redefine

      pred K // M;

      symmetry

      proof

        let K,M be Subset of POS;

        assume K // M;

        then

        consider a, b, c, d such that

         A1: a <> b & c <> d & K = ( Line (a,b)) & M = ( Line (c,d)) and

         A2: (a,b) // (c,d);

        reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of the AffinStruct of POS;

        (a9,b9) // (c9,d9) by A2, Th36;

        then (c9,d9) // (a9,b9) by AFF_1: 4;

        then (c,d) // (a,b) by Th36;

        hence thesis by A1;

      end;

    end

    theorem :: ANALMETR:50

    

     Th50: (r,s) _|_ K & K // M implies (r,s) _|_ M

    proof

      assume that

       A1: (r,s) _|_ K and

       A2: K // M;

      consider p, q such that

       A3: p <> q and

       A4: K = ( Line (p,q)) and

       A5: (r,s) _|_ (p,q) by A1;

      consider a, b, c, d such that

       A6: a <> b and

       A7: c <> d and

       A8: K = ( Line (a,b)) and

       A9: M = ( Line (c,d)) and

       A10: (a,b) // (c,d) by A2;

      reconsider p9 = p, q9 = q, a9 = a, b9 = b, c9 = c, d9 = d as Element of the AffinStruct of POS;

      

       A11: K = ( Line (a9,b9)) by A8, Th41;

      

       A12: K = ( Line (p9,q9)) by A4, Th41;

      then q9 in K by AFF_1: 15;

      then

       A13: LIN (a9,b9,q9) by A11, AFF_1:def 2;

      p9 in K by A12, AFF_1: 15;

      then LIN (a9,b9,p9) by A11, AFF_1:def 2;

      then

       A14: (a9,b9) // (p9,q9) by A13, AFF_1: 10;

      

       A15: (p,q) _|_ (r,s) by A5, Def7;

      (a9,b9) // (c9,d9) by A10, Th36;

      then (p9,q9) // (c9,d9) by A6, A14, AFF_1: 5;

      then (p,q) // (c,d) by Th36;

      then (r,s) _|_ (c,d) by A3, A15, Def7;

      hence thesis by A7, A9;

    end;

    theorem :: ANALMETR:51

    

     Th51: a in K & b in K & (a,b) _|_ K implies a = b

    proof

      assume that

       A1: a in K and

       A2: b in K and

       A3: (a,b) _|_ K;

      consider p, q such that

       A4: p <> q and

       A5: K = ( Line (p,q)) and

       A6: (a,b) _|_ (p,q) by A3;

      reconsider a9 = a, b9 = b, p9 = p, q9 = q as Element of the AffinStruct of POS;

      set K9 = ( Line (p9,q9));

      b9 in K9 by A2, A5, Th41;

      then

       A7: LIN (p9,q9,b9) by AFF_1:def 2;

      a9 in K9 by A1, A5, Th41;

      then LIN (p9,q9,a9) by AFF_1:def 2;

      then (p9,q9) // (a9,b9) by A7, AFF_1: 10;

      then

       A8: (p,q) // (a,b) by Th36;

      (p,q) _|_ (a,b) by A6, Def7;

      then (a,b) _|_ (a,b) by A4, A8, Def7;

      hence thesis by Def7;

    end;

    definition

      let POS;

      let K,M be Subset of POS;

      :: original: _|_

      redefine

      pred K _|_ M;

      irreflexivity

      proof

        let K be Subset of POS;

        assume not thesis;

        then

        consider a, b such that

         A1: a <> b and

         A2: K = ( Line (a,b)) and

         A3: (a,b) _|_ K;

        reconsider a9 = a, b9 = b as Element of the AffinStruct of POS;

        K = ( Line (a9,b9)) by A2, Th41;

        then a in K & b in K by AFF_1: 15;

        hence contradiction by A1, A3, Th51;

      end;

      symmetry

      proof

        let K,M be Subset of POS;

        assume K _|_ M;

        then

        consider a, b, c, d such that

         A4: a <> b & c <> d & K = ( Line (a,b)) & M = ( Line (c,d)) and

         A5: (a,b) _|_ (c,d) by Th45;

        (c,d) _|_ (a,b) by A5, Def7;

        hence thesis by A4, Th45;

      end;

    end

    theorem :: ANALMETR:52

    

     Th52: K _|_ M & K // N implies N _|_ M

    proof

      assume that

       A1: K _|_ M and

       A2: K // N;

      consider r, s such that

       A3: r <> s & M = ( Line (r,s)) and

       A4: (r,s) _|_ K by A1, Def13;

      (r,s) _|_ N by A2, A4, Th50;

      hence thesis by A3, Def13;

    end;

    theorem :: ANALMETR:53

    a in K & b in K & (c,d) _|_ K implies (c,d) _|_ (a,b) & (a,b) _|_ (c,d)

    proof

      assume that

       A1: a in K and

       A2: b in K and

       A3: (c,d) _|_ K;

      consider p, q such that

       A4: p <> q and

       A5: K = ( Line (p,q)) and

       A6: (c,d) _|_ (p,q) by A3;

      reconsider a9 = a, b9 = b, p9 = p, q9 = q as Element of the AffinStruct of POS;

       LIN (p,q,b) by A2, A5, Def10;

      then

       A7: LIN (p9,q9,b9) by Th40;

       LIN (p,q,a) by A1, A5, Def10;

      then LIN (p9,q9,a9) by Th40;

      then (p9,q9) // (a9,b9) by A7, AFF_1: 10;

      then

       A8: (p,q) // (a,b) by Th36;

      (p,q) _|_ (c,d) by A6, Def7;

      hence (c,d) _|_ (a,b) by A4, A8, Def7;

      hence thesis by Def7;

    end;

    theorem :: ANALMETR:54

    

     Th54: a in K & b in K & a <> b & K is being_line implies K = ( Line (a,b))

    proof

      assume that

       A1: a in K & b in K & a <> b and

       A2: K is being_line;

      reconsider a9 = a, b9 = b as Element of the AffinStruct of POS;

      reconsider K9 = K as Subset of the AffinStruct of POS;

      K9 is being_line by A2, Th43;

      then K9 = ( Line (a9,b9)) by A1, AFF_1: 57;

      hence thesis by Th41;

    end;

    theorem :: ANALMETR:55

    a in K & b in K & a <> b & K is being_line & ((a,b) _|_ (c,d) or (c,d) _|_ (a,b)) implies (c,d) _|_ K

    proof

      assume that

       A1: a in K & b in K and

       A2: a <> b and

       A3: K is being_line & ((a,b) _|_ (c,d) or (c,d) _|_ (a,b));

      (c,d) _|_ (a,b) & K = ( Line (a,b)) by A1, A2, A3, Def7, Th54;

      hence thesis by A2;

    end;

    theorem :: ANALMETR:56

    

     Th56: a in M & b in M & c in N & d in N & M _|_ N implies (a,b) _|_ (c,d)

    proof

      assume that

       A1: a in M and

       A2: b in M and

       A3: c in N and

       A4: d in N and

       A5: M _|_ N;

      consider p1,q1,p2,q2 be Element of POS such that

       A6: p1 <> q1 and

       A7: p2 <> q2 and

       A8: M = ( Line (p1,q1)) and

       A9: N = ( Line (p2,q2)) and

       A10: (p1,q1) _|_ (p2,q2) by A5, Th45;

      reconsider a9 = a, b9 = b, c9 = c, d9 = d, p19 = p1, q19 = q1, p29 = p2, q29 = q2 as Element of the AffinStruct of POS;

       LIN (p1,q1,b) by A2, A8, Def10;

      then

       A11: LIN (p19,q19,b9) by Th40;

       LIN (p1,q1,a) by A1, A8, Def10;

      then LIN (p19,q19,a9) by Th40;

      then (p19,q19) // (a9,b9) by A11, AFF_1: 10;

      then (p1,q1) // (a,b) by Th36;

      then

       A12: (p2,q2) _|_ (a,b) by A6, A10, Def7;

       LIN (p2,q2,d) by A4, A9, Def10;

      then

       A13: LIN (p29,q29,d9) by Th40;

       LIN (p2,q2,c) by A3, A9, Def10;

      then LIN (p29,q29,c9) by Th40;

      then (p29,q29) // (c9,d9) by A13, AFF_1: 10;

      then (p2,q2) // (c,d) by Th36;

      hence thesis by A7, A12, Def7;

    end;

    theorem :: ANALMETR:57

    p in M & p in N & a in M & b in N & a <> b & a in K & b in K & A _|_ M & A _|_ N & K is being_line implies A _|_ K

    proof

      assume that

       A1: p in M & p in N & a in M & b in N and

       A2: a <> b and

       A3: a in K & b in K and

       A4: A _|_ M and

       A5: A _|_ N and

       A6: K is being_line;

      A is being_line by A4;

      then

      consider q, r such that

       A7: q <> r and

       A8: A = ( Line (q,r));

      reconsider q9 = q, r9 = r as Element of the AffinStruct of POS;

      ( Line (q,r)) = ( Line (q9,r9)) by Th41;

      then q in A & r in A by A8, AFF_1: 15;

      then (q,r) _|_ (p,a) & (q,r) _|_ (p,b) by A1, A4, A5, Th56;

      then

       A9: (q,r) _|_ (a,b) by Def7;

      K = ( Line (a,b)) by A2, A3, A6, Th54;

      hence thesis by A2, A7, A8, A9, Th45;

    end;

    theorem :: ANALMETR:58

    

     Th58: (b,c) _|_ (a,a) & (a,a) _|_ (b,c) & (b,c) // (a,a) & (a,a) // (b,c)

    proof

      reconsider a9 = a, b9 = b, c9 = c as Element of the AffinStruct of POS;

      thus (b,c) _|_ (a,a) by Def7;

      hence (a,a) _|_ (b,c) by Def7;

      (b9,c9) // (a9,a9) & (a9,a9) // (b9,c9) by AFF_1: 3;

      hence thesis by Th36;

    end;

    theorem :: ANALMETR:59

    

     Th59: (a,b) // (c,d) implies (a,b) // (d,c) & (b,a) // (c,d) & (b,a) // (d,c) & (c,d) // (a,b) & (c,d) // (b,a) & (d,c) // (a,b) & (d,c) // (b,a)

    proof

      reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of the AffinStruct of POS;

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

      then

       A1: (a9,b9) // (c9,d9) by Th36;

      then

       A2: (b9,a9) // (d9,c9) & (c9,d9) // (a9,b9) by AFF_1: 4;

      

       A3: (d9,c9) // (b9,a9) by A1, AFF_1: 4;

      

       A4: (c9,d9) // (b9,a9) & (d9,c9) // (a9,b9) by A1, AFF_1: 4;

      (a9,b9) // (d9,c9) & (b9,a9) // (c9,d9) by A1, AFF_1: 4;

      hence thesis by A2, A4, A3, Th36;

    end;

    theorem :: ANALMETR:60

    p <> q & ((p,q) // (a,b) & (p,q) // (c,d) or (p,q) // (a,b) & (c,d) // (p,q) or (a,b) // (p,q) & (c,d) // (p,q) or (a,b) // (p,q) & (p,q) // (c,d)) implies (a,b) // (c,d)

    proof

      assume that

       A1: p <> q and

       A2: (p,q) // (a,b) & (p,q) // (c,d) or (p,q) // (a,b) & (c,d) // (p,q) or (a,b) // (p,q) & (c,d) // (p,q) or (a,b) // (p,q) & (p,q) // (c,d);

      reconsider p9 = p, q9 = q, a9 = a, b9 = b, c9 = c, d9 = d as Element of the AffinStruct of POS;

      (p9,q9) // (a9,b9) & (p9,q9) // (c9,d9) or (p9,q9) // (a9,b9) & (c9,d9) // (p9,q9) or (a9,b9) // (p9,q9) & (c9,d9) // (p9,q9) or (a9,b9) // (p9,q9) & (p9,q9) // (c9,d9) by A2, Th36;

      then (a9,b9) // (c9,d9) by A1, AFF_1: 5;

      hence thesis by Th36;

    end;

    theorem :: ANALMETR:61

    

     Th61: (a,b) _|_ (c,d) implies (a,b) _|_ (d,c) & (b,a) _|_ (c,d) & (b,a) _|_ (d,c) & (c,d) _|_ (a,b) & (c,d) _|_ (b,a) & (d,c) _|_ (a,b) & (d,c) _|_ (b,a)

    proof

      assume

       A1: (a,b) _|_ (c,d);

      then (a,b) _|_ (d,c) by Def7;

      then

       A2: (d,c) _|_ (a,b) by Def7;

      then (d,c) _|_ (b,a) by Def7;

      then (b,a) _|_ (d,c) by Def7;

      then (b,a) _|_ (c,d) by Def7;

      hence thesis by A1, A2, Def7;

    end;

    theorem :: ANALMETR:62

    

     Th62: p <> q & ((p,q) // (a,b) & (p,q) _|_ (c,d) or (p,q) // (c,d) & (p,q) _|_ (a,b) or (p,q) // (a,b) & (c,d) _|_ (p,q) or (p,q) // (c,d) & (a,b) _|_ (p,q) or (a,b) // (p,q) & (c,d) _|_ (p,q) or (c,d) // (p,q) & (a,b) _|_ (p,q) or (a,b) // (p,q) & (p,q) _|_ (c,d) or (c,d) // (p,q) & (p,q) _|_ (a,b)) implies (a,b) _|_ (c,d)

    proof

      assume that

       A1: p <> q and

       A2: (p,q) // (a,b) & (p,q) _|_ (c,d) or (p,q) // (c,d) & (p,q) _|_ (a,b) or (p,q) // (a,b) & (c,d) _|_ (p,q) or (p,q) // (c,d) & (a,b) _|_ (p,q) or (a,b) // (p,q) & (c,d) _|_ (p,q) or (c,d) // (p,q) & (a,b) _|_ (p,q) or (a,b) // (p,q) & (p,q) _|_ (c,d) or (c,d) // (p,q) & (p,q) _|_ (a,b);

       A3:

      now

        assume (p,q) // (a,b) & (p,q) _|_ (c,d) or (p,q) // (a,b) & (c,d) _|_ (p,q) or (a,b) // (p,q) & (c,d) _|_ (p,q) or (a,b) // (p,q) & (p,q) _|_ (c,d);

        then (p,q) // (a,b) & (p,q) _|_ (c,d) by Th59, Th61;

        then (c,d) _|_ (a,b) by A1, Def7;

        hence thesis by Th61;

      end;

      now

        assume (p,q) // (c,d) & (p,q) _|_ (a,b) or (p,q) // (c,d) & (a,b) _|_ (p,q) or (c,d) // (p,q) & (a,b) _|_ (p,q) or (c,d) // (p,q) & (p,q) _|_ (a,b);

        then (p,q) // (c,d) & (p,q) _|_ (a,b) by Th59, Th61;

        hence thesis by A1, Def7;

      end;

      hence thesis by A2, A3;

    end;

    reserve POS for OrtAfPl;

    reserve K,M,N for Subset of POS;

    reserve x,a,b,c,d,p,q for Element of POS;

    theorem :: ANALMETR:63

    

     Th63: p <> q & ((p,q) _|_ (a,b) & (p,q) _|_ (c,d) or (p,q) _|_ (a,b) & (c,d) _|_ (p,q) or (a,b) _|_ (p,q) & (c,d) _|_ (p,q) or (a,b) _|_ (p,q) & (p,q) _|_ (c,d)) implies (a,b) // (c,d)

    proof

      assume that

       A1: p <> q and

       A2: (p,q) _|_ (a,b) & (p,q) _|_ (c,d) or (p,q) _|_ (a,b) & (c,d) _|_ (p,q) or (a,b) _|_ (p,q) & (c,d) _|_ (p,q) or (a,b) _|_ (p,q) & (p,q) _|_ (c,d);

      (p,q) _|_ (a,b) & (p,q) _|_ (c,d) by A2, Th61;

      hence thesis by A1, Def8;

    end;

    theorem :: ANALMETR:64

    a in M & b in M & a <> b & M is being_line & c in N & d in N & c <> d & N is being_line & (a,b) // (c,d) implies M // N

    proof

      assume that

       A1: a in M & b in M and

       A2: a <> b and

       A3: M is being_line & c in N & d in N and

       A4: c <> d and

       A5: N is being_line and

       A6: (a,b) // (c,d);

      M = ( Line (a,b)) & N = ( Line (c,d)) by A1, A2, A3, A4, A5, Th54;

      hence thesis by A2, A4, A6;

    end;

    theorem :: ANALMETR:65

    M _|_ K & N _|_ K implies M // N

    proof

      assume that

       A1: M _|_ K and

       A2: N _|_ K;

      consider p1,q1,a,b be Element of POS such that

       A3: p1 <> q1 and

       A4: a <> b and

       A5: K = ( Line (p1,q1)) and

       A6: M = ( Line (a,b)) and

       A7: (p1,q1) _|_ (a,b) by A1, Th45;

      consider p2,q2,c,d be Element of POS such that

       A8: p2 <> q2 and

       A9: c <> d and

       A10: K = ( Line (p2,q2)) and

       A11: N = ( Line (c,d)) and

       A12: (p2,q2) _|_ (c,d) by A2, Th45;

      reconsider p19 = p1, p29 = p2, q19 = q1, q29 = q2 as Element of the AffinStruct of POS;

      

       A13: ( Line (p19,q19)) = ( Line (p2,q2)) by A5, A10, Th41

      .= ( Line (p29,q29)) by Th41;

      then q29 in ( Line (p19,q19)) by AFF_1: 15;

      then

       A14: LIN (p19,q19,q29) by AFF_1:def 2;

      p29 in ( Line (p19,q19)) by A13, AFF_1: 15;

      then LIN (p19,q19,p29) by AFF_1:def 2;

      then (p19,q19) // (p29,q29) by A14, AFF_1: 10;

      then (p1,q1) // (p2,q2) by Th36;

      then (a,b) _|_ (p2,q2) by A3, A7, Th62;

      then (a,b) // (c,d) by A8, A12, Th63;

      hence thesis by A4, A6, A9, A11;

    end;

    theorem :: ANALMETR:66

    

     Th66: M _|_ N implies ex p st p in M & p in N

    proof

      reconsider M9 = M, N9 = N as Subset of the AffinStruct of POS;

      assume

       A1: M _|_ N;

      then M is being_line;

      then

       A2: M9 is being_line by Th43;

      N is being_line by A1, Th44;

      then

       A3: N9 is being_line by Th43;

       not M // N by A1, Th52;

      then not M9 // N9 by Th46;

      hence thesis by A2, A3, AFF_1: 58;

    end;

    theorem :: ANALMETR:67

    

     Th67: (a,b) _|_ (c,d) implies ex p st LIN (a,b,p) & LIN (c,d,p)

    proof

      reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of the AffinStruct of POS;

      assume

       A1: (a,b) _|_ (c,d);

       A2:

      now

        set M = ( Line (a,b)), N = ( Line (c,d));

        assume a <> b & c <> d;

        then M _|_ N by A1, Th45;

        then

        consider p such that

         A3: p in M & p in N by Th66;

         LIN (a,b,p) & LIN (c,d,p) by A3, Def10;

        hence thesis;

      end;

       LIN (a9,b9,a9) by AFF_1: 7;

      then

       A4: LIN (a,b,a) by Th40;

       A5:

      now

        assume c = d;

        then (c,d) // (c,a) by Th58;

        then LIN (c,d,a);

        hence thesis by A4;

      end;

       LIN (c9,d9,c9) by AFF_1: 7;

      then

       A6: LIN (c,d,c) by Th40;

      now

        assume a = b;

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

        then LIN (a,b,c);

        hence thesis by A6;

      end;

      hence thesis by A5, A2;

    end;

    theorem :: ANALMETR:68

    (a,b) _|_ K implies ex p st LIN (a,b,p) & p in K

    proof

      assume (a,b) _|_ K;

      then

      consider p, q such that p <> q and

       A1: K = ( Line (p,q)) and

       A2: (a,b) _|_ (p,q);

      consider c such that

       A3: LIN (a,b,c) and

       A4: LIN (p,q,c) by A2, Th67;

      c in K by A1, A4, Def10;

      hence thesis by A3;

    end;

    theorem :: ANALMETR:69

    

     Th69: ex x st (a,x) _|_ (p,q) & LIN (p,q,x)

    proof

       A1:

      now

        assume p <> q;

        then

        consider x such that

         A2: (p,q) // (p,x) & (p,q) _|_ (x,a) by Def7;

        take x;

        thus (a,x) _|_ (p,q) & LIN (p,q,x) by A2, Th61;

      end;

      now

        assume

         A3: p = q;

        take x = a;

        (p,q) // (p,a) by A3, Th58;

        hence (a,x) _|_ (p,q) & LIN (p,q,x) by Th58;

      end;

      hence thesis by A1;

    end;

    theorem :: ANALMETR:70

    K is being_line implies ex x st (a,x) _|_ K & x in K

    proof

      assume K is being_line;

      then

      consider p, q such that

       A1: p <> q and

       A2: K = ( Line (p,q));

      consider x such that

       A3: (a,x) _|_ (p,q) and

       A4: LIN (p,q,x) by Th69;

      take x;

      thus (a,x) _|_ K by A1, A2, A3;

      thus thesis by A2, A4, Def10;

    end;