analort.miz



    begin

    reserve V for RealLinearSpace,

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

a,a1,a2,b,b1,b2,c1,c2,n,k1,k2 for Real;

    

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

    proof

      assume that

       A1: v1 = ((b1 * x) + (b2 * y)) and

       A2: v2 = ((c1 * x) + (c2 * y));

      

      thus (v1 + v2) = ((((b1 * x) + (b2 * y)) + (c1 * x)) + (c2 * y)) by A1, A2, RLVECT_1:def 3

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

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

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

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

      

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

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

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

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

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

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

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

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

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

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

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

    end;

    

     Lm2: v = ((b1 * x) + (b2 * y)) implies (a * v) = (((a * b1) * x) + ((a * b2) * y))

    proof

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

      

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

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

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

    end;

    

     Lm3: Gen (x,y) & ((a1 * x) + (a2 * y)) = ((b1 * x) + (b2 * y)) implies a1 = b1 & a2 = b2

    proof

      assume that

       A1: Gen (x,y) and

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

      

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

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

      then

       A4: (( - b1) + a1) = 0 by A1, ANALMETR:def 1;

      (( - b2) + a2) = 0 by A1, A3, ANALMETR:def 1;

      hence thesis by A4;

    end;

    

     Lm4: Gen (x,y) implies x <> ( 0. V) & y <> ( 0. V)

    proof

      assume

       A1: Gen (x,y);

      

       A2: x <> ( 0. V)

      proof

        assume

         A3: x = ( 0. V);

        consider a, b such that

         A4: a = 1 and

         A5: b = 0 ;

        ((a * x) + (b * y)) = (( 0. V) + ( 0 * y)) by A3, A5, RLVECT_1: 10

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

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

        hence contradiction by A1, A4, ANALMETR:def 1;

      end;

      y <> ( 0. V)

      proof

        assume

         A6: y = ( 0. V);

        consider a, b such that

         A7: a = 0 and

         A8: b = 1;

        ((a * x) + (b * y)) = (( 0. V) + (1 * ( 0. V))) by A6, A7, A8, RLVECT_1: 10

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

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

        hence thesis by A1, A8, ANALMETR:def 1;

      end;

      hence thesis by A2;

    end;

    

     Lm5: Gen (x,y) implies u = ((( pr1 (x,y,u)) * x) + (( pr2 (x,y,u)) * y))

    proof

      assume

       A1: Gen (x,y);

      then

      consider b such that

       A2: u = ((( pr1 (x,y,u)) * x) + (b * y)) by GEOMTRAP:def 4;

      thus thesis by A1, GEOMTRAP:def 5, A2;

    end;

    

     Lm6: Gen (x,y) & u = ((k1 * x) + (k2 * y)) implies k1 = ( pr1 (x,y,u)) & k2 = ( pr2 (x,y,u))

    proof

      assume that

       A1: Gen (x,y) and

       A2: u = ((k1 * x) + (k2 * y));

      u = ((( pr1 (x,y,u)) * x) + (( pr2 (x,y,u)) * y)) by A1, Lm5;

      hence thesis by A1, A2, Lm3;

    end;

    

     Lm7: Gen (x,y) implies ( pr1 (x,y,(u + v))) = (( pr1 (x,y,u)) + ( pr1 (x,y,v))) & ( pr2 (x,y,(u + v))) = (( pr2 (x,y,u)) + ( pr2 (x,y,v))) & ( pr1 (x,y,(u - v))) = (( pr1 (x,y,u)) - ( pr1 (x,y,v))) & ( pr2 (x,y,(u - v))) = (( pr2 (x,y,u)) - ( pr2 (x,y,v))) & ( pr1 (x,y,(a * u))) = (a * ( pr1 (x,y,u))) & ( pr2 (x,y,(a * u))) = (a * ( pr2 (x,y,u)))

    proof

      assume

       A1: Gen (x,y);

      set p1u = ( pr1 (x,y,u)), p2u = ( pr2 (x,y,u)), p1v = ( pr1 (x,y,v)), p2v = ( pr2 (x,y,v));

      

       A2: u = ((p1u * x) + (p2u * y)) by A1, Lm5;

      

       A3: v = ((p1v * x) + (p2v * y)) by A1, Lm5;

      

      then (u + v) = ((((p1u * x) + (p2u * y)) + (p1v * x)) + (p2v * y)) by A2, RLVECT_1:def 3

      .= ((((p1u * x) + (p1v * x)) + (p2u * y)) + (p2v * y)) by RLVECT_1:def 3

      .= (((p1u * x) + (p1v * x)) + ((p2u * y) + (p2v * y))) by RLVECT_1:def 3

      .= (((p1u + p1v) * x) + ((p2u * y) + (p2v * y))) by RLVECT_1:def 6

      .= (((p1u + p1v) * x) + ((p2u + p2v) * y)) by RLVECT_1:def 6;

      hence ( pr1 (x,y,(u + v))) = (p1u + p1v) & ( pr2 (x,y,(u + v))) = (p2u + p2v) by A1, Lm6;

      (u - v) = (((p1u - p1v) * x) + ((p2u - p2v) * y)) by A2, A3, Lm1;

      hence ( pr1 (x,y,(u - v))) = (p1u - p1v) & ( pr2 (x,y,(u - v))) = (p2u - p2v) by A1, Lm6;

      (a * u) = (((a * p1u) * x) + ((a * p2u) * y)) by A2, Lm2;

      hence thesis by A1, Lm6;

    end;

    definition

      let V, x, y;

      let u;

      :: ANALORT:def1

      func Ortm (x,y,u) -> VECTOR of V equals ((( pr1 (x,y,u)) * x) + (( - ( pr2 (x,y,u))) * y));

      correctness ;

    end

    theorem :: ANALORT:1

    

     Th1: Gen (x,y) implies ( Ortm (x,y,(u + v))) = (( Ortm (x,y,u)) + ( Ortm (x,y,v)))

    proof

      assume

       A1: Gen (x,y);

      

      hence ( Ortm (x,y,(u + v))) = (((( pr1 (x,y,u)) + ( pr1 (x,y,v))) * x) + (( - ( pr2 (x,y,(u + v)))) * y)) by Lm7

      .= (((( pr1 (x,y,u)) + ( pr1 (x,y,v))) * x) + (( - (( pr2 (x,y,u)) + ( pr2 (x,y,v)))) * y)) by A1, Lm7

      .= (((( pr1 (x,y,u)) * x) + (( pr1 (x,y,v)) * x)) + (( - (( pr2 (x,y,u)) + ( pr2 (x,y,v)))) * y)) by RLVECT_1:def 6

      .= (((( pr1 (x,y,u)) * x) + (( pr1 (x,y,v)) * x)) + ((( pr2 (x,y,u)) + ( pr2 (x,y,v))) * ( - y))) by RLVECT_1: 24

      .= (((( pr1 (x,y,u)) * x) + (( pr1 (x,y,v)) * x)) + ( - ((( pr2 (x,y,u)) + ( pr2 (x,y,v))) * y))) by RLVECT_1: 25

      .= (((( pr1 (x,y,u)) * x) + (( pr1 (x,y,v)) * x)) + ( - ((( pr2 (x,y,u)) * y) + (( pr2 (x,y,v)) * y)))) by RLVECT_1:def 6

      .= (((( pr1 (x,y,u)) * x) + (( pr1 (x,y,v)) * x)) + (( - (( pr2 (x,y,u)) * y)) + ( - (( pr2 (x,y,v)) * y)))) by RLVECT_1: 31

      .= ((( pr1 (x,y,u)) * x) + ((( pr1 (x,y,v)) * x) + (( - (( pr2 (x,y,u)) * y)) + ( - (( pr2 (x,y,v)) * y))))) by RLVECT_1:def 3

      .= ((( pr1 (x,y,u)) * x) + (( - (( pr2 (x,y,u)) * y)) + ((( pr1 (x,y,v)) * x) + ( - (( pr2 (x,y,v)) * y))))) by RLVECT_1:def 3

      .= (((( pr1 (x,y,u)) * x) + ( - (( pr2 (x,y,u)) * y))) + ((( pr1 (x,y,v)) * x) + ( - (( pr2 (x,y,v)) * y)))) by RLVECT_1:def 3

      .= (((( pr1 (x,y,u)) * x) + (( pr2 (x,y,u)) * ( - y))) + ((( pr1 (x,y,v)) * x) + ( - (( pr2 (x,y,v)) * y)))) by RLVECT_1: 25

      .= (((( pr1 (x,y,u)) * x) + (( pr2 (x,y,u)) * ( - y))) + ((( pr1 (x,y,v)) * x) + (( pr2 (x,y,v)) * ( - y)))) by RLVECT_1: 25

      .= (((( pr1 (x,y,u)) * x) + (( - ( pr2 (x,y,u))) * y)) + ((( pr1 (x,y,v)) * x) + (( pr2 (x,y,v)) * ( - y)))) by RLVECT_1: 24

      .= (( Ortm (x,y,u)) + ( Ortm (x,y,v))) by RLVECT_1: 24;

    end;

    theorem :: ANALORT:2

    

     Th2: Gen (x,y) implies ( Ortm (x,y,(n * u))) = (n * ( Ortm (x,y,u)))

    proof

      assume

       A1: Gen (x,y);

      

      hence ( Ortm (x,y,(n * u))) = (((n * ( pr1 (x,y,u))) * x) + (( - ( pr2 (x,y,(n * u)))) * y)) by Lm7

      .= (((n * ( pr1 (x,y,u))) * x) + (( - (n * ( pr2 (x,y,u)))) * y)) by A1, Lm7

      .= (((n * ( pr1 (x,y,u))) * x) + ((n * ( pr2 (x,y,u))) * ( - y))) by RLVECT_1: 24

      .= (((n * ( pr1 (x,y,u))) * x) + ( - ((n * ( pr2 (x,y,u))) * y))) by RLVECT_1: 25

      .= (((n * ( pr1 (x,y,u))) * x) + ( - (n * (( pr2 (x,y,u)) * y)))) by RLVECT_1:def 7

      .= (((n * ( pr1 (x,y,u))) * x) + (n * ( - (( pr2 (x,y,u)) * y)))) by RLVECT_1: 25

      .= ((n * (( pr1 (x,y,u)) * x)) + (n * ( - (( pr2 (x,y,u)) * y)))) by RLVECT_1:def 7

      .= (n * ((( pr1 (x,y,u)) * x) + ( - (( pr2 (x,y,u)) * y)))) by RLVECT_1:def 5

      .= (n * ((( pr1 (x,y,u)) * x) + (( pr2 (x,y,u)) * ( - y)))) by RLVECT_1: 25

      .= (n * ( Ortm (x,y,u))) by RLVECT_1: 24;

    end;

    theorem :: ANALORT:3

     Gen (x,y) implies ( Ortm (x,y,( 0. V))) = ( 0. V)

    proof

      assume

       A1: Gen (x,y);

      set u = the VECTOR of V;

      

      thus ( Ortm (x,y,( 0. V))) = ( Ortm (x,y,( 0 * u))) by RLVECT_1: 10

      .= ( 0 * ( Ortm (x,y,u))) by A1, Th2

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

    end;

    theorem :: ANALORT:4

    

     Th4: Gen (x,y) implies ( Ortm (x,y,( - u))) = ( - ( Ortm (x,y,u)))

    proof

      assume

       A1: Gen (x,y);

      

      then

       A2: ( - u) = ( - ((( pr1 (x,y,u)) * x) + (( pr2 (x,y,u)) * y))) by Lm5

      .= (( - (( pr1 (x,y,u)) * x)) + ( - (( pr2 (x,y,u)) * y))) by RLVECT_1: 31

      .= ((( pr1 (x,y,u)) * ( - x)) + ( - (( pr2 (x,y,u)) * y))) by RLVECT_1: 25

      .= ((( - ( pr1 (x,y,u))) * x) + ( - (( pr2 (x,y,u)) * y))) by RLVECT_1: 24

      .= ((( - ( pr1 (x,y,u))) * x) + (( pr2 (x,y,u)) * ( - y))) by RLVECT_1: 25

      .= ((( - ( pr1 (x,y,u))) * x) + (( - ( pr2 (x,y,u))) * y)) by RLVECT_1: 24;

      

      hence ( Ortm (x,y,( - u))) = ((( - ( pr1 (x,y,u))) * x) + (( - ( pr2 (x,y,( - u)))) * y)) by A1, Lm6

      .= ((( - ( pr1 (x,y,u))) * x) + (( - ( - ( pr2 (x,y,u)))) * y)) by A1, A2, Lm6

      .= ((( pr1 (x,y,u)) * ( - x)) + (( - ( - ( pr2 (x,y,u)))) * y)) by RLVECT_1: 24

      .= (( - (( pr1 (x,y,u)) * x)) + (( - ( - ( pr2 (x,y,u)))) * y)) by RLVECT_1: 25

      .= (( - (( pr1 (x,y,u)) * x)) + (( - ( pr2 (x,y,u))) * ( - y))) by RLVECT_1: 24

      .= (( - (( pr1 (x,y,u)) * x)) + ( - (( - ( pr2 (x,y,u))) * y))) by RLVECT_1: 25

      .= ( - ( Ortm (x,y,u))) by RLVECT_1: 31;

    end;

    theorem :: ANALORT:5

    

     Th5: Gen (x,y) implies ( Ortm (x,y,(u - v))) = (( Ortm (x,y,u)) - ( Ortm (x,y,v)))

    proof

      assume

       A1: Gen (x,y);

      

      hence ( Ortm (x,y,(u - v))) = (( Ortm (x,y,u)) + ( Ortm (x,y,( - v)))) by Th1

      .= (( Ortm (x,y,u)) - ( Ortm (x,y,v))) by A1, Th4;

    end;

    theorem :: ANALORT:6

    

     Th6: Gen (x,y) & ( Ortm (x,y,u)) = ( Ortm (x,y,v)) implies u = v

    proof

      assume that

       A1: Gen (x,y) and

       A2: ( Ortm (x,y,u)) = ( Ortm (x,y,v));

      (((( pr1 (x,y,u)) * x) + (( - ( pr2 (x,y,u))) * y)) - ((( pr1 (x,y,v)) * x) + (( - ( pr2 (x,y,v))) * y))) = ( 0. V) by A2, RLVECT_1: 15;

      then ((((( pr1 (x,y,u)) * x) + (( - ( pr2 (x,y,u))) * y)) - (( pr1 (x,y,v)) * x)) - (( - ( pr2 (x,y,v))) * y)) = ( 0. V) by RLVECT_1: 27;

      then ((((( pr1 (x,y,u)) * x) + ( - (( pr1 (x,y,v)) * x))) + (( - ( pr2 (x,y,u))) * y)) - (( - ( pr2 (x,y,v))) * y)) = ( 0. V) by RLVECT_1:def 3;

      then (((( pr1 (x,y,u)) * x) - (( pr1 (x,y,v)) * x)) + ((( - ( pr2 (x,y,u))) * y) - (( - ( pr2 (x,y,v))) * y))) = ( 0. V) by RLVECT_1:def 3;

      then (((( pr1 (x,y,u)) - ( pr1 (x,y,v))) * x) + ((( - ( pr2 (x,y,u))) * y) - (( - ( pr2 (x,y,v))) * y))) = ( 0. V) by RLVECT_1: 35;

      then

       A3: (((( pr1 (x,y,u)) - ( pr1 (x,y,v))) * x) + ((( - ( pr2 (x,y,u))) - ( - ( pr2 (x,y,v)))) * y)) = ( 0. V) by RLVECT_1: 35;

      then

       A4: (( pr1 (x,y,u)) - ( pr1 (x,y,v))) = 0 by A1, ANALMETR:def 1;

      (( - ( pr2 (x,y,u))) - ( - ( pr2 (x,y,v)))) = 0 by A1, A3, ANALMETR:def 1;

      

      hence u = ((( pr1 (x,y,v)) * x) + (( pr2 (x,y,v)) * y)) by A1, A4, Lm5

      .= v by A1, Lm5;

    end;

    theorem :: ANALORT:7

    

     Th7: Gen (x,y) implies ( Ortm (x,y,( Ortm (x,y,u)))) = u

    proof

      assume

       A1: Gen (x,y);

      

      hence ( Ortm (x,y,( Ortm (x,y,u)))) = ((( pr1 (x,y,u)) * x) + (( - ( pr2 (x,y,((( pr1 (x,y,u)) * x) + (( - ( pr2 (x,y,u))) * y))))) * y)) by GEOMTRAP:def 4

      .= ((( pr1 (x,y,u)) * x) + (( - ( - ( pr2 (x,y,u)))) * y)) by A1, GEOMTRAP:def 5

      .= u by A1, Lm5;

    end;

    theorem :: ANALORT:8

    

     Th8: Gen (x,y) implies ex v st u = ( Ortm (x,y,v))

    proof

      assume

       A1: Gen (x,y);

      take ( Ortm (x,y,u));

      thus thesis by A1, Th7;

    end;

    definition

      let V, x, y;

      let u;

      :: ANALORT:def2

      func Orte (x,y,u) -> VECTOR of V equals ((( pr2 (x,y,u)) * x) + (( - ( pr1 (x,y,u))) * y));

      correctness ;

    end

    theorem :: ANALORT:9

    

     Th9: Gen (x,y) implies ( Orte (x,y,( - v))) = ( - ( Orte (x,y,v)))

    proof

      assume

       A1: Gen (x,y);

      

      then

       A2: ( - v) = ( - ((( pr1 (x,y,v)) * x) + (( pr2 (x,y,v)) * y))) by Lm5

      .= (( - (( pr1 (x,y,v)) * x)) + ( - (( pr2 (x,y,v)) * y))) by RLVECT_1: 31

      .= ((( pr1 (x,y,v)) * ( - x)) + ( - (( pr2 (x,y,v)) * y))) by RLVECT_1: 25

      .= ((( - ( pr1 (x,y,v))) * x) + ( - (( pr2 (x,y,v)) * y))) by RLVECT_1: 24

      .= ((( - ( pr1 (x,y,v))) * x) + (( pr2 (x,y,v)) * ( - y))) by RLVECT_1: 25

      .= ((( - ( pr1 (x,y,v))) * x) + (( - ( pr2 (x,y,v))) * y)) by RLVECT_1: 24;

      

      hence ( Orte (x,y,( - v))) = ((( - ( pr2 (x,y,v))) * x) + (( - ( pr1 (x,y,( - v)))) * y)) by A1, Lm6

      .= ((( - ( pr2 (x,y,v))) * x) + (( - ( - ( pr1 (x,y,v)))) * y)) by A1, A2, Lm6

      .= ((( pr2 (x,y,v)) * ( - x)) + (( - ( - ( pr1 (x,y,v)))) * y)) by RLVECT_1: 24

      .= (( - (( pr2 (x,y,v)) * x)) + (( - ( - ( pr1 (x,y,v)))) * y)) by RLVECT_1: 25

      .= (( - (( pr2 (x,y,v)) * x)) + (( - ( pr1 (x,y,v))) * ( - y))) by RLVECT_1: 24

      .= (( - (( pr2 (x,y,v)) * x)) + ( - (( - ( pr1 (x,y,v))) * y))) by RLVECT_1: 25

      .= ( - ( Orte (x,y,v))) by RLVECT_1: 31;

    end;

    theorem :: ANALORT:10

    

     Th10: Gen (x,y) implies ( Orte (x,y,(u + v))) = (( Orte (x,y,u)) + ( Orte (x,y,v)))

    proof

      assume

       A1: Gen (x,y);

      

      hence ( Orte (x,y,(u + v))) = ((( pr2 (x,y,(u + v))) * x) + (( - (( pr1 (x,y,u)) + ( pr1 (x,y,v)))) * y)) by Lm7

      .= (((( pr2 (x,y,u)) + ( pr2 (x,y,v))) * x) + (( - (( pr1 (x,y,u)) + ( pr1 (x,y,v)))) * y)) by A1, Lm7

      .= (((( pr2 (x,y,u)) * x) + (( pr2 (x,y,v)) * x)) + (( - (( pr1 (x,y,u)) + ( pr1 (x,y,v)))) * y)) by RLVECT_1:def 6

      .= (((( pr2 (x,y,u)) * x) + (( pr2 (x,y,v)) * x)) + ((( pr1 (x,y,u)) + ( pr1 (x,y,v))) * ( - y))) by RLVECT_1: 24

      .= (((( pr2 (x,y,u)) * x) + (( pr2 (x,y,v)) * x)) + ( - ((( pr1 (x,y,u)) + ( pr1 (x,y,v))) * y))) by RLVECT_1: 25

      .= (((( pr2 (x,y,u)) * x) + (( pr2 (x,y,v)) * x)) + ( - ((( pr1 (x,y,u)) * y) + (( pr1 (x,y,v)) * y)))) by RLVECT_1:def 6

      .= (((( pr2 (x,y,u)) * x) + (( pr2 (x,y,v)) * x)) + (( - (( pr1 (x,y,u)) * y)) + ( - (( pr1 (x,y,v)) * y)))) by RLVECT_1: 31

      .= ((( pr2 (x,y,u)) * x) + ((( pr2 (x,y,v)) * x) + (( - (( pr1 (x,y,u)) * y)) + ( - (( pr1 (x,y,v)) * y))))) by RLVECT_1:def 3

      .= ((( pr2 (x,y,u)) * x) + (( - (( pr1 (x,y,u)) * y)) + ((( pr2 (x,y,v)) * x) + ( - (( pr1 (x,y,v)) * y))))) by RLVECT_1:def 3

      .= (((( pr2 (x,y,u)) * x) + ( - (( pr1 (x,y,u)) * y))) + ((( pr2 (x,y,v)) * x) + ( - (( pr1 (x,y,v)) * y)))) by RLVECT_1:def 3

      .= (((( pr2 (x,y,u)) * x) + (( pr1 (x,y,u)) * ( - y))) + ((( pr2 (x,y,v)) * x) + ( - (( pr1 (x,y,v)) * y)))) by RLVECT_1: 25

      .= (((( pr2 (x,y,u)) * x) + (( pr1 (x,y,u)) * ( - y))) + ((( pr2 (x,y,v)) * x) + (( pr1 (x,y,v)) * ( - y)))) by RLVECT_1: 25

      .= (((( pr2 (x,y,u)) * x) + (( - ( pr1 (x,y,u))) * y)) + ((( pr2 (x,y,v)) * x) + (( pr1 (x,y,v)) * ( - y)))) by RLVECT_1: 24

      .= (( Orte (x,y,u)) + ( Orte (x,y,v))) by RLVECT_1: 24;

    end;

    theorem :: ANALORT:11

    

     Th11: Gen (x,y) implies ( Orte (x,y,(u - v))) = (( Orte (x,y,u)) - ( Orte (x,y,v)))

    proof

      assume

       A1: Gen (x,y);

      

      hence ( Orte (x,y,(u - v))) = (( Orte (x,y,u)) + ( Orte (x,y,( - v)))) by Th10

      .= (( Orte (x,y,u)) - ( Orte (x,y,v))) by A1, Th9;

    end;

    theorem :: ANALORT:12

    

     Th12: Gen (x,y) implies ( Orte (x,y,(n * u))) = (n * ( Orte (x,y,u)))

    proof

      assume

       A1: Gen (x,y);

      

      hence ( Orte (x,y,(n * u))) = (((n * ( pr2 (x,y,u))) * x) + (( - ( pr1 (x,y,(n * u)))) * y)) by Lm7

      .= (((n * ( pr2 (x,y,u))) * x) + (( - (n * ( pr1 (x,y,u)))) * y)) by A1, Lm7

      .= (((n * ( pr2 (x,y,u))) * x) + ((n * ( pr1 (x,y,u))) * ( - y))) by RLVECT_1: 24

      .= (((n * ( pr2 (x,y,u))) * x) + ( - ((n * ( pr1 (x,y,u))) * y))) by RLVECT_1: 25

      .= (((n * ( pr2 (x,y,u))) * x) + ( - (n * (( pr1 (x,y,u)) * y)))) by RLVECT_1:def 7

      .= (((n * ( pr2 (x,y,u))) * x) + (n * ( - (( pr1 (x,y,u)) * y)))) by RLVECT_1: 25

      .= ((n * (( pr2 (x,y,u)) * x)) + (n * ( - (( pr1 (x,y,u)) * y)))) by RLVECT_1:def 7

      .= (n * ((( pr2 (x,y,u)) * x) + ( - (( pr1 (x,y,u)) * y)))) by RLVECT_1:def 5

      .= (n * ((( pr2 (x,y,u)) * x) + (( pr1 (x,y,u)) * ( - y)))) by RLVECT_1: 25

      .= (n * ( Orte (x,y,u))) by RLVECT_1: 24;

    end;

    theorem :: ANALORT:13

    

     Th13: Gen (x,y) & ( Orte (x,y,u)) = ( Orte (x,y,v)) implies u = v

    proof

      assume that

       A1: Gen (x,y) and

       A2: ( Orte (x,y,u)) = ( Orte (x,y,v));

      (((( pr2 (x,y,u)) * x) + (( - ( pr1 (x,y,u))) * y)) - ((( pr2 (x,y,v)) * x) + (( - ( pr1 (x,y,v))) * y))) = ( 0. V) by A2, RLVECT_1: 15;

      then ((((( pr2 (x,y,u)) * x) + (( - ( pr1 (x,y,u))) * y)) - (( pr2 (x,y,v)) * x)) - (( - ( pr1 (x,y,v))) * y)) = ( 0. V) by RLVECT_1: 27;

      then ((((( pr2 (x,y,u)) * x) + ( - (( pr2 (x,y,v)) * x))) + (( - ( pr1 (x,y,u))) * y)) - (( - ( pr1 (x,y,v))) * y)) = ( 0. V) by RLVECT_1:def 3;

      then (((( pr2 (x,y,u)) * x) - (( pr2 (x,y,v)) * x)) + ((( - ( pr1 (x,y,u))) * y) - (( - ( pr1 (x,y,v))) * y))) = ( 0. V) by RLVECT_1:def 3;

      then (((( pr2 (x,y,u)) - ( pr2 (x,y,v))) * x) + ((( - ( pr1 (x,y,u))) * y) - (( - ( pr1 (x,y,v))) * y))) = ( 0. V) by RLVECT_1: 35;

      then

       A3: (((( pr2 (x,y,u)) - ( pr2 (x,y,v))) * x) + ((( - ( pr1 (x,y,u))) - ( - ( pr1 (x,y,v)))) * y)) = ( 0. V) by RLVECT_1: 35;

      then

       A4: (( pr2 (x,y,u)) - ( pr2 (x,y,v))) = 0 by A1, ANALMETR:def 1;

      (( - ( pr1 (x,y,u))) - ( - ( pr1 (x,y,v)))) = 0 by A1, A3, ANALMETR:def 1;

      

      hence u = ((( pr1 (x,y,v)) * x) + (( pr2 (x,y,v)) * y)) by A1, A4, Lm5

      .= v by A1, Lm5;

    end;

    theorem :: ANALORT:14

    

     Th14: Gen (x,y) implies ( Orte (x,y,( Orte (x,y,u)))) = ( - u)

    proof

      assume

       A1: Gen (x,y);

      

      hence ( Orte (x,y,( Orte (x,y,u)))) = ((( - ( pr1 (x,y,u))) * x) + (( - ( pr1 (x,y,((( pr2 (x,y,u)) * x) + (( - ( pr1 (x,y,u))) * y))))) * y)) by GEOMTRAP:def 5

      .= ((( - ( pr1 (x,y,u))) * x) + (( - ( pr2 (x,y,u))) * y)) by A1, GEOMTRAP:def 4

      .= ((( pr1 (x,y,u)) * ( - x)) + (( - ( pr2 (x,y,u))) * y)) by RLVECT_1: 24

      .= (( - (( pr1 (x,y,u)) * x)) + (( - ( pr2 (x,y,u))) * y)) by RLVECT_1: 25

      .= (( - (( pr1 (x,y,u)) * x)) + (( pr2 (x,y,u)) * ( - y))) by RLVECT_1: 24

      .= (( - (( pr1 (x,y,u)) * x)) + ( - (( pr2 (x,y,u)) * y))) by RLVECT_1: 25

      .= ( - ((( pr1 (x,y,u)) * x) + (( pr2 (x,y,u)) * y))) by RLVECT_1: 31

      .= ( - u) by A1, Lm5;

    end;

    theorem :: ANALORT:15

    

     Th15: Gen (x,y) implies ex v st ( Orte (x,y,v)) = u

    proof

      assume

       A1: Gen (x,y);

      take v = ( - ( Orte (x,y,u)));

      

      thus ( Orte (x,y,v)) = ( - ( Orte (x,y,( Orte (x,y,u))))) by A1, Th9

      .= ( - ( - u)) by A1, Th14

      .= u by RLVECT_1: 17;

    end;

    definition

      let V;

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

      :: ANALORT:def3

      pred u,v,u1,v1 are_COrte_wrt x,y means (( Orte (x,y,u)),( Orte (x,y,v))) // (u1,v1);

      :: ANALORT:def4

      pred u,v,u1,v1 are_COrtm_wrt x,y means (( Ortm (x,y,u)),( Ortm (x,y,v))) // (u1,v1);

    end

    theorem :: ANALORT:16

    

     Th16: Gen (x,y) implies ((u,v) // (u1,v1) implies (( Orte (x,y,u)),( Orte (x,y,v))) // (( Orte (x,y,u1)),( Orte (x,y,v1))))

    proof

      assume

       A1: Gen (x,y);

      assume

       A2: (u,v) // (u1,v1);

      now

        assume that

         A3: u <> v and

         A4: u1 <> v1;

        consider a, b such that

         A5: 0 < a and

         A6: 0 < b and

         A7: (a * (v - u)) = (b * (v1 - u1)) by A2, A3, A4, ANALOAF:def 1;

        (a * (( Orte (x,y,v)) - ( Orte (x,y,u)))) = (a * ( Orte (x,y,(v - u)))) by A1, Th11

        .= ( Orte (x,y,(b * (v1 - u1)))) by A1, A7, Th12

        .= (b * ( Orte (x,y,(v1 - u1)))) by A1, Th12

        .= (b * (( Orte (x,y,v1)) - ( Orte (x,y,u1)))) by A1, Th11;

        hence thesis by A5, A6, ANALOAF:def 1;

      end;

      hence thesis by ANALOAF: 9;

    end;

    theorem :: ANALORT:17

    

     Th17: Gen (x,y) implies ((u,v) // (u1,v1) implies (( Ortm (x,y,u)),( Ortm (x,y,v))) // (( Ortm (x,y,u1)),( Ortm (x,y,v1))))

    proof

      assume

       A1: Gen (x,y);

      assume

       A2: (u,v) // (u1,v1);

      now

        assume

         A3: u <> v;

        now

          assume u1 <> v1;

          then

          consider a, b such that

           A4: 0 < a and

           A5: 0 < b and

           A6: (a * (v - u)) = (b * (v1 - u1)) by A2, A3, ANALOAF:def 1;

          (a * (( Ortm (x,y,v)) - ( Ortm (x,y,u)))) = (a * ( Ortm (x,y,(v - u)))) by A1, Th5

          .= ( Ortm (x,y,(b * (v1 - u1)))) by A1, A6, Th2

          .= (b * ( Ortm (x,y,(v1 - u1)))) by A1, Th2

          .= (b * (( Ortm (x,y,v1)) - ( Ortm (x,y,u1)))) by A1, Th5;

          hence thesis by A4, A5, ANALOAF:def 1;

        end;

        hence thesis by ANALOAF: 9;

      end;

      hence thesis by ANALOAF: 9;

    end;

    theorem :: ANALORT:18

    

     Th18: Gen (x,y) implies ((u,u1,v,v1) are_COrte_wrt (x,y) implies (v,v1,u1,u) are_COrte_wrt (x,y))

    proof

      assume

       A1: Gen (x,y);

      assume (u,u1,v,v1) are_COrte_wrt (x,y);

      then (( Orte (x,y,u)),( Orte (x,y,u1))) // (v,v1);

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

      then (( Orte (x,y,v)),( Orte (x,y,v1))) // (( Orte (x,y,( Orte (x,y,u)))),( Orte (x,y,( Orte (x,y,u1))))) by A1, Th16;

      then (( Orte (x,y,v)),( Orte (x,y,v1))) // (( - u),( Orte (x,y,( Orte (x,y,u1))))) by A1, Th14;

      then (( Orte (x,y,v)),( Orte (x,y,v1))) // (( - u),( - u1)) by A1, Th14;

      then

       A2: (( - u),( - u1)) // (( Orte (x,y,v)),( Orte (x,y,v1))) by ANALOAF: 12;

      (( - u1) - ( - u)) = (u + ( - u1)) by RLVECT_1: 17

      .= (u - u1);

      then

       A3: (( - u),( - u1)) // (u1,u) by ANALOAF: 15;

      

       A4: ( - u) <> ( - u1) implies thesis by A2, A3, ANALOAF: 11;

      now

        assume ( - u) = ( - u1);

        

        then u = ( - ( - u1)) by RLVECT_1: 17

        .= u1 by RLVECT_1: 17;

        then (( Orte (x,y,v)),( Orte (x,y,v1))) // (u1,u) by ANALOAF: 9;

        hence thesis;

      end;

      hence thesis by A4;

    end;

    theorem :: ANALORT:19

    

     Th19: Gen (x,y) implies ((u,u1,v,v1) are_COrtm_wrt (x,y) implies (v,v1,u,u1) are_COrtm_wrt (x,y))

    proof

      assume

       A1: Gen (x,y);

      assume (u,u1,v,v1) are_COrtm_wrt (x,y);

      then (( Ortm (x,y,u)),( Ortm (x,y,u1))) // (v,v1);

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

      then (( Ortm (x,y,v)),( Ortm (x,y,v1))) // (( Ortm (x,y,( Ortm (x,y,u)))),( Ortm (x,y,( Ortm (x,y,u1))))) by A1, Th17;

      then (( Ortm (x,y,v)),( Ortm (x,y,v1))) // (u,( Ortm (x,y,( Ortm (x,y,u1))))) by A1, Th7;

      then (( Ortm (x,y,v)),( Ortm (x,y,v1))) // (u,u1) by A1, Th7;

      hence thesis;

    end;

    theorem :: ANALORT:20

    

     Th20: (u,u,v,w) are_COrte_wrt (x,y) by ANALOAF: 9;

    theorem :: ANALORT:21

    (u,u,v,w) are_COrtm_wrt (x,y) by ANALOAF: 9;

    theorem :: ANALORT:22

    (u,v,w,w) are_COrte_wrt (x,y) by ANALOAF: 9;

    theorem :: ANALORT:23

    (u,v,w,w) are_COrtm_wrt (x,y) by ANALOAF: 9;

    theorem :: ANALORT:24

    

     Th24: Gen (x,y) implies (u,v,( Orte (x,y,u)),( Orte (x,y,v))) are_Ort_wrt (x,y)

    proof

      assume

       A1: Gen (x,y);

      set w = (( Orte (x,y,v)) - ( Orte (x,y,u)));

      

       A2: w = ( Orte (x,y,(v - u))) by A1, Th11

      .= ((( pr2 (x,y,(v - u))) * x) + (( - ( pr1 (x,y,(v - u)))) * y));

      ( PProJ (x,y,(v - u),w)) = ((( pr1 (x,y,(v - u))) * ( pr1 (x,y,w))) + (( pr2 (x,y,(v - u))) * ( pr2 (x,y,w)))) by GEOMTRAP:def 6

      .= ((( pr1 (x,y,(v - u))) * ( pr2 (x,y,(v - u)))) + (( pr2 (x,y,(v - u))) * ( pr2 (x,y,w)))) by A1, A2, Lm6

      .= ((( pr1 (x,y,(v - u))) * ( pr2 (x,y,(v - u)))) + (( - ( pr1 (x,y,(v - u)))) * ( pr2 (x,y,(v - u))))) by A1, A2, Lm6

      .= 0 ;

      then ((v - u),w) are_Ort_wrt (x,y) by A1, GEOMTRAP: 32;

      hence thesis by ANALMETR:def 3;

    end;

    theorem :: ANALORT:25

    (u,v,( Orte (x,y,u)),( Orte (x,y,v))) are_COrte_wrt (x,y) by ANALOAF: 8;

    theorem :: ANALORT:26

    (u,v,( Ortm (x,y,u)),( Ortm (x,y,v))) are_COrtm_wrt (x,y) by ANALOAF: 8;

    theorem :: ANALORT:27

     Gen (x,y) implies ((u,v) // (u1,v1) iff ex u2, v2 st u2 <> v2 & (u2,v2,u,v) are_COrte_wrt (x,y) & (u2,v2,u1,v1) are_COrte_wrt (x,y))

    proof

      assume

       A1: Gen (x,y);

      

       A2: (u,v) // (u1,v1) implies ex u2, v2 st u2 <> v2 & (u2,v2,u,v) are_COrte_wrt (x,y) & (u2,v2,u1,v1) are_COrte_wrt (x,y)

      proof

        assume

         A3: (u,v) // (u1,v1);

         A4:

        now

          assume that

           A5: u = v and

           A6: u1 = v1;

          take u2 = ( 0. V), v2 = x;

          

           A7: (( Orte (x,y,u2)),( Orte (x,y,v2))) // (u,v) by A5, ANALOAF: 9;

          (( Orte (x,y,u2)),( Orte (x,y,v2))) // (u1,v1) by A6, ANALOAF: 9;

          then

           A8: (u2,v2,u1,v1) are_COrte_wrt (x,y);

          

           A9: (u2,v2,u,v) are_COrte_wrt (x,y) by A7;

          u2 <> v2 by A1, Lm4;

          hence thesis by A8, A9;

        end;

         A10:

        now

          assume

           A11: u <> v;

          consider u2 such that

           A12: ( Orte (x,y,u2)) = u by A1, Th15;

          consider v2 such that

           A13: ( Orte (x,y,v2)) = v by A1, Th15;

          (( Orte (x,y,u2)),( Orte (x,y,v2))) // (u,v) by A12, A13, ANALOAF: 8;

          then

           A14: (u2,v2,u,v) are_COrte_wrt (x,y);

          (u2,v2,u1,v1) are_COrte_wrt (x,y) by A3, A12, A13;

          hence thesis by A11, A12, A13, A14;

        end;

        now

          assume

           A15: u1 <> v1;

          consider u2 such that

           A16: ( Orte (x,y,u2)) = u1 by A1, Th15;

          consider v2 such that

           A17: ( Orte (x,y,v2)) = v1 by A1, Th15;

          (( Orte (x,y,u2)),( Orte (x,y,v2))) // (u1,v1) by A16, A17, ANALOAF: 8;

          then

           A18: (u2,v2,u1,v1) are_COrte_wrt (x,y);

          (( Orte (x,y,u2)),( Orte (x,y,v2))) // (u,v) by A3, A16, A17, ANALOAF: 12;

          then (u2,v2,u,v) are_COrte_wrt (x,y);

          hence thesis by A15, A16, A17, A18;

        end;

        hence thesis by A4, A10;

      end;

      (ex u2, v2 st u2 <> v2 & (u2,v2,u,v) are_COrte_wrt (x,y) & (u2,v2,u1,v1) are_COrte_wrt (x,y)) implies (u,v) // (u1,v1) by A1, Th13, ANALOAF: 11;

      hence thesis by A2;

    end;

    theorem :: ANALORT:28

     Gen (x,y) implies ((u,v) // (u1,v1) iff ex u2, v2 st u2 <> v2 & (u2,v2,u,v) are_COrtm_wrt (x,y) & (u2,v2,u1,v1) are_COrtm_wrt (x,y))

    proof

      assume

       A1: Gen (x,y);

      

       A2: (u,v) // (u1,v1) implies ex u2, v2 st u2 <> v2 & (u2,v2,u,v) are_COrtm_wrt (x,y) & (u2,v2,u1,v1) are_COrtm_wrt (x,y)

      proof

        assume

         A3: (u,v) // (u1,v1);

         A4:

        now

          assume that

           A5: u = v and

           A6: u1 = v1;

          take u2 = ( 0. V), v2 = x;

          

           A7: (( Ortm (x,y,u2)),( Ortm (x,y,v2))) // (u,v) by A5, ANALOAF: 9;

          (( Ortm (x,y,u2)),( Ortm (x,y,v2))) // (u1,v1) by A6, ANALOAF: 9;

          then

           A8: (u2,v2,u1,v1) are_COrtm_wrt (x,y);

          

           A9: (u2,v2,u,v) are_COrtm_wrt (x,y) by A7;

          u2 <> v2 by A1, Lm4;

          hence thesis by A8, A9;

        end;

         A10:

        now

          assume

           A11: u <> v;

          consider u2 such that

           A12: ( Ortm (x,y,u2)) = u by A1, Th8;

          consider v2 such that

           A13: ( Ortm (x,y,v2)) = v by A1, Th8;

          (( Ortm (x,y,u2)),( Ortm (x,y,v2))) // (u,v) by A12, A13, ANALOAF: 8;

          then

           A14: (u2,v2,u,v) are_COrtm_wrt (x,y);

          (u2,v2,u1,v1) are_COrtm_wrt (x,y) by A3, A12, A13;

          hence thesis by A11, A12, A13, A14;

        end;

        now

          assume

           A15: u1 <> v1;

          consider u2 such that

           A16: ( Ortm (x,y,u2)) = u1 by A1, Th8;

          consider v2 such that

           A17: ( Ortm (x,y,v2)) = v1 by A1, Th8;

          (( Ortm (x,y,u2)),( Ortm (x,y,v2))) // (u1,v1) by A16, A17, ANALOAF: 8;

          then

           A18: (u2,v2,u1,v1) are_COrtm_wrt (x,y);

          (( Ortm (x,y,u2)),( Ortm (x,y,v2))) // (u,v) by A3, A16, A17, ANALOAF: 12;

          then (u2,v2,u,v) are_COrtm_wrt (x,y);

          hence thesis by A15, A16, A17, A18;

        end;

        hence thesis by A4, A10;

      end;

      (ex u2, v2 st u2 <> v2 & (u2,v2,u,v) are_COrtm_wrt (x,y) & (u2,v2,u1,v1) are_COrtm_wrt (x,y)) implies (u,v) // (u1,v1) by A1, Th6, ANALOAF: 11;

      hence thesis by A2;

    end;

    theorem :: ANALORT:29

     Gen (x,y) implies ((u,v,u1,v1) are_Ort_wrt (x,y) iff (u,v,u1,v1) are_COrte_wrt (x,y) or (u,v,v1,u1) are_COrte_wrt (x,y))

    proof

      assume

       A1: Gen (x,y);

       A2:

      now

        assume u = v;

        then (v - u) = ( 0. V) by RLVECT_1: 15;

        then ((v - u),(v1 - u1)) are_Ort_wrt (x,y) by A1, ANALMETR: 5;

        hence (u,v,u1,v1) are_Ort_wrt (x,y) by ANALMETR:def 3;

      end;

      now

        assume

         A3: u <> v;

        set u2 = ( Orte (x,y,u)), v2 = ( Orte (x,y,v));

        

         A4: (v - u) <> ( 0. V) by A3, RLVECT_1: 21;

        (u,v,u2,v2) are_Ort_wrt (x,y) by A1, Th24;

        then

         A5: ((v - u),(v2 - u2)) are_Ort_wrt (x,y) by ANALMETR:def 3;

         A6:

        now

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

          then ((v - u),(v1 - u1)) are_Ort_wrt (x,y) by ANALMETR:def 3;

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

          then (u2,v2) // (u1,v1) or (u2,v2) // (v1,u1) by ANALMETR: 14;

          hence (u,v,u1,v1) are_COrte_wrt (x,y) or (u,v,v1,u1) are_COrte_wrt (x,y);

        end;

        now

          assume (u,v,u1,v1) are_COrte_wrt (x,y) or (u,v,v1,u1) are_COrte_wrt (x,y);

          then (u2,v2) // (u1,v1) or (u2,v2) // (v1,u1);

          then

          consider a, b such that

           A7: (a * (v2 - u2)) = (b * (v1 - u1)) and

           A8: a <> 0 or b <> 0 by ANALMETR: 14;

           A9:

          now

            assume

             A10: b = 0 ;

            then ( 0. V) = (a * (v2 - u2)) by A7, RLVECT_1: 10;

            then (v2 - u2) = ( 0. V) by A8, A10, RLVECT_1: 11;

            then v2 = u2 by RLVECT_1: 21;

            then u = v by A1, Th13;

            then (v - u) = ( 0. V) by RLVECT_1: 15;

            then ((v - u),(v1 - u1)) are_Ort_wrt (x,y) by A1, ANALMETR: 5;

            hence (u,v,u1,v1) are_Ort_wrt (x,y) by ANALMETR:def 3;

          end;

          now

            assume

             A11: b <> 0 ;

            (((b " ) * a) * (v2 - u2)) = ((b " ) * (b * (v1 - u1))) by A7, RLVECT_1:def 7;

            then (((b " ) * a) * (v2 - u2)) = (((b " ) * b) * (v1 - u1)) by RLVECT_1:def 7;

            then (((b " ) * a) * (v2 - u2)) = (1 * (v1 - u1)) by A11, XCMPLX_0:def 7;

            then (v1 - u1) = (((b " ) * a) * (v2 - u2)) by RLVECT_1:def 8;

            then ((v - u),(v1 - u1)) are_Ort_wrt (x,y) by A5, ANALMETR: 7;

            hence (u,v,u1,v1) are_Ort_wrt (x,y) by ANALMETR:def 3;

          end;

          hence (u,v,u1,v1) are_Ort_wrt (x,y) by A9;

        end;

        hence thesis by A6;

      end;

      hence thesis by A2, Th20;

    end;

    theorem :: ANALORT:30

     Gen (x,y) & (u,v,u1,v1) are_COrte_wrt (x,y) & (u,v,v1,u1) are_COrte_wrt (x,y) implies u = v or u1 = v1

    proof

      assume

       A1: Gen (x,y);

      assume that

       A2: (u,v,u1,v1) are_COrte_wrt (x,y) and

       A3: (u,v,v1,u1) are_COrte_wrt (x,y);

      assume that

       A4: u <> v and

       A5: u1 <> v1;

      

       A6: (( Orte (x,y,u)),( Orte (x,y,v))) // (u1,v1) by A2;

      

       A7: (( Orte (x,y,u)),( Orte (x,y,v))) // (v1,u1) by A3;

      ( Orte (x,y,u)) <> ( Orte (x,y,v)) by A1, A4, Th13;

      hence contradiction by A5, A6, A7, ANALOAF: 10, ANALOAF: 11;

    end;

    theorem :: ANALORT:31

     Gen (x,y) & (u,v,u1,v1) are_COrtm_wrt (x,y) & (u,v,v1,u1) are_COrtm_wrt (x,y) implies u = v or u1 = v1

    proof

      assume

       A1: Gen (x,y);

      assume that

       A2: (u,v,u1,v1) are_COrtm_wrt (x,y) and

       A3: (u,v,v1,u1) are_COrtm_wrt (x,y);

      assume that

       A4: u <> v and

       A5: u1 <> v1;

      

       A6: (( Ortm (x,y,u)),( Ortm (x,y,v))) // (u1,v1) by A2;

      

       A7: (( Ortm (x,y,u)),( Ortm (x,y,v))) // (v1,u1) by A3;

      ( Ortm (x,y,u)) <> ( Ortm (x,y,v)) by A1, A4, Th6;

      hence contradiction by A5, A6, A7, ANALOAF: 10, ANALOAF: 11;

    end;

    theorem :: ANALORT:32

     Gen (x,y) & (u,v,u1,v1) are_COrte_wrt (x,y) & (u,v,u1,w) are_COrte_wrt (x,y) implies (u,v,v1,w) are_COrte_wrt (x,y) or (u,v,w,v1) are_COrte_wrt (x,y)

    proof

      assume that

       A1: Gen (x,y) and

       A2: (u,v,u1,v1) are_COrte_wrt (x,y) and

       A3: (u,v,u1,w) are_COrte_wrt (x,y);

      

       A4: (( Orte (x,y,u)),( Orte (x,y,v))) // (u1,v1) by A2;

      

       A5: (( Orte (x,y,u)),( Orte (x,y,v))) // (u1,w) by A3;

      now

        assume

         A6: u <> v;

        now

          assume that

           A7: u1 <> v1 and

           A8: u1 <> w;

          

           A9: (u1,v1) // (u1,w) by A1, A4, A5, A6, Th13, ANALOAF: 11;

           A10:

          now

            assume

             A11: (u1,v1) // (v1,w);

            (u1,v1) // (( Orte (x,y,u)),( Orte (x,y,v))) by A4, ANALOAF: 12;

            then (( Orte (x,y,u)),( Orte (x,y,v))) // (v1,w) by A7, A11, ANALOAF: 11;

            hence thesis;

          end;

          now

            assume

             A12: (u1,w) // (w,v1);

            (u1,w) // (( Orte (x,y,u)),( Orte (x,y,v))) by A5, ANALOAF: 12;

            then (( Orte (x,y,u)),( Orte (x,y,v))) // (w,v1) by A8, A12, ANALOAF: 11;

            hence thesis;

          end;

          hence thesis by A9, A10, ANALOAF: 14;

        end;

        hence thesis by A2, A3;

      end;

      hence thesis by Th20;

    end;

    theorem :: ANALORT:33

     Gen (x,y) & (u,v,u1,v1) are_COrtm_wrt (x,y) & (u,v,u1,w) are_COrtm_wrt (x,y) implies (u,v,v1,w) are_COrtm_wrt (x,y) or (u,v,w,v1) are_COrtm_wrt (x,y)

    proof

      assume that

       A1: Gen (x,y) and

       A2: (u,v,u1,v1) are_COrtm_wrt (x,y) and

       A3: (u,v,u1,w) are_COrtm_wrt (x,y);

      

       A4: (( Ortm (x,y,u)),( Ortm (x,y,v))) // (u1,v1) by A2;

      

       A5: (( Ortm (x,y,u)),( Ortm (x,y,v))) // (u1,w) by A3;

       A6:

      now

        assume that

         A7: u <> v and

         A8: u1 <> v1;

        (u1,v1) // (u1,w) by A1, A4, A5, A7, Th6, ANALOAF: 11;

        then

         A9: (u1,v1) // (v1,w) or (u1,w) // (w,v1) by ANALOAF: 14;

        now

          assume

           A10: u1 <> w;

          

           A11: (u1,v1) // (( Ortm (x,y,u)),( Ortm (x,y,v))) by A4, ANALOAF: 12;

          (u1,w) // (( Ortm (x,y,u)),( Ortm (x,y,v))) by A5, ANALOAF: 12;

          then (( Ortm (x,y,u)),( Ortm (x,y,v))) // (v1,w) or (( Ortm (x,y,u)),( Ortm (x,y,v))) // (w,v1) by A8, A9, A10, A11, ANALOAF: 11;

          hence thesis;

        end;

        hence thesis by A2;

      end;

      u = v implies thesis by ANALOAF: 9;

      hence thesis by A3, A6;

    end;

    theorem :: ANALORT:34

    (u,v,u1,v1) are_COrte_wrt (x,y) implies (v,u,v1,u1) are_COrte_wrt (x,y) by ANALOAF: 12;

    theorem :: ANALORT:35

    (u,v,u1,v1) are_COrtm_wrt (x,y) implies (v,u,v1,u1) are_COrtm_wrt (x,y) by ANALOAF: 12;

    theorem :: ANALORT:36

     Gen (x,y) & (u,v,u1,v1) are_COrte_wrt (x,y) & (u,v,v1,w) are_COrte_wrt (x,y) implies (u,v,u1,w) are_COrte_wrt (x,y)

    proof

      assume

       A1: Gen (x,y);

      assume that

       A2: (u,v,u1,v1) are_COrte_wrt (x,y) and

       A3: (u,v,v1,w) are_COrte_wrt (x,y);

      

       A4: (( Orte (x,y,u)),( Orte (x,y,v))) // (u1,v1) by A2;

      

       A5: (( Orte (x,y,u)),( Orte (x,y,v))) // (v1,w) by A3;

      

       A6: (u1,v1) // (( Orte (x,y,u)),( Orte (x,y,v))) by A4, ANALOAF: 12;

       A7:

      now

        assume u <> v;

        then (u1,v1) // (v1,w) by A1, A4, A5, Th13, ANALOAF: 11;

        then

         A8: (u1,v1) // (u1,w) by ANALOAF: 13;

        u1 <> v1 implies thesis by A6, A8, ANALOAF: 11;

        hence thesis by A3;

      end;

      u = v implies thesis by ANALOAF: 9;

      hence thesis by A7;

    end;

    theorem :: ANALORT:37

     Gen (x,y) & (u,v,u1,v1) are_COrtm_wrt (x,y) & (u,v,v1,w) are_COrtm_wrt (x,y) implies (u,v,u1,w) are_COrtm_wrt (x,y)

    proof

      assume

       A1: Gen (x,y);

      assume that

       A2: (u,v,u1,v1) are_COrtm_wrt (x,y) and

       A3: (u,v,v1,w) are_COrtm_wrt (x,y);

      

       A4: (( Ortm (x,y,u)),( Ortm (x,y,v))) // (u1,v1) by A2;

      

       A5: (( Ortm (x,y,u)),( Ortm (x,y,v))) // (v1,w) by A3;

      

       A6: (u1,v1) // (( Ortm (x,y,u)),( Ortm (x,y,v))) by A4, ANALOAF: 12;

       A7:

      now

        assume u <> v;

        then (u1,v1) // (v1,w) by A1, A4, A5, Th6, ANALOAF: 11;

        then

         A8: (u1,v1) // (u1,w) by ANALOAF: 13;

        u1 <> v1 implies thesis by A6, A8, ANALOAF: 11;

        hence thesis by A3;

      end;

      u = v implies thesis by ANALOAF: 9;

      hence thesis by A7;

    end;

    theorem :: ANALORT:38

     Gen (x,y) implies for u, v, w holds ex u1 st w <> u1 & (w,u1,u,v) are_COrte_wrt (x,y)

    proof

      assume

       A1: Gen (x,y);

      let u, v, w;

       A2:

      now

        assume

         A3: u = v;

        take u1 = (w + x);

        (( Orte (x,y,w)),( Orte (x,y,u1))) // (u,v) by A3, ANALOAF: 9;

        then

         A4: (w,u1,u,v) are_COrte_wrt (x,y);

        now

          assume w = u1;

          then x = ( 0. V) by RLVECT_1: 9;

          hence contradiction by A1, Lm4;

        end;

        hence thesis by A4;

      end;

      now

        assume

         A5: u <> v;

        consider u2 such that

         A6: ( Orte (x,y,u2)) = u by A1, Th15;

        consider v2 such that

         A7: ( Orte (x,y,v2)) = v by A1, Th15;

        take u1 = ((v2 + w) - u2);

        (u2,v2) // (w,u1) by ANALOAF: 16;

        then (w,u1) // (u2,v2) by ANALOAF: 12;

        then (( Orte (x,y,w)),( Orte (x,y,u1))) // (( Orte (x,y,u2)),( Orte (x,y,v2))) by A1, Th16;

        then

         A8: (w,u1,u,v) are_COrte_wrt (x,y) by A6, A7;

        now

          assume w = u1;

          then w = (w + (v2 - u2)) by RLVECT_1:def 3;

          then (v2 - u2) = ( 0. V) by RLVECT_1: 9;

          hence contradiction by A5, A6, A7, RLVECT_1: 21;

        end;

        hence thesis by A8;

      end;

      hence thesis by A2;

    end;

    theorem :: ANALORT:39

     Gen (x,y) implies for u, v, w holds ex u1 st w <> u1 & (w,u1,u,v) are_COrtm_wrt (x,y)

    proof

      assume

       A1: Gen (x,y);

      let u, v, w;

       A2:

      now

        assume

         A3: u = v;

        take u1 = (w + x);

        (( Ortm (x,y,w)),( Ortm (x,y,u1))) // (u,v) by A3, ANALOAF: 9;

        then

         A4: (w,u1,u,v) are_COrtm_wrt (x,y);

        now

          assume w = u1;

          then x = ( 0. V) by RLVECT_1: 9;

          hence contradiction by A1, Lm4;

        end;

        hence thesis by A4;

      end;

      now

        assume

         A5: u <> v;

        consider u2 such that

         A6: ( Ortm (x,y,u2)) = u by A1, Th8;

        consider v2 such that

         A7: ( Ortm (x,y,v2)) = v by A1, Th8;

        take u1 = ((v2 + w) - u2);

        (u2,v2) // (w,u1) by ANALOAF: 16;

        then (w,u1) // (u2,v2) by ANALOAF: 12;

        then (( Ortm (x,y,w)),( Ortm (x,y,u1))) // (( Ortm (x,y,u2)),( Ortm (x,y,v2))) by A1, Th17;

        then

         A8: (w,u1,u,v) are_COrtm_wrt (x,y) by A6, A7;

        now

          assume w = u1;

          then w = (w + (v2 - u2)) by RLVECT_1:def 3;

          then (v2 - u2) = ( 0. V) by RLVECT_1: 9;

          hence contradiction by A5, A6, A7, RLVECT_1: 21;

        end;

        hence thesis by A8;

      end;

      hence thesis by A2;

    end;

    theorem :: ANALORT:40

    

     Th40: Gen (x,y) implies for u, v, w holds ex u1 st w <> u1 & (u,v,w,u1) are_COrte_wrt (x,y)

    proof

      assume

       A1: Gen (x,y);

      let u, v, w;

       A2:

      now

        assume

         A3: u = v;

        take u1 = (w + x);

        (( Orte (x,y,u)),( Orte (x,y,v))) // (w,u1) by A3, ANALOAF: 9;

        then

         A4: (u,v,w,u1) are_COrte_wrt (x,y);

        now

          assume w = u1;

          then x = ( 0. V) by RLVECT_1: 9;

          hence contradiction by A1, Lm4;

        end;

        hence thesis by A4;

      end;

      now

        assume

         A5: u <> v;

        consider u2 such that

         A6: ( Orte (x,y,u2)) = u by A1, Th15;

        consider v2 such that

         A7: ( Orte (x,y,v2)) = v by A1, Th15;

        take u1 = ((u2 + w) - v2);

        (v2,u2) // (w,u1) by ANALOAF: 16;

        then (( Orte (x,y,v2)),( Orte (x,y,u2))) // (( Orte (x,y,w)),( Orte (x,y,u1))) by A1, Th16;

        then (( Orte (x,y,w)),( Orte (x,y,u1))) // (v,u) by A6, A7, ANALOAF: 12;

        then (( Orte (x,y,u1)),( Orte (x,y,w))) // (u,v) by ANALOAF: 12;

        then

         A8: (u1,w,u,v) are_COrte_wrt (x,y);

        now

          assume w = u1;

          then w = (w + (u2 - v2)) by RLVECT_1:def 3;

          then (u2 - v2) = ( 0. V) by RLVECT_1: 9;

          hence contradiction by A5, A6, A7, RLVECT_1: 21;

        end;

        hence thesis by A1, A8, Th18;

      end;

      hence thesis by A2;

    end;

    theorem :: ANALORT:41

    

     Th41: Gen (x,y) implies for u, v, w holds ex u1 st w <> u1 & (u,v,w,u1) are_COrtm_wrt (x,y)

    proof

      assume

       A1: Gen (x,y);

      let u, v, w;

       A2:

      now

        assume

         A3: u = v;

        take u1 = (w + x);

        (( Ortm (x,y,w)),( Ortm (x,y,u1))) // (u,v) by A3, ANALOAF: 9;

        then

         A4: (w,u1,u,v) are_COrtm_wrt (x,y);

        w <> u1

        proof

          assume w = u1;

          then x = ( 0. V) by RLVECT_1: 9;

          hence contradiction by A1, Lm4;

        end;

        hence thesis by A1, A4, Th19;

      end;

      now

        assume

         A5: u <> v;

        consider u2 such that

         A6: ( Ortm (x,y,u2)) = u by A1, Th8;

        consider v2 such that

         A7: ( Ortm (x,y,v2)) = v by A1, Th8;

        take u1 = ((v2 + w) - u2);

        (u2,v2) // (w,u1) by ANALOAF: 16;

        then (w,u1) // (u2,v2) by ANALOAF: 12;

        then (( Ortm (x,y,w)),( Ortm (x,y,u1))) // (( Ortm (x,y,u2)),( Ortm (x,y,v2))) by A1, Th17;

        then

         A8: (w,u1,u,v) are_COrtm_wrt (x,y) by A6, A7;

        w <> u1

        proof

          assume w = u1;

          then w = (w + (v2 - u2)) by RLVECT_1:def 3;

          then (v2 - u2) = ( 0. V) by RLVECT_1: 9;

          hence contradiction by A5, A6, A7, RLVECT_1: 21;

        end;

        hence thesis by A1, A8, Th19;

      end;

      hence thesis by A2;

    end;

    theorem :: ANALORT:42

     Gen (x,y) & (u,u1,v,v1) are_COrte_wrt (x,y) & (w,w1,v,v1) are_COrte_wrt (x,y) & (w,w1,u2,v2) are_COrte_wrt (x,y) implies w = w1 or v = v1 or (u,u1,u2,v2) are_COrte_wrt (x,y)

    proof

      assume

       A1: Gen (x,y);

      assume that

       A2: (u,u1,v,v1) are_COrte_wrt (x,y) and

       A3: (w,w1,v,v1) are_COrte_wrt (x,y) and

       A4: (w,w1,u2,v2) are_COrte_wrt (x,y);

      (( Orte (x,y,u)),( Orte (x,y,u1))) // (v,v1) by A2;

      then

       A5: (v,v1) // (( Orte (x,y,u)),( Orte (x,y,u1))) by ANALOAF: 12;

      (( Orte (x,y,w)),( Orte (x,y,w1))) // (v,v1) by A3;

      then

       A6: (v,v1) // (( Orte (x,y,w)),( Orte (x,y,w1))) by ANALOAF: 12;

      

       A7: (( Orte (x,y,w)),( Orte (x,y,w1))) // (u2,v2) by A4;

      now

        assume that

         A8: w <> w1 and

         A9: v <> v1;

        (( Orte (x,y,w)),( Orte (x,y,w1))) // (( Orte (x,y,u)),( Orte (x,y,u1))) by A5, A6, A9, ANALOAF: 11;

        then (( Orte (x,y,u)),( Orte (x,y,u1))) // (u2,v2) by A1, A7, A8, Th13, ANALOAF: 11;

        hence (u,u1,u2,v2) are_COrte_wrt (x,y);

      end;

      hence thesis;

    end;

    theorem :: ANALORT:43

     Gen (x,y) & (u,u1,v,v1) are_COrtm_wrt (x,y) & (w,w1,v,v1) are_COrtm_wrt (x,y) & (w,w1,u2,v2) are_COrtm_wrt (x,y) implies w = w1 or v = v1 or (u,u1,u2,v2) are_COrtm_wrt (x,y)

    proof

      assume

       A1: Gen (x,y);

      assume that

       A2: (u,u1,v,v1) are_COrtm_wrt (x,y) and

       A3: (w,w1,v,v1) are_COrtm_wrt (x,y) and

       A4: (w,w1,u2,v2) are_COrtm_wrt (x,y);

      (( Ortm (x,y,u)),( Ortm (x,y,u1))) // (v,v1) by A2;

      then

       A5: (v,v1) // (( Ortm (x,y,u)),( Ortm (x,y,u1))) by ANALOAF: 12;

      (( Ortm (x,y,w)),( Ortm (x,y,w1))) // (v,v1) by A3;

      then

       A6: (v,v1) // (( Ortm (x,y,w)),( Ortm (x,y,w1))) by ANALOAF: 12;

      

       A7: (( Ortm (x,y,w)),( Ortm (x,y,w1))) // (u2,v2) by A4;

      now

        assume that

         A8: w <> w1 and

         A9: v <> v1;

        (( Ortm (x,y,w)),( Ortm (x,y,w1))) // (( Ortm (x,y,u)),( Ortm (x,y,u1))) by A5, A6, A9, ANALOAF: 11;

        then (( Ortm (x,y,u)),( Ortm (x,y,u1))) // (u2,v2) by A1, A7, A8, Th6, ANALOAF: 11;

        hence (u,u1,u2,v2) are_COrtm_wrt (x,y);

      end;

      hence thesis;

    end;

    theorem :: ANALORT:44

     Gen (x,y) & (u,u1,v,v1) are_COrte_wrt (x,y) & (v,v1,w,w1) are_COrte_wrt (x,y) & (u2,v2,w,w1) are_COrte_wrt (x,y) implies (u,u1,u2,v2) are_COrte_wrt (x,y) or v = v1 or w = w1

    proof

      assume

       A1: Gen (x,y);

      assume that

       A2: (u,u1,v,v1) are_COrte_wrt (x,y) and

       A3: (v,v1,w,w1) are_COrte_wrt (x,y) and

       A4: (u2,v2,w,w1) are_COrte_wrt (x,y);

      (v,v1,u1,u) are_COrte_wrt (x,y) by A1, A2, Th18;

      then

       A5: (( Orte (x,y,v)),( Orte (x,y,v1))) // (u1,u);

      (( Orte (x,y,v)),( Orte (x,y,v1))) // (w,w1) by A3;

      then

       A6: (w,w1) // (( Orte (x,y,v)),( Orte (x,y,v1))) by ANALOAF: 12;

      (( Orte (x,y,u2)),( Orte (x,y,v2))) // (w,w1) by A4;

      then

       A7: (w,w1) // (( Orte (x,y,u2)),( Orte (x,y,v2))) by ANALOAF: 12;

      now

        assume that

         A8: w <> w1 and

         A9: v <> v1;

        (( Orte (x,y,v)),( Orte (x,y,v1))) // (( Orte (x,y,u2)),( Orte (x,y,v2))) by A6, A7, A8, ANALOAF: 11;

        then (( Orte (x,y,u2)),( Orte (x,y,v2))) // (u1,u) by A1, A5, A9, Th13, ANALOAF: 11;

        then (( Orte (x,y,v2)),( Orte (x,y,u2))) // (u,u1) by ANALOAF: 12;

        then (v2,u2,u,u1) are_COrte_wrt (x,y);

        hence thesis by A1, Th18;

      end;

      hence thesis;

    end;

    theorem :: ANALORT:45

     Gen (x,y) & (u,u1,v,v1) are_COrtm_wrt (x,y) & (v,v1,w,w1) are_COrtm_wrt (x,y) & (u2,v2,w,w1) are_COrtm_wrt (x,y) implies (u,u1,u2,v2) are_COrtm_wrt (x,y) or v = v1 or w = w1

    proof

      assume

       A1: Gen (x,y);

      assume that

       A2: (u,u1,v,v1) are_COrtm_wrt (x,y) and

       A3: (v,v1,w,w1) are_COrtm_wrt (x,y) and

       A4: (u2,v2,w,w1) are_COrtm_wrt (x,y);

      (( Ortm (x,y,u)),( Ortm (x,y,u1))) // (v,v1) by A2;

      then

       A5: (v,v1) // (( Ortm (x,y,u)),( Ortm (x,y,u1))) by ANALOAF: 12;

      (w,w1,v,v1) are_COrtm_wrt (x,y) by A1, A3, Th19;

      then (( Ortm (x,y,w)),( Ortm (x,y,w1))) // (v,v1);

      then

       A6: (v,v1) // (( Ortm (x,y,w)),( Ortm (x,y,w1))) by ANALOAF: 12;

      (w,w1,u2,v2) are_COrtm_wrt (x,y) by A1, A4, Th19;

      then

       A7: (( Ortm (x,y,w)),( Ortm (x,y,w1))) // (u2,v2);

      now

        assume that

         A8: w <> w1 and

         A9: v <> v1;

        (( Ortm (x,y,w)),( Ortm (x,y,w1))) // (( Ortm (x,y,u)),( Ortm (x,y,u1))) by A5, A6, A9, ANALOAF: 11;

        then (( Ortm (x,y,u)),( Ortm (x,y,u1))) // (u2,v2) by A1, A7, A8, Th6, ANALOAF: 11;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: ANALORT:46

     Gen (x,y) & (u,u1,v,v1) are_COrte_wrt (x,y) & (v,v1,w,w1) are_COrte_wrt (x,y) & (u,u1,u2,v2) are_COrte_wrt (x,y) implies (u2,v2,w,w1) are_COrte_wrt (x,y) or v = v1 or u = u1

    proof

      assume

       A1: Gen (x,y);

      assume that

       A2: (u,u1,v,v1) are_COrte_wrt (x,y) and

       A3: (v,v1,w,w1) are_COrte_wrt (x,y) and

       A4: (u,u1,u2,v2) are_COrte_wrt (x,y);

      

       A5: (( Orte (x,y,u)),( Orte (x,y,u1))) // (v,v1) by A2;

      

       A6: (( Orte (x,y,v)),( Orte (x,y,v1))) // (w,w1) by A3;

      

       A7: (( Orte (x,y,u)),( Orte (x,y,u1))) // (u2,v2) by A4;

      now

        assume that

         A8: u <> u1 and

         A9: v <> v1;

        (v,v1) // (u2,v2) by A1, A5, A7, A8, Th13, ANALOAF: 11;

        then (( Orte (x,y,v)),( Orte (x,y,v1))) // (( Orte (x,y,u2)),( Orte (x,y,v2))) by A1, Th16;

        then (( Orte (x,y,u2)),( Orte (x,y,v2))) // (w,w1) by A1, A6, A9, Th13, ANALOAF: 11;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: ANALORT:47

     Gen (x,y) & (u,u1,v,v1) are_COrtm_wrt (x,y) & (v,v1,w,w1) are_COrtm_wrt (x,y) & (u,u1,u2,v2) are_COrtm_wrt (x,y) implies (u2,v2,w,w1) are_COrtm_wrt (x,y) or v = v1 or u = u1

    proof

      assume

       A1: Gen (x,y);

      assume that

       A2: (u,u1,v,v1) are_COrtm_wrt (x,y) and

       A3: (v,v1,w,w1) are_COrtm_wrt (x,y) and

       A4: (u,u1,u2,v2) are_COrtm_wrt (x,y);

      

       A5: (( Ortm (x,y,u)),( Ortm (x,y,u1))) // (v,v1) by A2;

      

       A6: (( Ortm (x,y,v)),( Ortm (x,y,v1))) // (w,w1) by A3;

      

       A7: (( Ortm (x,y,u)),( Ortm (x,y,u1))) // (u2,v2) by A4;

      now

        assume that

         A8: u <> u1 and

         A9: v <> v1;

        (v,v1) // (u2,v2) by A1, A5, A7, A8, Th6, ANALOAF: 11;

        then (( Ortm (x,y,v)),( Ortm (x,y,v1))) // (( Ortm (x,y,u2)),( Ortm (x,y,v2))) by A1, Th17;

        then (( Ortm (x,y,u2)),( Ortm (x,y,v2))) // (w,w1) by A1, A6, A9, Th6, ANALOAF: 11;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: ANALORT:48

     Gen (x,y) implies for v, w, u1, v1, w1 holds not (v,v1,w,u1) are_COrte_wrt (x,y) & not (v,v1,u1,w) are_COrte_wrt (x,y) & (u1,w1,u1,w) are_COrte_wrt (x,y) implies ex u2 st ((v,v1,v,u2) are_COrte_wrt (x,y) or (v,v1,u2,v) are_COrte_wrt (x,y)) & ((u1,w1,u1,u2) are_COrte_wrt (x,y) or (u1,w1,u2,u1) are_COrte_wrt (x,y))

    proof

      assume

       A1: Gen (x,y);

      let v, w, u1, v1, w1;

      consider u such that

       A2: v <> u and

       A3: (v,v1,v,u) are_COrte_wrt (x,y) by A1, Th40;

      assume that

       A4: not (v,v1,w,u1) are_COrte_wrt (x,y) and

       A5: not (v,v1,u1,w) are_COrte_wrt (x,y) and

       A6: (u1,w1,u1,w) are_COrte_wrt (x,y);

      

       A7: not (( Orte (x,y,v)),( Orte (x,y,v1))) // (w,u1) by A4;

      

       A8: (( Orte (x,y,v)),( Orte (x,y,v1))) // (v,u) by A3;

      

       A9: (( Orte (x,y,u1)),( Orte (x,y,w1))) // (u1,w) by A6;

      

       A10: not (( Orte (x,y,v)),( Orte (x,y,v1))) // (u1,w) by A5;

      

       A11: (v,u) // (( Orte (x,y,v)),( Orte (x,y,v1))) by A8, ANALOAF: 12;

      

       A12: (u1,w) // (( Orte (x,y,u1)),( Orte (x,y,w1))) by A9, ANALOAF: 12;

      

       A13: u1 <> w by A7, ANALOAF: 9;

      

       A14: not (v,u) // (u1,w) by A2, A10, A11, ANALOAF: 11;

      

       A15: not (v,u) // (w,u1) by A2, A7, A11, ANALOAF: 11;

       Gen (x,y) implies ex u, v st for w holds ex a, b st ((a * u) + (b * v)) = w

      proof

        assume

         A16: Gen (x,y);

        take x, y;

        thus thesis by A16, ANALMETR:def 1;

      end;

      then

      consider u2 such that

       A17: (v,u) // (v,u2) or (v,u) // (u2,v) and

       A18: (u1,w) // (u1,u2) or (u1,w) // (u2,u1) by A1, A14, A15, ANALOAF: 21;

      (( Orte (x,y,v)),( Orte (x,y,v1))) // (v,u2) or (( Orte (x,y,v)),( Orte (x,y,v1))) // (u2,v) by A2, A11, A17, ANALOAF: 11;

      then

       A19: (v,v1,v,u2) are_COrte_wrt (x,y) or (v,v1,u2,v) are_COrte_wrt (x,y);

      (( Orte (x,y,u1)),( Orte (x,y,w1))) // (u1,u2) or (( Orte (x,y,u1)),( Orte (x,y,w1))) // (u2,u1) by A12, A13, A18, ANALOAF: 11;

      then (u1,w1,u1,u2) are_COrte_wrt (x,y) or (u1,w1,u2,u1) are_COrte_wrt (x,y);

      hence thesis by A19;

    end;

    theorem :: ANALORT:49

     Gen (x,y) implies ex u, v, w st ((u,v,u,w) are_COrte_wrt (x,y) & for v1, w1 st (v1,w1,u,v) are_COrte_wrt (x,y) holds ( not (v1,w1,u,w) are_COrte_wrt (x,y) & not (v1,w1,w,u) are_COrte_wrt (x,y) or v1 = w1))

    proof

      assume

       A1: Gen (x,y);

       Gen (x,y) implies ex u, v st u <> v

      proof

        assume

         A2: Gen (x,y);

        take x, ( 0. V);

        thus thesis by A2, Lm4;

      end;

      then

      consider u, v such that

       A3: u <> v by A1;

      take u, v;

      consider w such that

       A4: w <> u and

       A5: (u,v,u,w) are_COrte_wrt (x,y) by A1, Th40;

      take w;

      thus (u,v,u,w) are_COrte_wrt (x,y) by A5;

      

       A6: (( Orte (x,y,u)),( Orte (x,y,v))) // (u,w) by A5;

      let v1, w1;

      assume (v1,w1,u,v) are_COrte_wrt (x,y);

      then

       A7: (( Orte (x,y,v1)),( Orte (x,y,w1))) // (u,v);

      now

        assume

         A8: v1 <> w1;

        assume (v1,w1,u,w) are_COrte_wrt (x,y) or (v1,w1,w,u) are_COrte_wrt (x,y);

        then (( Orte (x,y,v1)),( Orte (x,y,w1))) // (u,w) or (( Orte (x,y,v1)),( Orte (x,y,w1))) // (w,u);

        then (u,v) // (u,w) or (u,v) // (w,u) by A1, A7, A8, Th13, ANALOAF: 11;

        then (( Orte (x,y,u)),( Orte (x,y,v))) // (( Orte (x,y,u)),( Orte (x,y,w))) or (( Orte (x,y,u)),( Orte (x,y,v))) // (( Orte (x,y,w)),( Orte (x,y,u))) by A1, Th16;

        then (u,w) // (( Orte (x,y,u)),( Orte (x,y,w))) or (u,w) // (( Orte (x,y,w)),( Orte (x,y,u))) by A1, A3, A6, Th13, ANALOAF: 11;

        then

        consider a, b such that

         A9: (a * (w - u)) = (b * (( Orte (x,y,w)) - ( Orte (x,y,u)))) and

         A10: a <> 0 or b <> 0 by ANALMETR: 14;

        take a, b;

        (a * (w - u)) = (b * ( Orte (x,y,(w - u)))) by A1, A9, Th11;

        then

         A11: (a * ((( pr1 (x,y,(w - u))) * x) + (( pr2 (x,y,(w - u))) * y))) = (b * ( Orte (x,y,(w - u)))) by A1, Lm5;

         A12:

        now

          assume

           A13: a <> 0 ;

          

           A14: ( pr2 (x,y,(w - u))) <> 0

          proof

            assume

             A15: not thesis;

            then (a * ((( pr1 (x,y,(w - u))) * x) + (( pr2 (x,y,(w - u))) * y))) = (((b * 0 ) * x) + ((b * ( - ( pr1 (x,y,(w - u))))) * y)) by A11, Lm2;

            then (((a * ( pr1 (x,y,(w - u)))) * x) + ((a * ( pr2 (x,y,(w - u)))) * y)) = (((b * 0 ) * x) + ((b * ( - ( pr1 (x,y,(w - u))))) * y)) by Lm2;

            then (a * ( pr1 (x,y,(w - u)))) = 0 by A1, Lm3;

            then ( pr1 (x,y,(w - u))) = 0 by A13, XCMPLX_1: 6;

            

            then (w - u) = (( 0 * x) + ( 0 * y)) by A1, A15, Lm5

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

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

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

            hence thesis by A4, RLVECT_1: 21;

          end;

          (((a " ) * a) * ((( pr1 (x,y,(w - u))) * x) + (( pr2 (x,y,(w - u))) * y))) = ((a " ) * (b * ((( pr2 (x,y,(w - u))) * x) + (( - ( pr1 (x,y,(w - u)))) * y)))) by A11, RLVECT_1:def 7;

          then (((a " ) * a) * ((( pr1 (x,y,(w - u))) * x) + (( pr2 (x,y,(w - u))) * y))) = (((a " ) * b) * ((( pr2 (x,y,(w - u))) * x) + (( - ( pr1 (x,y,(w - u)))) * y))) by RLVECT_1:def 7;

          then (1 * ((( pr1 (x,y,(w - u))) * x) + (( pr2 (x,y,(w - u))) * y))) = (((a " ) * b) * ((( pr2 (x,y,(w - u))) * x) + (( - ( pr1 (x,y,(w - u)))) * y))) by A13, XCMPLX_0:def 7;

          then ((( pr1 (x,y,(w - u))) * x) + (( pr2 (x,y,(w - u))) * y)) = (((a " ) * b) * ((( pr2 (x,y,(w - u))) * x) + (( - ( pr1 (x,y,(w - u)))) * y))) by RLVECT_1:def 8;

          then

           A16: ((( pr1 (x,y,(w - u))) * x) + (( pr2 (x,y,(w - u))) * y)) = (((((a " ) * b) * ( pr2 (x,y,(w - u)))) * x) + ((((a " ) * b) * ( - ( pr1 (x,y,(w - u))))) * y)) by Lm2;

          then ( pr1 (x,y,(w - u))) = (((a " ) * b) * ( pr2 (x,y,(w - u)))) by A1, Lm3;

          then

           A17: ( pr2 (x,y,(w - u))) = ( - (((a " ) * b) * (((a " ) * b) * ( pr2 (x,y,(w - u)))))) by A1, A16, Lm3;

          ( - ((( pr2 (x,y,(w - u))) " ) * ( pr2 (x,y,(w - u))))) = ((( pr2 (x,y,(w - u))) " ) * ( - ( pr2 (x,y,(w - u)))))

          .= ((( pr2 (x,y,(w - u))) " ) * (((a " ) * b) * (((a " ) * b) * ( pr2 (x,y,(w - u)))))) by A17;

          then ( - 1) = (((( pr2 (x,y,(w - u))) " ) * ( pr2 (x,y,(w - u)))) * (((a " ) * b) * ((a " ) * b))) by A14, XCMPLX_0:def 7;

          then ( - 1) = (1 * (((a " ) * b) * ((a " ) * b))) by A14, XCMPLX_0:def 7;

          hence thesis by XREAL_1: 63;

        end;

        now

          assume

           A18: b <> 0 ;

          

           A19: ( pr2 (x,y,(w - u))) <> 0

          proof

            assume

             A20: not thesis;

            then (a * ((( pr1 (x,y,(w - u))) * x) + ( 0 * y))) = (((b * 0 ) * x) + ((b * ( - ( pr1 (x,y,(w - u))))) * y)) by A11, Lm2;

            then (((a * ( pr1 (x,y,(w - u)))) * x) + ((a * 0 ) * y)) = (((b * 0 ) * x) + ((b * ( - ( pr1 (x,y,(w - u))))) * y)) by Lm2;

            then (b * ( - ( pr1 (x,y,(w - u))))) = 0 by A1, Lm3;

            then ( - ( pr1 (x,y,(w - u)))) = 0 by A18, XCMPLX_1: 6;

            

            then (w - u) = (( 0 * x) + (( - 0 ) * y)) by A1, A20, Lm5

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

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

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

            hence thesis by A4, RLVECT_1: 21;

          end;

          ((b " ) * (a * ((( pr1 (x,y,(w - u))) * x) + (( pr2 (x,y,(w - u))) * y)))) = (((b " ) * b) * ((( pr2 (x,y,(w - u))) * x) + (( - ( pr1 (x,y,(w - u)))) * y))) by A11, RLVECT_1:def 7;

          then (((b " ) * a) * ((( pr1 (x,y,(w - u))) * x) + (( pr2 (x,y,(w - u))) * y))) = (((b " ) * b) * ((( pr2 (x,y,(w - u))) * x) + (( - ( pr1 (x,y,(w - u)))) * y))) by RLVECT_1:def 7;

          then (((b " ) * a) * ((( pr1 (x,y,(w - u))) * x) + (( pr2 (x,y,(w - u))) * y))) = (1 * ((( pr2 (x,y,(w - u))) * x) + (( - ( pr1 (x,y,(w - u)))) * y))) by A18, XCMPLX_0:def 7;

          then (((b " ) * a) * ((( pr1 (x,y,(w - u))) * x) + (( pr2 (x,y,(w - u))) * y))) = ((( pr2 (x,y,(w - u))) * x) + (( - ( pr1 (x,y,(w - u)))) * y)) by RLVECT_1:def 8;

          then

           A21: (((((b " ) * a) * ( pr1 (x,y,(w - u)))) * x) + ((((b " ) * a) * ( pr2 (x,y,(w - u)))) * y)) = ((( pr2 (x,y,(w - u))) * x) + (( - ( pr1 (x,y,(w - u)))) * y)) by Lm2;

          then (((b " ) * a) * ( pr2 (x,y,(w - u)))) = ( - ( pr1 (x,y,(w - u)))) by A1, Lm3;

          then

           A22: ( pr2 (x,y,(w - u))) = (((b " ) * a) * ( - (((b " ) * a) * ( pr2 (x,y,(w - u)))))) by A1, A21, Lm3;

          ( - ((( pr2 (x,y,(w - u))) " ) * ( pr2 (x,y,(w - u))))) = ((( pr2 (x,y,(w - u))) " ) * ( - ( pr2 (x,y,(w - u)))))

          .= ((( pr2 (x,y,(w - u))) " ) * (((b " ) * a) * (((b " ) * a) * ( pr2 (x,y,(w - u)))))) by A22;

          then ( - 1) = (((( pr2 (x,y,(w - u))) " ) * ( pr2 (x,y,(w - u)))) * (((b " ) * a) * ((b " ) * a))) by A19, XCMPLX_0:def 7;

          then ( - 1) = (1 * (((b " ) * a) * ((b " ) * a))) by A19, XCMPLX_0:def 7;

          hence thesis by XREAL_1: 63;

        end;

        hence thesis by A10, A12;

      end;

      hence thesis;

    end;

    theorem :: ANALORT:50

     Gen (x,y) implies for v, w, u1, v1, w1 holds not (v,v1,w,u1) are_COrtm_wrt (x,y) & not (v,v1,u1,w) are_COrtm_wrt (x,y) & (u1,w1,u1,w) are_COrtm_wrt (x,y) implies ex u2 st ((v,v1,v,u2) are_COrtm_wrt (x,y) or (v,v1,u2,v) are_COrtm_wrt (x,y)) & ((u1,w1,u1,u2) are_COrtm_wrt (x,y) or (u1,w1,u2,u1) are_COrtm_wrt (x,y))

    proof

      assume

       A1: Gen (x,y);

      let v, w, u1, v1, w1;

      consider u such that

       A2: v <> u and

       A3: (v,v1,v,u) are_COrtm_wrt (x,y) by A1, Th41;

      assume that

       A4: not (v,v1,w,u1) are_COrtm_wrt (x,y) and

       A5: not (v,v1,u1,w) are_COrtm_wrt (x,y) and

       A6: (u1,w1,u1,w) are_COrtm_wrt (x,y);

      

       A7: not (( Ortm (x,y,v)),( Ortm (x,y,v1))) // (w,u1) by A4;

      

       A8: (( Ortm (x,y,v)),( Ortm (x,y,v1))) // (v,u) by A3;

      

       A9: (( Ortm (x,y,u1)),( Ortm (x,y,w1))) // (u1,w) by A6;

      

       A10: not (( Ortm (x,y,v)),( Ortm (x,y,v1))) // (u1,w) by A5;

      

       A11: (v,u) // (( Ortm (x,y,v)),( Ortm (x,y,v1))) by A8, ANALOAF: 12;

      

       A12: (u1,w) // (( Ortm (x,y,u1)),( Ortm (x,y,w1))) by A9, ANALOAF: 12;

      

       A13: u1 <> w by A7, ANALOAF: 9;

      

       A14: not (v,u) // (u1,w) by A2, A10, A11, ANALOAF: 11;

      

       A15: not (v,u) // (w,u1) by A2, A7, A11, ANALOAF: 11;

       Gen (x,y) implies ex u, v st for w holds ex a, b st ((a * u) + (b * v)) = w

      proof

        assume

         A16: Gen (x,y);

        take x, y;

        thus thesis by A16, ANALMETR:def 1;

      end;

      then

      consider u2 such that

       A17: (v,u) // (v,u2) or (v,u) // (u2,v) and

       A18: (u1,w) // (u1,u2) or (u1,w) // (u2,u1) by A1, A14, A15, ANALOAF: 21;

      (( Ortm (x,y,v)),( Ortm (x,y,v1))) // (v,u2) or (( Ortm (x,y,v)),( Ortm (x,y,v1))) // (u2,v) by A2, A11, A17, ANALOAF: 11;

      then

       A19: (v,v1,v,u2) are_COrtm_wrt (x,y) or (v,v1,u2,v) are_COrtm_wrt (x,y);

      (( Ortm (x,y,u1)),( Ortm (x,y,w1))) // (u1,u2) or (( Ortm (x,y,u1)),( Ortm (x,y,w1))) // (u2,u1) by A12, A13, A18, ANALOAF: 11;

      then (u1,w1,u1,u2) are_COrtm_wrt (x,y) or (u1,w1,u2,u1) are_COrtm_wrt (x,y);

      hence thesis by A19;

    end;

    theorem :: ANALORT:51

     Gen (x,y) implies ex u, v, w st ((u,v,u,w) are_COrtm_wrt (x,y) & for v1, w1 holds ((v1,w1,u,v) are_COrtm_wrt (x,y) implies ( not (v1,w1,u,w) are_COrtm_wrt (x,y) & not (v1,w1,w,u) are_COrtm_wrt (x,y) or v1 = w1)))

    proof

      assume

       A1: Gen (x,y);

      take u = (( 0 * x) + ( 0 * y)), v = ((1 * x) + (1 * y)), w = ((1 * x) + (( - 1) * y));

      

       A2: ( pr1 (x,y,u)) = 0 by A1, Lm6;

      

       A3: ( pr2 (x,y,u)) = 0 by A1, Lm6;

      

       A4: ( pr1 (x,y,v)) = 1 by A1, Lm6;

      ( pr2 (x,y,v)) = 1 by A1, Lm6;

      then

       A5: (( Ortm (x,y,u)),( Ortm (x,y,v))) // (u,w) by A2, A3, A4, ANALOAF: 8;

      for v1, w1 holds ((v1,w1,u,v) are_COrtm_wrt (x,y) implies ( not (v1,w1,u,w) are_COrtm_wrt (x,y) & not (v1,w1,w,u) are_COrtm_wrt (x,y) or v1 = w1))

      proof

        let v1, w1;

        assume (v1,w1,u,v) are_COrtm_wrt (x,y);

        then

         A6: (( Ortm (x,y,v1)),( Ortm (x,y,w1))) // (u,v);

        now

          assume

           A7: v1 <> w1;

          assume (v1,w1,u,w) are_COrtm_wrt (x,y) or (v1,w1,w,u) are_COrtm_wrt (x,y);

          then (( Ortm (x,y,v1)),( Ortm (x,y,w1))) // (u,w) or (( Ortm (x,y,v1)),( Ortm (x,y,w1))) // (w,u);

          then (u,v) // (u,w) or (u,v) // (w,u) by A1, A6, A7, Th6, ANALOAF: 11;

          then

          consider a, b such that

           A8: (a * (v - u)) = (b * (w - u)) and

           A9: a <> 0 or b <> 0 by ANALMETR: 14;

          take a, b;

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

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

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

          then (a * v) = (b * (w - ( 0. V))) by A8, RLVECT_1: 13;

          then

           A10: (a * v) = (b * w) by RLVECT_1: 13;

           A11:

          now

            assume

             A12: a <> 0 ;

            (((a " ) * a) * v) = ((a " ) * (b * w)) by A10, RLVECT_1:def 7;

            then (((a " ) * a) * v) = (((a " ) * b) * w) by RLVECT_1:def 7;

            then (1 * v) = (((a " ) * b) * w) by A12, XCMPLX_0:def 7;

            then (1 * v) = (((((a " ) * b) * 1) * x) + ((((a " ) * b) * ( - 1)) * y)) by Lm2;

            then

             A13: (((1 * 1) * x) + ((1 * 1) * y)) = (((((a " ) * b) * 1) * x) + ((((a " ) * b) * ( - 1)) * y)) by Lm2;

            then (a * 1) = (a * ((a " ) * (b * 1))) by A1, Lm3;

            then

             A14: (a * 1) = ((a * (a " )) * (b * 1));

            1 = (((a " ) * b) * ( - 1)) by A1, A13, Lm3;

            then 1 = (((a " ) * a) * ( - 1)) by A12, A14, XCMPLX_0:def 7;

            hence thesis by A12, XCMPLX_0:def 7;

          end;

          now

            assume

             A15: b <> 0 ;

            (((b " ) * a) * v) = ((b " ) * (b * w)) by A10, RLVECT_1:def 7;

            then (((b " ) * a) * v) = (((b " ) * b) * w) by RLVECT_1:def 7;

            then (((b " ) * a) * v) = (1 * w) by A15, XCMPLX_0:def 7;

            then (((((b " ) * a) * 1) * x) + ((((b " ) * a) * 1) * y)) = (1 * w) by Lm2;

            then

             A16: (((((b " ) * a) * 1) * x) + ((((b " ) * a) * 1) * y)) = (((1 * 1) * x) + ((1 * ( - 1)) * y)) by Lm2;

            then (b * 1) = (b * ((b " ) * (a * 1))) by A1, Lm3;

            then

             A17: (b * 1) = ((b * (b " )) * (a * 1));

            ( - 1) = (((b " ) * a) * 1) by A1, A16, Lm3;

            then ( - 1) = (((b " ) * b) * 1) by A15, A17, XCMPLX_0:def 7;

            hence thesis by A15, XCMPLX_0:def 7;

          end;

          hence thesis by A9, A11;

        end;

        hence thesis;

      end;

      hence thesis by A5;

    end;

    reserve uu,vv for object;

    definition

      let V;

      let x, y;

      :: ANALORT:def5

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

      : Def5: [uu, vv] in it iff ex u1, u2, v1, v2 st uu = [u1, u2] & vv = [v1, v2] & (u1,u2,v1,v2) are_COrte_wrt (x,y);

      existence

      proof

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

        defpred P[ object, object] means ex u1, u2, v1, v2 st $1 = [u1, u2] & $2 = [v1, v2] & (u1,u2,v1,v2) are_COrte_wrt (x,y);

        consider P be Relation of VV, VV such that

         A1: for uu,vv be object holds ( [uu, vv] in P iff uu in VV & vv in VV & P[uu, vv]) from RELSET_1:sch 1;

        take P;

        let uu, vv;

        thus [uu, vv] in P implies ex u1, u2, v1, v2 st uu = [u1, u2] & vv = [v1, v2] & (u1,u2,v1,v2) are_COrte_wrt (x,y) by A1;

        assume

         A2: ex u1, u2, v1, v2 st uu = [u1, u2] & vv = [v1, v2] & (u1,u2,v1,v2) are_COrte_wrt (x,y);

        then

         A3: uu in VV by ZFMISC_1:def 2;

        vv in VV by A2, ZFMISC_1:def 2;

        hence thesis by A1, A2, A3;

      end;

      uniqueness

      proof

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

         A4: [uu, vv] in P iff ex u1, u2, v1, v2 st uu = [u1, u2] & vv = [v1, v2] & (u1,u2,v1,v2) are_COrte_wrt (x,y) and

         A5: [uu, vv] in Q iff ex u1, u2, v1, v2 st uu = [u1, u2] & vv = [v1, v2] & (u1,u2,v1,v2) are_COrte_wrt (x,y);

        for uu,vv be object holds [uu, vv] in P iff [uu, vv] in Q

        proof

          let uu,vv be object;

           [uu, vv] in P iff ex u1, u2, v1, v2 st uu = [u1, u2] & vv = [v1, v2] & (u1,u2,v1,v2) are_COrte_wrt (x,y) by A4;

          hence thesis by A5;

        end;

        hence thesis by RELAT_1:def 2;

      end;

    end

    definition

      let V;

      let x, y;

      :: ANALORT:def6

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

      : Def6: [uu, vv] in it iff ex u1, u2, v1, v2 st uu = [u1, u2] & vv = [v1, v2] & (u1,u2,v1,v2) are_COrtm_wrt (x,y);

      existence

      proof

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

        defpred P[ object, object] means ex u1, u2, v1, v2 st $1 = [u1, u2] & $2 = [v1, v2] & (u1,u2,v1,v2) are_COrtm_wrt (x,y);

        consider P be Relation of VV, VV such that

         A1: for uu,vv be object holds ( [uu, vv] in P iff uu in VV & vv in VV & P[uu, vv]) from RELSET_1:sch 1;

        take P;

        let uu, vv;

        thus [uu, vv] in P implies ex u1, u2, v1, v2 st uu = [u1, u2] & vv = [v1, v2] & (u1,u2,v1,v2) are_COrtm_wrt (x,y) by A1;

        assume

         A2: ex u1, u2, v1, v2 st uu = [u1, u2] & vv = [v1, v2] & (u1,u2,v1,v2) are_COrtm_wrt (x,y);

        then

         A3: uu in VV by ZFMISC_1:def 2;

        vv in VV by A2, ZFMISC_1:def 2;

        hence thesis by A1, A2, A3;

      end;

      uniqueness

      proof

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

         A4: [uu, vv] in P iff ex u1, u2, v1, v2 st uu = [u1, u2] & vv = [v1, v2] & (u1,u2,v1,v2) are_COrtm_wrt (x,y) and

         A5: [uu, vv] in Q iff ex u1, u2, v1, v2 st uu = [u1, u2] & vv = [v1, v2] & (u1,u2,v1,v2) are_COrtm_wrt (x,y);

        for uu,vv be object holds [uu, vv] in P iff [uu, vv] in Q

        proof

          let uu,vv be object;

           [uu, vv] in P iff ex u1, u2, v1, v2 st uu = [u1, u2] & vv = [v1, v2] & (u1,u2,v1,v2) are_COrtm_wrt (x,y) by A4;

          hence thesis by A5;

        end;

        hence thesis by RELAT_1:def 2;

      end;

    end

    definition

      let V;

      let x, y;

      :: ANALORT:def7

      func CESpace (V,x,y) -> strict OrtStr equals OrtStr (# the carrier of V, ( CORTE (V,x,y)) #);

      correctness ;

    end

    registration

      let V;

      let x, y;

      cluster ( CESpace (V,x,y)) -> non empty;

      coherence ;

    end

    definition

      let V;

      let x, y;

      :: ANALORT:def8

      func CMSpace (V,x,y) -> strict OrtStr equals OrtStr (# the carrier of V, ( CORTM (V,x,y)) #);

      correctness ;

    end

    registration

      let V;

      let x, y;

      cluster ( CMSpace (V,x,y)) -> non empty;

      coherence ;

    end

    theorem :: ANALORT:52

    uu is Element of ( CESpace (V,x,y)) iff uu is VECTOR of V;

    theorem :: ANALORT:53

    uu is Element of ( CMSpace (V,x,y)) iff uu is VECTOR of V;

    reserve p,q,r,s for Element of ( CESpace (V,x,y));

    theorem :: ANALORT:54

    u = p & v = q & u1 = r & v1 = s implies ((p,q) _|_ (r,s) iff (u,v,u1,v1) are_COrte_wrt (x,y))

    proof

      assume that

       A1: u = p and

       A2: v = q and

       A3: u1 = r and

       A4: v1 = s;

      

       A5: (p,q) _|_ (r,s) implies (u,v,u1,v1) are_COrte_wrt (x,y)

      proof

        assume (p,q) _|_ (r,s);

        then [ [p, q], [r, s]] in the orthogonality of ( CESpace (V,x,y)) by ANALMETR:def 5;

        then

        consider u19,u29,v19,v29 be VECTOR of V such that

         A6: [u, v] = [u19, u29] and

         A7: [u1, v1] = [v19, v29] and

         A8: (u19,u29,v19,v29) are_COrte_wrt (x,y) by A1, A2, A3, A4, Def5;

        

         A9: u = u19 by A6, XTUPLE_0: 1;

        

         A10: v = u29 by A6, XTUPLE_0: 1;

        u1 = v19 by A7, XTUPLE_0: 1;

        hence thesis by A7, A8, A9, A10, XTUPLE_0: 1;

      end;

      (u,v,u1,v1) are_COrte_wrt (x,y) implies (p,q) _|_ (r,s)

      proof

        assume (u,v,u1,v1) are_COrte_wrt (x,y);

        then [ [u, v], [u1, v1]] in the orthogonality of OrtStr (# the carrier of V, ( CORTE (V,x,y)) #) by Def5;

        hence thesis by A1, A2, A3, A4, ANALMETR:def 5;

      end;

      hence thesis by A5;

    end;

    reserve p,q,r,s for Element of ( CMSpace (V,x,y));

    theorem :: ANALORT:55

    u = p & v = q & u1 = r & v1 = s implies ((p,q) _|_ (r,s) iff (u,v,u1,v1) are_COrtm_wrt (x,y))

    proof

      assume that

       A1: u = p and

       A2: v = q and

       A3: u1 = r and

       A4: v1 = s;

      

       A5: (p,q) _|_ (r,s) implies (u,v,u1,v1) are_COrtm_wrt (x,y)

      proof

        assume (p,q) _|_ (r,s);

        then [ [p, q], [r, s]] in the orthogonality of ( CMSpace (V,x,y)) by ANALMETR:def 5;

        then

        consider u19,u29,v19,v29 be VECTOR of V such that

         A6: [u, v] = [u19, u29] and

         A7: [u1, v1] = [v19, v29] and

         A8: (u19,u29,v19,v29) are_COrtm_wrt (x,y) by A1, A2, A3, A4, Def6;

        

         A9: u = u19 by A6, XTUPLE_0: 1;

        

         A10: v = u29 by A6, XTUPLE_0: 1;

        u1 = v19 by A7, XTUPLE_0: 1;

        hence thesis by A7, A8, A9, A10, XTUPLE_0: 1;

      end;

      (u,v,u1,v1) are_COrtm_wrt (x,y) implies (p,q) _|_ (r,s)

      proof

        assume (u,v,u1,v1) are_COrtm_wrt (x,y);

        then [ [u, v], [u1, v1]] in the orthogonality of OrtStr (# the carrier of V, ( CORTM (V,x,y)) #) by Def6;

        hence thesis by A1, A2, A3, A4, ANALMETR:def 5;

      end;

      hence thesis by A5;

    end;