analoaf.miz



    begin

    reserve V for RealLinearSpace;

    reserve p,q,u,v,w,y for VECTOR of V;

    reserve a,b,c,d for Real;

    definition

      let V;

      let u, v, w, y;

      :: ANALOAF:def1

      pred u,v // w,y means u = v or w = y or ex a, b st 0 < a & 0 < b & (a * (v - u)) = (b * (y - w));

    end

    theorem :: ANALOAF:1

    

     Th1: ((w - v) + (v - u)) = (w - u)

    proof

      

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

      .= (w - ((v - v) + u)) by RLVECT_1: 29

      .= (w - (( 0. V) + u)) by RLVECT_1: 15

      .= (w - u) by RLVECT_1: 4;

    end;

    theorem :: ANALOAF:2

    

     Th2: (y + u) = (v + w) implies (y - w) = (v - u)

    proof

      assume

       A1: (y + u) = (v + w);

      

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

      .= ((y + (u - u)) - w) by RLVECT_1: 15

      .= (((v + w) + ( - u)) - w) by A1, RLVECT_1:def 3

      .= (( - u) + ((v + w) - w)) by RLVECT_1:def 3

      .= (v - u) by RLSUB_2: 61;

    end;

    theorem :: ANALOAF:3

    

     Th3: (a * (u - v)) = ( - (a * (v - u)))

    proof

      ((a * (v - u)) + (a * (u - v))) = ((a * (v - u)) + (a * ( - (v - u)))) by RLVECT_1: 33

      .= ((a * (v - u)) - (a * (v - u))) by RLVECT_1: 25

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

      hence thesis by RLVECT_1:def 10;

    end;

    theorem :: ANALOAF:4

    

     Th4: ((a - b) * (u - v)) = ((b - a) * (v - u))

    proof

      

      thus ((a - b) * (u - v)) = (( - (b - a)) * ( - (v - u))) by RLVECT_1: 33

      .= ((b - a) * (v - u)) by RLVECT_1: 26;

    end;

    theorem :: ANALOAF:5

    

     Th5: a <> 0 & (a * u) = v implies u = ((a " ) * v)

    proof

      assume that

       A1: a <> 0 and

       A2: (a * u) = v;

      

      thus u = (1 * u) by RLVECT_1:def 8

      .= (((a " ) * a) * u) by A1, XCMPLX_0:def 7

      .= ((a " ) * v) by A2, RLVECT_1:def 7;

    end;

    theorem :: ANALOAF:6

    

     Th6: (a <> 0 & (a * u) = v implies u = ((a " ) * v)) & (a <> 0 & u = ((a " ) * v) implies (a * u) = v)

    proof

      now

        assume a <> 0 & u = ((a " ) * v);

        

        hence v = (((a " ) " ) * u) by Th5, XCMPLX_1: 202

        .= (a * u);

      end;

      hence thesis by Th5;

    end;

    theorem :: ANALOAF:7

    (u,v) // (w,y) & u <> v & w <> y implies ex a, b st (a * (v - u)) = (b * (y - w)) & 0 < a & 0 < b;

    reconsider jj = 1 as Real;

    theorem :: ANALOAF:8

    

     Th8: (u,v) // (u,v)

    proof

      (jj * (v - u)) = (jj * (v - u));

      hence thesis;

    end;

    theorem :: ANALOAF:9

    (u,v) // (w,w) & (u,u) // (v,w);

    theorem :: ANALOAF:10

    

     Th10: (u,v) // (v,u) implies u = v

    proof

      assume

       A1: (u,v) // (v,u);

      assume

       A2: u <> v;

      then

      consider a, b such that

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

       A4: 0 < a & 0 < b by A1;

      (a * (v - u)) = ( - (b * (v - u))) by A3, Th3;

      then ((b * (v - u)) + (a * (v - u))) = ( 0. V) by RLVECT_1: 5;

      then ((b + a) * (v - u)) = ( 0. V) by RLVECT_1:def 6;

      then (v - u) = ( 0. V) or (b + a) = 0 by RLVECT_1: 11;

      then ( 0. V) = (( - u) + v) by A4;

      

      then v = ( - ( - u)) by RLVECT_1:def 10

      .= u by RLVECT_1: 17;

      hence contradiction by A2;

    end;

    theorem :: ANALOAF:11

    

     Th11: p <> q & (p,q) // (u,v) & (p,q) // (w,y) implies (u,v) // (w,y)

    proof

      assume that

       A1: p <> q and

       A2: (p,q) // (u,v) and

       A3: (p,q) // (w,y);

      now

        assume that

         A4: u <> v and

         A5: w <> y;

        consider a, b such that

         A6: (a * (q - p)) = (b * (v - u)) and

         A7: 0 < a and

         A8: 0 < b by A1, A2, A4;

         0 < (a " ) by A7;

        then

         A9: 0 < ((a " ) * b) by A8, XREAL_1: 129;

        consider c, d such that

         A10: (c * (q - p)) = (d * (y - w)) and

         A11: 0 < c and

         A12: 0 < d by A1, A3, A5;

        

         A13: (q - p) = ((c " ) * (d * (y - w))) by A10, A11, Th6

        .= (((c " ) * d) * (y - w)) by RLVECT_1:def 7;

         0 < (c " ) by A11;

        then

         A14: 0 < ((c " ) * d) by A12, XREAL_1: 129;

        (q - p) = ((a " ) * (b * (v - u))) by A6, A7, Th6

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

        hence thesis by A13, A9, A14;

      end;

      hence thesis;

    end;

    theorem :: ANALOAF:12

    

     Th12: (u,v) // (w,y) implies (v,u) // (y,w) & (w,y) // (u,v)

    proof

      assume

       A1: (u,v) // (w,y);

      now

        assume u <> v & w <> y;

        then

        consider a, b such that

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

         A3: 0 < a & 0 < b by A1;

        (a * (u - v)) = ( - (b * (y - w))) by A2, Th3

        .= (b * (w - y)) by Th3;

        hence thesis by A2, A3;

      end;

      hence thesis;

    end;

    theorem :: ANALOAF:13

    

     Th13: (u,v) // (v,w) implies (u,v) // (u,w)

    proof

      assume

       A1: (u,v) // (v,w);

      now

        assume u <> v & v <> w;

        then

        consider a, b such that

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

         A3: 0 < a and

         A4: 0 < b by A1;

        

         A5: 0 < (a + b) by A3, A4;

        (b * (w - u)) = (b * ((w - v) + (v - u))) by Th1

        .= ((a * (v - u)) + (b * (v - u))) by A2, RLVECT_1:def 5

        .= ((a + b) * (v - u)) by RLVECT_1:def 6;

        hence thesis by A4, A5;

      end;

      hence thesis by Th8;

    end;

    theorem :: ANALOAF:14

    

     Th14: (u,v) // (u,w) implies (u,v) // (v,w) or (u,w) // (w,v)

    proof

      assume

       A1: (u,v) // (u,w);

      now

        assume u <> v & u <> w;

        then

        consider a, b such that

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

         A3: 0 < a and

         A4: 0 < b by A1;

        (w - v) = ((w - u) + (u - v)) by Th1

        .= ((w - u) - (v - u)) by RLVECT_1: 33;

        

        then

         A5: (a * (w - v)) = ((a * (w - u)) - (b * (w - u))) by A2, RLVECT_1: 34

        .= ((a - b) * (w - u)) by RLVECT_1: 35

        .= ((b - a) * (u - w)) by Th4;

        (v - w) = ((v - u) + (u - w)) by Th1

        .= ((v - u) - (w - u)) by RLVECT_1: 33;

        

        then

         A6: (b * (v - w)) = ((b * (v - u)) - (a * (v - u))) by A2, RLVECT_1: 34

        .= ((b - a) * (v - u)) by RLVECT_1: 35

        .= ((a - b) * (u - v)) by Th4;

         A7:

        now

          assume a <> b;

          then 0 < (a - b) or 0 < (b - a) by XREAL_1: 55;

          then (v,u) // (w,v) or (w,u) // (v,w) by A3, A4, A6, A5;

          hence thesis by Th12;

        end;

        now

          assume a = b;

          then (( - u) + v) = (( - u) + w) by A2, A3, RLVECT_1: 36;

          then v = w by RLVECT_1: 8;

          hence thesis;

        end;

        hence thesis by A7;

      end;

      hence thesis;

    end;

    theorem :: ANALOAF:15

    

     Th15: (v - u) = (y - w) implies (u,v) // (w,y)

    proof

      assume (v - u) = (y - w);

      then (jj * (v - u)) = (jj * (y - w));

      hence thesis;

    end;

    theorem :: ANALOAF:16

    

     Th16: y = ((v + w) - u) implies (u,v) // (w,y) & (u,w) // (v,y)

    proof

      set y = ((v + w) - u);

      (y + u) = (v + w) by RLSUB_2: 61;

      then (y - v) = (w - u) & (y - w) = (v - u) by Th2;

      hence thesis by Th15;

    end;

    theorem :: ANALOAF:17

    

     Th17: (ex p, q st p <> q) implies for u, v, w holds ex y st (u,v) // (w,y) & (u,w) // (v,y) & v <> y

    proof

      given p, q such that

       A1: p <> q;

      let u, v, w;

       A2:

      now

        assume

         A3: u <> w;

        take y = ((v + w) - u);

         A4:

        now

          assume v = y;

          then v = (v + (w - u)) by RLVECT_1:def 3;

          then (w - u) = ( 0. V) by RLVECT_1: 9;

          hence contradiction by A3, RLVECT_1: 21;

        end;

        (u,v) // (w,y) & (u,w) // (v,y) by Th16;

        hence thesis by A4;

      end;

      now

        assume

         A5: u = w;

         A6:

        now

          assume u = v;

          then

           A7: (u,v) // (w,p) & (u,v) // (w,q);

          

           A8: v <> p or v <> q by A1;

          (u,w) // (v,p) & (u,w) // (v,q) by A5;

          hence thesis by A8, A7;

        end;

        (u,v) // (w,u) & (u,w) // (v,u) by A5;

        hence thesis by A6;

      end;

      hence thesis by A2;

    end;

    theorem :: ANALOAF:18

    

     Th18: p <> v & (v,p) // (p,w) implies ex y st (u,p) // (p,y) & (u,v) // (w,y)

    proof

      assume

       A1: p <> v & (v,p) // (p,w);

       A2:

      now

        assume p <> w;

        then

        consider a, b such that

         A3: (a * (p - v)) = (b * (w - p)) and

         A4: 0 < a and

         A5: 0 < b by A1;

        set y = ((((b " ) * a) * (p - u)) + p);

        

         A6: (y - p) = (((b " ) * a) * (p - u)) by RLSUB_2: 61

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

        

         A7: (y - w) = ((y - p) + (p - w)) by Th1

        .= ((y - p) - (w - p)) by RLVECT_1: 33;

        (v - u) = ((p - u) + (v - p)) by Th1

        .= ((p - u) - (p - v)) by RLVECT_1: 33;

        

        then (a * (v - u)) = ((a * (p - u)) - (a * (p - v))) by RLVECT_1: 34

        .= ((b * (y - p)) - (b * (w - p))) by A3, A5, A6, Th6

        .= (b * (y - w)) by A7, RLVECT_1: 34;

        then

         A8: (u,v) // (w,y) by A4, A5;

         0 < (b " ) by A5;

        then

         A9: 0 < ((b " ) * a) by A4, XREAL_1: 129;

        (jj * (y - p)) = (y - p) by RLVECT_1:def 8

        .= (((b " ) * a) * (p - u)) by RLSUB_2: 61;

        then (u,p) // (p,y) by A9;

        hence thesis by A8;

      end;

      now

        assume

         A10: p = w;

        take y = p;

        thus (u,p) // (p,y) & (u,v) // (w,y) by A10;

      end;

      hence thesis by A2;

    end;

    theorem :: ANALOAF:19

    

     Th19: (for a, b st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 ) implies u <> v & u <> ( 0. V) & v <> ( 0. V)

    proof

      assume

       A1: for a, b st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 ;

      thus u <> v

      proof

        assume u = v;

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

        then ((1 * u) + ( - v)) = ( 0. V) by RLVECT_1:def 8;

        then ((1 * u) + (( - jj) * v)) = ( 0. V) by RLVECT_1: 16;

        hence contradiction by A1;

      end;

      thus u <> ( 0. V)

      proof

        assume u = ( 0. V);

        then (1 * u) = ( 0. V) by RLVECT_1: 10;

        then ((1 * u) + ( 0. V)) = ( 0. V) by RLVECT_1: 4;

        then ((jj * u) + ( 0 * v)) = ( 0. V) by RLVECT_1: 10;

        hence contradiction by A1;

      end;

      thus v <> ( 0. V)

      proof

        assume v = ( 0. V);

        then (1 * v) = ( 0. V) by RLVECT_1: 10;

        then (( 0. V) + (1 * v)) = ( 0. V) by RLVECT_1: 4;

        then (( 0 * u) + (jj * v)) = ( 0. V) by RLVECT_1: 10;

        hence contradiction by A1;

      end;

    end;

    theorem :: ANALOAF:20

    

     Th20: (ex u, v st (for a, b st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 )) implies ex u, v, w, y st not (u,v) // (w,y) & not (u,v) // (y,w)

    proof

      given u, v such that

       A1: for a, b st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 ;

      

       A2: u <> ( 0. V) & v <> ( 0. V) by A1, Th19;

      

       A3: not (( 0. V),u) // (v,( 0. V))

      proof

         A4:

        now

          given a, b such that

           A5: 0 < a and 0 < b and

           A6: (a * (u - ( 0. V))) = (b * (( 0. V) - v));

          (a * u) = (a * (u - ( 0. V))) & (b * (( 0. V) - v)) = (b * ( - v)) by RLVECT_1: 13, RLVECT_1: 14;

          then (a * u) = ( - (b * v)) by A6, RLVECT_1: 25;

          then ((a * u) + (b * v)) = ( 0. V) by RLVECT_1: 5;

          hence contradiction by A1, A5;

        end;

        assume (( 0. V),u) // (v,( 0. V));

        hence contradiction by A2, A4;

      end;

       not (( 0. V),u) // (( 0. V),v)

      proof

         A7:

        now

          given a, b such that

           A8: 0 < a and 0 < b and

           A9: (a * (u - ( 0. V))) = (b * (v - ( 0. V)));

          (a * u) = (a * (u - ( 0. V))) & (b * (v - ( 0. V))) = (b * v) by RLVECT_1: 13;

          

          then ( 0. V) = ((a * u) - (b * v)) by A9, RLVECT_1: 15

          .= ((a * u) + (b * ( - v))) by RLVECT_1: 25

          .= ((a * u) + (( - b) * v)) by RLVECT_1: 24;

          hence contradiction by A1, A8;

        end;

        assume (( 0. V),u) // (( 0. V),v);

        hence contradiction by A2, A7;

      end;

      hence thesis by A3;

    end;

    

     Lm1: (a * (v - u)) = (b * (w - y)) & (a <> 0 or b <> 0 ) implies (u,v) // (w,y) or (u,v) // (y,w)

    proof

      assume that

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

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

       A3:

      now

        assume

         A4: b = 0 ;

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

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

        then u = v by RLVECT_1: 21;

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

      end;

       A5:

      now

         A6:

        now

          

           A7: (a * (v - u)) = ( - ( - (b * (w - y)))) by A1, RLVECT_1: 17

          .= ( - (b * ( - (w - y)))) by RLVECT_1: 25

          .= ( - (b * (y - w))) by RLVECT_1: 33

          .= (b * ( - (y - w))) by RLVECT_1: 25

          .= (( - b) * (y - w)) by RLVECT_1: 24;

          assume that

           A8: 0 < a and

           A9: b < 0 ;

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

          hence (u,v) // (w,y) by A8, A7;

        end;

         A10:

        now

          

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

          .= ( - (b * (w - y))) by A1, RLVECT_1: 25

          .= (b * ( - (w - y))) by RLVECT_1: 25

          .= (b * (y - w)) by RLVECT_1: 33;

          assume that

           A12: a < 0 and

           A13: 0 < b;

           0 < ( - a) by A12, XREAL_1: 58;

          hence (u,v) // (w,y) by A13, A11;

        end;

         A14:

        now

          assume a < 0 & b < 0 ;

          then

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

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

          .= ( - (b * (w - y))) by A1, RLVECT_1: 25

          .= (b * ( - (w - y))) by RLVECT_1: 25

          .= (( - b) * (w - y)) by RLVECT_1: 24;

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

        end;

        assume a <> 0 & b <> 0 ;

        hence thesis by A1, A14, A10, A6;

      end;

      now

        assume

         A16: a = 0 ;

        then ( 0. V) = (b * (w - y)) by A1, RLVECT_1: 10;

        then (w - y) = ( 0. V) by A2, A16, RLVECT_1: 11;

        then w = y by RLVECT_1: 21;

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

      end;

      hence thesis by A3, A5;

    end;

    theorem :: ANALOAF:21

    

     Th21: (ex p, q st (for w holds ex a, b st ((a * p) + (b * q)) = w)) implies for u, v, w, y st not (u,v) // (w,y) & not (u,v) // (y,w) holds ex z be VECTOR of V st ((u,v) // (u,z) or (u,v) // (z,u)) & ((w,y) // (w,z) or (w,y) // (z,w))

    proof

      given p, q such that

       A1: for w holds ex a, b st ((a * p) + (b * q)) = w;

      let u, v, w, y such that

       A2: not (u,v) // (w,y) and

       A3: not (u,v) // (y,w);

      consider r1,s1 be Real such that

       A4: ((r1 * p) + (s1 * q)) = (v - u) by A1;

      consider r2,s2 be Real such that

       A5: ((r2 * p) + (s2 * q)) = (y - w) by A1;

      set r = ((r1 * s2) - (r2 * s1));

       A6:

      now

        assume

         A7: r = 0 ;

         A8:

        now

          assume that

           A9: r1 <> 0 and

           A10: r2 = 0 ;

          s2 <> 0

          proof

            assume s2 = 0 ;

            

            then (y - w) = (( 0. V) + ( 0 * q)) by A5, A10, RLVECT_1: 10

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

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

            then y = w by RLVECT_1: 21;

            hence contradiction by A2;

          end;

          hence contradiction by A7, A9, A10, XCMPLX_1: 6;

        end;

         A11:

        now

          assume

           A12: r1 = 0 ;

          

           A13: s1 <> 0

          proof

            assume s1 = 0 ;

            

            then (v - u) = (( 0. V) + ( 0 * q)) by A4, A12, RLVECT_1: 10

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

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

            then u = v by RLVECT_1: 21;

            hence contradiction by A2;

          end;

          then

           A14: r2 = 0 by A7, A12, XCMPLX_1: 6;

          

           A15: s2 <> 0

          proof

            assume s2 = 0 ;

            

            then (y - w) = (( 0. V) + ( 0 * q)) by A5, A14, RLVECT_1: 10

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

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

            then y = w by RLVECT_1: 21;

            hence contradiction by A2;

          end;

          (y - w) = (( 0. V) + (s2 * q)) by A5, A14, RLVECT_1: 10

          .= (s2 * q) by RLVECT_1: 4;

          

          then

           A16: ((s2 " ) * (y - w)) = (((s2 " ) * s2) * q) by RLVECT_1:def 7

          .= (1 * q) by A15, XCMPLX_0:def 7

          .= q by RLVECT_1:def 8;

          (v - u) = (( 0. V) + (s1 * q)) by A4, A12, RLVECT_1: 10

          .= (s1 * q) by RLVECT_1: 4;

          

          then

           A17: ((s1 " ) * (v - u)) = (((s1 " ) * s1) * q) by RLVECT_1:def 7

          .= (1 * q) by A13, XCMPLX_0:def 7

          .= q by RLVECT_1:def 8;

          (s1 " ) <> 0 by A13, XCMPLX_1: 202;

          hence contradiction by A2, A3, A17, A16, Lm1;

        end;

         A18:

        now

          assume that

           A19: r1 <> 0 and

           A20: r2 <> 0 and

           A21: s1 = 0 ;

          (v - u) = ((r1 * p) + ( 0. V)) by A4, A21, RLVECT_1: 10

          .= (r1 * p) by RLVECT_1: 4;

          

          then

           A22: ((r1 " ) * (v - u)) = (((r1 " ) * r1) * p) by RLVECT_1:def 7

          .= (1 * p) by A19, XCMPLX_0:def 7

          .= p by RLVECT_1:def 8;

          s2 = 0 by A7, A19, A21, XCMPLX_1: 6;

          

          then (y - w) = ((r2 * p) + ( 0. V)) by A5, RLVECT_1: 10

          .= (r2 * p) by RLVECT_1: 4;

          

          then

           A23: ((r2 " ) * (y - w)) = (((r2 " ) * r2) * p) by RLVECT_1:def 7

          .= (1 * p) by A20, XCMPLX_0:def 7

          .= p by RLVECT_1:def 8;

          (r1 " ) <> 0 by A19, XCMPLX_1: 202;

          hence contradiction by A2, A3, A22, A23, Lm1;

        end;

        now

          assume that

           A24: r1 <> 0 and r2 <> 0 and s1 <> 0 and s2 <> 0 ;

          (r2 * (v - u)) = ((r2 * (r1 * p)) + (r2 * (s1 * q))) by A4, RLVECT_1:def 5

          .= (((r2 * r1) * p) + (r2 * (s1 * q))) by RLVECT_1:def 7

          .= (((r1 * r2) * p) + ((r1 * s2) * q)) by A7, RLVECT_1:def 7

          .= ((r1 * (r2 * p)) + ((r1 * s2) * q)) by RLVECT_1:def 7

          .= ((r1 * (r2 * p)) + (r1 * (s2 * q))) by RLVECT_1:def 7

          .= (r1 * (y - w)) by A5, RLVECT_1:def 5;

          hence contradiction by A2, A3, A24, Lm1;

        end;

        hence contradiction by A7, A11, A8, A18, XCMPLX_1: 6;

      end;

      consider r3,s3 be Real such that

       A25: ((r3 * p) + (s3 * q)) = (u - w) by A1;

      set a = ((r2 * s3) - (r3 * s2)), b = ((r1 * s3) - (r3 * s1));

      

       A26: (b * r2) = ((r1 * a) + (r3 * r));

      set z = (u + (((r " ) * a) * (v - u)));

      

       A27: (r * (z - u)) = ((r * z) - (r * u)) by RLVECT_1: 34

      .= (((r * u) + (r * (((r " ) * a) * (v - u)))) - (r * u)) by RLVECT_1:def 5

      .= (((r * u) + ((r * ((r " ) * a)) * (v - u))) - (r * u)) by RLVECT_1:def 7

      .= (((r * u) + (((r * (r " )) * a) * (v - u))) - (r * u))

      .= (((r * u) + ((1 * a) * (v - u))) - (r * u)) by A6, XCMPLX_0:def 7

      .= ((a * (v - u)) + ((r * u) - (r * u))) by RLVECT_1:def 3

      .= ((a * (v - u)) + ( 0. V)) by RLVECT_1: 15

      .= (a * (v - u)) by RLVECT_1: 4;

      

       A28: (r * (z - w)) = ((r * z) - (r * w)) by RLVECT_1: 34

      .= (((r * u) + (r * (((r " ) * a) * (v - u)))) - (r * w)) by RLVECT_1:def 5

      .= (((r * u) + ((r * ((r " ) * a)) * (v - u))) - (r * w)) by RLVECT_1:def 7

      .= (((r * u) + (((r * (r " )) * a) * (v - u))) - (r * w))

      .= (((r * u) + ((1 * a) * (v - u))) - (r * w)) by A6, XCMPLX_0:def 7

      .= ((a * (v - u)) + ((r * u) - (r * w))) by RLVECT_1:def 3

      .= ((a * ((r1 * p) + (s1 * q))) + (r * ((r3 * p) + (s3 * q)))) by A4, A25, RLVECT_1: 34

      .= (((a * (r1 * p)) + (a * (s1 * q))) + (r * ((r3 * p) + (s3 * q)))) by RLVECT_1:def 5

      .= (((a * (r1 * p)) + (a * (s1 * q))) + ((r * (r3 * p)) + (r * (s3 * q)))) by RLVECT_1:def 5

      .= ((((a * r1) * p) + (a * (s1 * q))) + ((r * (r3 * p)) + (r * (s3 * q)))) by RLVECT_1:def 7

      .= ((((a * r1) * p) + ((a * s1) * q)) + ((r * (r3 * p)) + (r * (s3 * q)))) by RLVECT_1:def 7

      .= ((((a * r1) * p) + ((a * s1) * q)) + (((r * r3) * p) + (r * (s3 * q)))) by RLVECT_1:def 7

      .= ((((a * r1) * p) + ((a * s1) * q)) + (((r * s3) * q) + ((r * r3) * p))) by RLVECT_1:def 7

      .= (((((a * r1) * p) + ((a * s1) * q)) + ((r * s3) * q)) + ((r * r3) * p)) by RLVECT_1:def 3

      .= (((((a * s1) * q) + ((r * s3) * q)) + ((a * r1) * p)) + ((r * r3) * p)) by RLVECT_1:def 3

      .= ((((a * s1) * q) + ((r * s3) * q)) + (((a * r1) * p) + ((r * r3) * p))) by RLVECT_1:def 3

      .= ((((a * s1) + (r * s3)) * q) + (((a * r1) * p) + ((r * r3) * p))) by RLVECT_1:def 6

      .= (((b * s2) * q) + ((b * r2) * p)) by A26, RLVECT_1:def 6

      .= ((b * (s2 * q)) + ((b * r2) * p)) by RLVECT_1:def 7

      .= ((b * (s2 * q)) + (b * (r2 * p))) by RLVECT_1:def 7

      .= (b * (y - w)) by A5, RLVECT_1:def 5;

      

       A29: (b * s2) = ((s1 * a) + (s3 * r));

      per cases ;

        suppose that

         A30: a = 0 and

         A31: b <> 0 ;

        (r * (z - u)) = ( 0. V) by A27, A30, RLVECT_1: 10;

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

        then z = u by RLVECT_1: 21;

        then

         A32: (u,v) // (u,z);

        (w,y) // (w,z) or (w,y) // (z,w) by A28, A31, Lm1;

        hence thesis by A32;

      end;

        suppose a = 0 & b = 0 ;

        then r3 = 0 & s3 = 0 by A6, A26, A29, XCMPLX_1: 6;

        then (( 0. V) + ( 0 * q)) = (u - w) by A25, RLVECT_1: 10;

        then (( 0. V) + ( 0. V)) = (u - w) by RLVECT_1: 10;

        then ( 0. V) = (u - w) by RLVECT_1: 4;

        then u = w by RLVECT_1: 21;

        then

         A33: (w,y) // (w,u);

        (u,v) // (u,u);

        hence thesis by A33;

      end;

        suppose that

         A34: a <> 0 and

         A35: b = 0 ;

        (r * (z - w)) = ( 0. V) by A28, A35, RLVECT_1: 10;

        then (z - w) = ( 0. V) by A6, RLVECT_1: 11;

        then z = w by RLVECT_1: 21;

        then

         A36: (w,y) // (w,z);

        (u,v) // (u,z) or (u,v) // (z,u) by A27, A34, Lm1;

        hence thesis by A36;

      end;

        suppose that

         A37: a <> 0 and

         A38: b <> 0 ;

        

         A39: (w,y) // (w,z) or (w,y) // (z,w) by A28, A38, Lm1;

        (u,v) // (u,z) or (u,v) // (z,u) by A27, A37, Lm1;

        hence thesis by A39;

      end;

    end;

    definition

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

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

       attr strict strict;

    end

    registration

      cluster non trivial strict for AffinStruct;

      existence

      proof

        set A = the non trivial set, R = the Relation of [:A, A:];

        take AffinStruct (# A, R #);

        thus thesis;

      end;

    end

    reserve AS for non empty AffinStruct;

    reserve a,b,c,d for Element of AS;

    reserve x,z for object;

    definition

      let AS, a, b, c, d;

      :: ANALOAF:def2

      pred a,b // c,d means [ [a, b], [c, d]] in the CONGR of AS;

    end

    definition

      let V;

      :: ANALOAF:def3

      func DirPar (V) -> Relation of [:the carrier of V, the carrier of V:] means

      : Def3: [x, z] in it iff ex u, v, w, y st x = [u, v] & z = [w, y] & (u,v) // (w,y);

      existence

      proof

        defpred P[ object, object] means ex u, v, w, y st $1 = [u, v] & $2 = [w, y] & (u,v) // (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;

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

        assume ex u, v, w, y st x = [u, v] & z = [w, y] & (u,v) // (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: [x, z] in P iff ex u, v, w, y st x = [u, v] & z = [w, y] & (u,v) // (w,y) and

         A3: [x, z] in Q iff ex u, v, w, y st x = [u, v] & z = [w, y] & (u,v) // (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, v, w, y st x = [u, v] & z = [w, y] & (u,v) // (w,y) by A2;

          hence thesis by A3;

        end;

        hence thesis by RELAT_1:def 2;

      end;

    end

    theorem :: ANALOAF:22

    

     Th22: [ [u, v], [w, y]] in ( DirPar V) iff (u,v) // (w,y)

    proof

      thus [ [u, v], [w, y]] in ( DirPar V) implies (u,v) // (w,y)

      proof

        assume [ [u, v], [w, y]] in ( DirPar V);

        then

        consider u9,v9,w9,y9 be VECTOR of V such that

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

         A2: [w, y] = [w9, y9] and

         A3: (u9,v9) // (w9,y9) by Def3;

        

         A4: w = w9 by A2, XTUPLE_0: 1;

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

        hence thesis by A2, A3, A4, XTUPLE_0: 1;

      end;

      thus thesis by Def3;

    end;

    definition

      let V;

      :: ANALOAF:def4

      func OASpace (V) -> strict AffinStruct equals AffinStruct (# the carrier of V, ( DirPar V) #);

      correctness ;

    end

    registration

      let V;

      cluster ( OASpace V) -> non empty;

      coherence ;

    end

    theorem :: ANALOAF:23

    

     Th23: (ex u, v st for a,b be Real st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 ) implies (ex a,b be Element of ( OASpace V) st a <> b) & (for a,b,c,d,p,q,r,s be Element of ( OASpace V) holds (a,b) // (c,c) & ((a,b) // (b,a) implies a = b) & (a <> b & (a,b) // (p,q) & (a,b) // (r,s) implies (p,q) // (r,s)) & ((a,b) // (c,d) implies (b,a) // (d,c)) & ((a,b) // (b,c) implies (a,b) // (a,c)) & ((a,b) // (a,c) implies (a,b) // (b,c) or (a,c) // (c,b))) & (ex a,b,c,d be Element of ( OASpace V) st not (a,b) // (c,d) & not (a,b) // (d,c)) & (for a,b,c be Element of ( OASpace V) holds ex d be Element of ( OASpace V) st (a,b) // (c,d) & (a,c) // (b,d) & b <> d) & for p,a,b,c be Element of ( OASpace V) st p <> b & (b,p) // (p,c) holds ex d be Element of ( OASpace V) st (a,p) // (p,d) & (a,b) // (c,d)

    proof

      given u, v such that

       A1: for a,b be Real st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 ;

      set S = ( OASpace V);

      

       A2: u <> v by A1, Th19;

      hence ex a,b be Element of S st a <> b;

      thus for a,b,c,d,p,q,r,s be Element of S holds (a,b) // (c,c) & ((a,b) // (b,a) implies a = b) & (a <> b & (a,b) // (p,q) & (a,b) // (r,s) implies (p,q) // (r,s)) & ((a,b) // (c,d) implies (b,a) // (d,c)) & ((a,b) // (b,c) implies (a,b) // (a,c)) & ((a,b) // (a,c) implies (a,b) // (b,c) or (a,c) // (c,b))

      proof

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

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

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

        hence [ [a, b], [c, c]] in the CONGR of S by Def3;

        thus (a,b) // (b,a) implies a = b by Th22, Th10;

        thus a <> b & (a,b) // (p,q) & (a,b) // (r,s) implies (p,q) // (r,s)

        proof

          assume that

           A3: a <> b and

           A4: [ [a, b], [p, q]] in the CONGR of S & [ [a, b], [r, s]] in the CONGR of S;

          (a9,b9) // (p9,q9) & (a9,b9) // (r9,s9) by A4, Th22;

          then (p9,q9) // (r9,s9) by A3, Th11;

          then [ [p, q], [r, s]] in the CONGR of S by Th22;

          hence thesis;

        end;

        thus (a,b) // (c,d) implies (b,a) // (d,c)

        proof

          assume [ [a, b], [c, d]] in the CONGR of S;

          then (a9,b9) // (c9,d9) by Th22;

          then (b9,a9) // (d9,c9) by Th12;

          then [ [b, a], [d, c]] in the CONGR of S by Th22;

          hence thesis;

        end;

        thus (a,b) // (b,c) implies (a,b) // (a,c)

        proof

          assume [ [a, b], [b, c]] in the CONGR of S;

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

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

          then [ [a, b], [a, c]] in the CONGR of S by Th22;

          hence thesis;

        end;

        thus (a,b) // (a,c) implies (a,b) // (b,c) or (a,c) // (c,b)

        proof

          assume [ [a, b], [a, c]] in the CONGR of S;

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

          then (a9,b9) // (b9,c9) or (a9,c9) // (c9,b9) by Th14;

          then [ [a, b], [b, c]] in the CONGR of S or [ [a, c], [c, b]] in the CONGR of S by Th22;

          hence thesis;

        end;

      end;

      thus ex a,b,c,d be Element of S st not (a,b) // (c,d) & not (a,b) // (d,c)

      proof

        consider a9,b9,c9,d9 be VECTOR of V such that

         A5: not (a9,b9) // (c9,d9) and

         A6: not (a9,b9) // (d9,c9) by A1, Th20;

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

         not [ [a, b], [d, c]] in the CONGR of S by A6, Th22;

        then

         A7: not (a,b) // (d,c);

         not [ [a, b], [c, d]] in the CONGR of S by A5, Th22;

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

        hence thesis by A7;

      end;

      thus for a,b,c be Element of S holds ex d be Element of S st (a,b) // (c,d) & (a,c) // (b,d) & b <> d

      proof

        let a,b,c be Element of S;

        reconsider a9 = a, b9 = b, c9 = c as Element of V;

        consider d9 be VECTOR of V such that

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

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

         A10: b9 <> d9 by A2, Th17;

        reconsider d = d9 as Element of S;

         [ [a, c], [b, d]] in the CONGR of S by A9, Th22;

        then

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

         [ [a, b], [c, d]] in the CONGR of S by A8, Th22;

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

        hence thesis by A10, A11;

      end;

      thus for p,a,b,c be Element of S st p <> b & (b,p) // (p,c) holds ex d be Element of S st (a,p) // (p,d) & (a,b) // (c,d)

      proof

        let p,a,b,c be Element of S;

        assume that

         A12: p <> b and

         A13: [ [b, p], [p, c]] in the CONGR of S;

        reconsider p9 = p, a9 = a, b9 = b, c9 = c as Element of V;

        (b9,p9) // (p9,c9) by A13, Th22;

        then

        consider d9 be VECTOR of V such that

         A14: (a9,p9) // (p9,d9) and

         A15: (a9,b9) // (c9,d9) by A12, Th18;

        reconsider d = d9 as Element of S;

         [ [a, b], [c, d]] in the CONGR of S by A15, Th22;

        then

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

         [ [a, p], [p, d]] in the CONGR of S by A14, Th22;

        then (a,p) // (p,d);

        hence thesis by A16;

      end;

    end;

    theorem :: ANALOAF:24

    

     Th24: (ex p,q be VECTOR of V st (for w be VECTOR of V holds ex a,b be Real st ((a * p) + (b * q)) = w)) implies for a,b,c,d be Element of ( OASpace V) st not (a,b) // (c,d) & not (a,b) // (d,c) holds ex t be Element of ( OASpace V) st ((a,b) // (a,t) or (a,b) // (t,a)) & ((c,d) // (c,t) or (c,d) // (t,c))

    proof

      assume

       A1: ex p,q be VECTOR of V st for w be VECTOR of V holds ex a,b be Real st ((a * p) + (b * q)) = w;

      set S = ( OASpace V);

      let a,b,c,d be Element of ( OASpace V);

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

      assume ( not [ [a, b], [c, d]] in the CONGR of S) & not [ [a, b], [d, c]] in the CONGR of S;

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

      then

      consider t9 be VECTOR of V such that

       A2: (a9,b9) // (a9,t9) or (a9,b9) // (t9,a9) and

       A3: (c9,d9) // (c9,t9) or (c9,d9) // (t9,c9) by A1, Th21;

      reconsider t = t9 as Element of S;

       [ [c, d], [c, t]] in the CONGR of S or [ [c, d], [t, c]] in the CONGR of S by A3, Th22;

      then

       A4: (c,d) // (c,t) or (c,d) // (t,c);

       [ [a, b], [a, t]] in the CONGR of S or [ [a, b], [t, a]] in the CONGR of S by A2, Th22;

      then (a,b) // (a,t) or (a,b) // (t,a);

      hence thesis by A4;

    end;

    definition

      let IT be non empty AffinStruct;

      :: ANALOAF:def5

      attr IT is OAffinSpace-like means

      : Def5: (for a,b,c,d,p,q,r,s be Element of IT holds (a,b) // (c,c) & ((a,b) // (b,a) implies a = b) & (a <> b & (a,b) // (p,q) & (a,b) // (r,s) implies (p,q) // (r,s)) & ((a,b) // (c,d) implies (b,a) // (d,c)) & ((a,b) // (b,c) implies (a,b) // (a,c)) & ((a,b) // (a,c) implies (a,b) // (b,c) or (a,c) // (c,b))) & (ex a,b,c,d be Element of IT st not (a,b) // (c,d) & not (a,b) // (d,c)) & (for a,b,c be Element of IT holds ex d be Element of IT st (a,b) // (c,d) & (a,c) // (b,d) & b <> d) & for p,a,b,c be Element of IT st p <> b & (b,p) // (p,c) holds ex d be Element of IT st (a,p) // (p,d) & (a,b) // (c,d);

    end

    registration

      cluster strict OAffinSpace-like for non trivial AffinStruct;

      existence

      proof

        consider V, u, v such that

         A1: for a,b be Real st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 and for w holds ex a,b be Real st w = ((a * u) + (b * v)) by FUNCSDOM: 23;

        

         A2: (ex a,b,c,d be Element of ( OASpace V) st not (a,b) // (c,d) & not (a,b) // (d,c)) & for a,b,c be Element of ( OASpace V) holds ex d be Element of ( OASpace V) st (a,b) // (c,d) & (a,c) // (b,d) & b <> d by A1, Th23;

        

         A3: for p,a,b,c be Element of ( OASpace V) st p <> b & (b,p) // (p,c) holds ex d be Element of ( OASpace V) st (a,p) // (p,d) & (a,b) // (c,d) by A1, Th23;

        (ex a,b be Element of ( OASpace V) st a <> b) & for a,b,c,d,p,q,r,s be Element of ( OASpace V) holds (a,b) // (c,c) & ((a,b) // (b,a) implies a = b) & (a <> b & (a,b) // (p,q) & (a,b) // (r,s) implies (p,q) // (r,s)) & ((a,b) // (c,d) implies (b,a) // (d,c)) & ((a,b) // (b,c) implies (a,b) // (a,c)) & ((a,b) // (a,c) implies (a,b) // (b,c) or (a,c) // (c,b)) by A1, Th23;

        then ( OASpace V) is non trivial OAffinSpace-like by A2, A3, STRUCT_0:def 10;

        hence thesis;

      end;

    end

    definition

      mode OAffinSpace is OAffinSpace-like non trivial AffinStruct;

    end

    theorem :: ANALOAF:25

    (ex a,b be Element of AS st a <> b) & (for a,b,c,d,p,q,r,s be Element of AS holds (a,b) // (c,c) & ((a,b) // (b,a) implies a = b) & (a <> b & (a,b) // (p,q) & (a,b) // (r,s) implies (p,q) // (r,s)) & ((a,b) // (c,d) implies (b,a) // (d,c)) & ((a,b) // (b,c) implies (a,b) // (a,c)) & ((a,b) // (a,c) implies (a,b) // (b,c) or (a,c) // (c,b))) & (ex a,b,c,d be Element of AS st not (a,b) // (c,d) & not (a,b) // (d,c)) & (for a,b,c be Element of AS holds ex d be Element of AS st (a,b) // (c,d) & (a,c) // (b,d) & b <> d) & (for p,a,b,c be Element of AS st p <> b & (b,p) // (p,c) holds ex d be Element of AS st (a,p) // (p,d) & (a,b) // (c,d)) iff AS is OAffinSpace by Def5, STRUCT_0:def 10;

    theorem :: ANALOAF:26

    

     Th26: (ex u, v st for a,b be Real st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 ) implies ( OASpace V) is OAffinSpace

    proof

      assume

       A1: ex u, v st for a,b be Real st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 ;

      then

       A2: (ex a,b,c,d be Element of ( OASpace V) st not (a,b) // (c,d) & not (a,b) // (d,c)) & for a,b,c be Element of ( OASpace V) holds ex d be Element of ( OASpace V) st (a,b) // (c,d) & (a,c) // (b,d) & b <> d by Th23;

      

       A3: for p,a,b,c be Element of ( OASpace V) st p <> b & (b,p) // (p,c) holds ex d be Element of ( OASpace V) st (a,p) // (p,d) & (a,b) // (c,d) by A1, Th23;

      (ex a,b be Element of ( OASpace V) st a <> b) & for a,b,c,d,p,q,r,s be Element of ( OASpace V) holds (a,b) // (c,c) & ((a,b) // (b,a) implies a = b) & (a <> b & (a,b) // (p,q) & (a,b) // (r,s) implies (p,q) // (r,s)) & ((a,b) // (c,d) implies (b,a) // (d,c)) & ((a,b) // (b,c) implies (a,b) // (a,c)) & ((a,b) // (a,c) implies (a,b) // (b,c) or (a,c) // (c,b)) by A1, Th23;

      hence thesis by A2, A3, Def5, STRUCT_0:def 10;

    end;

    definition

      let IT be OAffinSpace;

      :: ANALOAF:def6

      attr IT is 2-dimensional means

      : Def6: for a,b,c,d be Element of IT st not (a,b) // (c,d) & not (a,b) // (d,c) holds ex p be Element of IT st ((a,b) // (a,p) or (a,b) // (p,a)) & ((c,d) // (c,p) or (c,d) // (p,c));

    end

    registration

      cluster strict 2-dimensional for OAffinSpace;

      existence

      proof

        consider V such that

         A1: ex u, v st (for a,b be Real st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 ) & for w holds ex a,b be Real st w = ((a * u) + (b * v)) by FUNCSDOM: 23;

        reconsider S = ( OASpace V) as OAffinSpace by A1, Th26;

        for a,b,c,d be Element of S st not (a,b) // (c,d) & not (a,b) // (d,c) holds ex p be Element of S st ((a,b) // (a,p) or (a,b) // (p,a)) & ((c,d) // (c,p) or (c,d) // (p,c)) by A1, Th24;

        then S is 2-dimensional;

        hence thesis;

      end;

    end

    definition

      mode OAffinPlane is 2-dimensional OAffinSpace;

    end

    theorem :: ANALOAF:27

    (ex a,b be Element of AS st a <> b) & (for a,b,c,d,p,q,r,s be Element of AS holds (a,b) // (c,c) & ((a,b) // (b,a) implies a = b) & (a <> b & (a,b) // (p,q) & (a,b) // (r,s) implies (p,q) // (r,s)) & ((a,b) // (c,d) implies (b,a) // (d,c)) & ((a,b) // (b,c) implies (a,b) // (a,c)) & ((a,b) // (a,c) implies (a,b) // (b,c) or (a,c) // (c,b))) & (ex a,b,c,d be Element of AS st not (a,b) // (c,d) & not (a,b) // (d,c)) & (for a,b,c be Element of AS holds ex d be Element of AS st (a,b) // (c,d) & (a,c) // (b,d) & b <> d) & (for p,a,b,c be Element of AS st p <> b & (b,p) // (p,c) holds ex d be Element of AS st (a,p) // (p,d) & (a,b) // (c,d)) & (for a,b,c,d be Element of AS st not (a,b) // (c,d) & not (a,b) // (d,c) holds ex p be Element of AS st ((a,b) // (a,p) or (a,b) // (p,a)) & ((c,d) // (c,p) or (c,d) // (p,c))) iff AS is OAffinPlane by Def5, Def6, STRUCT_0:def 10;

    theorem :: ANALOAF:28

    (ex u, v st (for a,b be Real st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 ) & (for w holds ex a,b be Real st w = ((a * u) + (b * v)))) implies ( OASpace V) is OAffinPlane

    proof

      set S = ( OASpace V);

      assume

       A1: ex u, v st (for a,b be Real st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 ) & for w holds ex a,b be Real st w = ((a * u) + (b * v));

      then for a,b,c,d be Element of S st not (a,b) // (c,d) & not (a,b) // (d,c) holds ex p be Element of S st ((a,b) // (a,p) or (a,b) // (p,a)) & ((c,d) // (c,p) or (c,d) // (p,c)) by Th24;

      hence thesis by A1, Def6, Th26;

    end;