geomtrap.miz



    begin

    reserve V for RealLinearSpace;

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

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

    reserve x,z for set;

    definition

      let V;

      let u, v, u1, v1;

      :: GEOMTRAP:def1

      pred u,v '||' u1,v1 means (u,v) // (u1,v1) or (u,v) // (v1,u1);

    end

    theorem :: GEOMTRAP:1

    

     Th1: Gen (w,y) implies ( OASpace V) is OAffinSpace

    proof

      assume Gen (w,y);

      then for a1, a2 st ((a1 * w) + (a2 * y)) = ( 0. V) holds a1 = 0 & a2 = 0 by ANALMETR:def 1;

      hence thesis by ANALOAF: 26;

    end;

    theorem :: GEOMTRAP:2

    

     Th2: for p,q,p1,q1 be Element of ( OASpace V) st p = u & q = v & p1 = u1 & q1 = v1 holds ((p,q) // (p1,q1) iff (u,v) // (u1,v1))

    proof

      

       A1: ( OASpace V) = AffinStruct (# the carrier of V, ( DirPar V) #) by ANALOAF:def 4;

      let p,q,p1,q1 be Element of ( OASpace V) such that

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

       A3:

      now

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

        then [ [p, q], [p1, q1]] in the CONGR of ( OASpace V) by A2, A1, ANALOAF: 22;

        hence (p,q) // (p1,q1) by ANALOAF:def 2;

      end;

      now

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

        then [ [u, v], [u1, v1]] in ( DirPar V) by A2, A1, ANALOAF:def 2;

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

      end;

      hence thesis by A3;

    end;

    theorem :: GEOMTRAP:3

    

     Th3: Gen (w,y) implies for p,q,p1,q1 be Element of the carrier of ( Lambda ( OASpace V)) st p = u & q = v & p1 = u1 & q1 = v1 holds ((p,q) // (p1,q1) iff (u,v) '||' (u1,v1))

    proof

      assume Gen (w,y);

      then

      reconsider S = ( OASpace V) as OAffinSpace by Th1;

      let p,q,p1,q1 be Element of the carrier of ( Lambda ( OASpace V)) such that

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

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

      then

      reconsider p9 = p, q9 = q, p19 = p1, q19 = q1 as Element of S;

       A2:

      now

        assume (u,v) '||' (u1,v1);

        then (u,v) // (u1,v1) or (u,v) // (v1,u1);

        then (p9,q9) // (p19,q19) or (p9,q9) // (q19,p19) by A1, Th2;

        then (p9,q9) '||' (p19,q19) by DIRAF:def 4;

        hence (p,q) // (p1,q1) by DIRAF: 38;

      end;

      now

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

        then (p9,q9) '||' (p19,q19) by DIRAF: 38;

        then (p9,q9) // (p19,q19) or (p9,q9) // (q19,p19) by DIRAF:def 4;

        then (u,v) // (u1,v1) or (u,v) // (v1,u1) by A1, Th2;

        hence (u,v) '||' (u1,v1);

      end;

      hence thesis by A2;

    end;

    theorem :: GEOMTRAP:4

    

     Th4: for p,q,p1,q1 be Element of the carrier of ( AMSpace (V,w,y)) st p = u & q = v & p1 = u1 & q1 = v1 holds ((p,q) // (p1,q1) iff (u,v) '||' (u1,v1))

    proof

      let p,q,p1,q1 be Element of the carrier of ( AMSpace (V,w,y)) such that

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

       A2:

      now

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

        then ex a, b st (a * (v - u)) = (b * (v1 - u1)) & (a <> 0 or b <> 0 ) by A1, ANALMETR: 22;

        then (u,v) // (u1,v1) or (u,v) // (v1,u1) by ANALMETR: 14;

        hence (u,v) '||' (u1,v1);

      end;

      now

        assume (u,v) '||' (u1,v1);

        then (u,v) // (u1,v1) or (u,v) // (v1,u1);

        then ex a, b st (a * (v - u)) = (b * (v1 - u1)) & (a <> 0 or b <> 0 ) by ANALMETR: 14;

        hence (p,q) // (p1,q1) by A1, ANALMETR: 22;

      end;

      hence thesis by A2;

    end;

    definition

      let V;

      let u, v;

      :: GEOMTRAP:def2

      func u # v -> VECTOR of V means

      : Def2: (it + it ) = (u + v);

      existence

      proof

        set y = (u + v);

        set w = ((2 " ) * y);

        ((2 " ) + (2 " )) = 1;

        

        then (w + w) = (1 * y) by RLVECT_1:def 6

        .= y by RLVECT_1:def 8;

        hence thesis;

      end;

      uniqueness

      proof

        let w, w1;

        assume (w + w) = (u + v) & (w1 + w1) = (u + v);

        

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

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

        .= (w + ((w - w1) - w1)) by RLVECT_1: 27

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

        .= ((w - w1) + (w - w1)) by RLVECT_1:def 3;

        then (w - w1) = ( 0. V) by RLVECT_1: 20;

        hence thesis by RLVECT_1: 21;

      end;

      commutativity ;

      idempotence ;

    end

    theorem :: GEOMTRAP:5

    

     Th5: ex y st (u # y) = w

    proof

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

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

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

      .= (w + w) by RLVECT_1: 4;

      hence thesis by Def2;

    end;

    theorem :: GEOMTRAP:6

    

     Th6: ((u # u1) # (v # v1)) = ((u # v) # (u1 # v1))

    proof

      set p = (u # u1), q = (v # v1), r = (u # v), s = (u1 # v1);

      set x = (p # q), y = (r # s);

       A1:

      now

        let w;

        w = (1 * w) by RLVECT_1:def 8;

        

        then ((w + w) + (w + w)) = (((1 + 1) * w) + ((1 * w) + (1 * w))) by RLVECT_1:def 6

        .= (((1 + 1) * w) + ((1 + 1) * w)) by RLVECT_1:def 6

        .= (((1 + 1) + (1 + 1)) * w) by RLVECT_1:def 6;

        hence ((w + w) + (w + w)) = (4 * w);

      end;

      ((x + x) + (x + x)) = ((x + x) + (p + q)) by Def2

      .= ((p + q) + (p + q)) by Def2

      .= (p + (q + (p + q))) by RLVECT_1:def 3

      .= (p + (p + (q + q))) by RLVECT_1:def 3

      .= ((p + p) + (q + q)) by RLVECT_1:def 3

      .= ((p + p) + (v + v1)) by Def2

      .= ((u + u1) + (v + v1)) by Def2

      .= (u + (u1 + (v + v1))) by RLVECT_1:def 3

      .= (u + (v + (v1 + u1))) by RLVECT_1:def 3

      .= ((u + v) + (v1 + u1)) by RLVECT_1:def 3

      .= ((u + v) + (s + s)) by Def2

      .= ((r + r) + (s + s)) by Def2

      .= (r + (r + (s + s))) by RLVECT_1:def 3

      .= (r + (s + (s + r))) by RLVECT_1:def 3

      .= ((r + s) + (s + r)) by RLVECT_1:def 3

      .= ((y + y) + (r + s)) by Def2

      .= ((y + y) + (y + y)) by Def2;

      

      then (4 * x) = ((y + y) + (y + y)) by A1

      .= (4 * y) by A1;

      hence thesis by RLVECT_1: 36;

    end;

    theorem :: GEOMTRAP:7

    

     Th7: (u # y) = (u # w) implies y = w

    proof

      assume

       A1: (u # y) = (u # w);

      set p = (u # y);

      (u + y) = (p + p) by Def2

      .= (u + w) by A1, Def2;

      hence thesis by RLVECT_1: 8;

    end;

    theorem :: GEOMTRAP:8

    

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

    proof

      set p = (y # u), r = (y # v);

      

       A1: (y + u) = (p + p) & (y + v) = (r + r) by Def2;

      (2 * (r - p)) = (((1 + 1) * r) - ((1 + 1) * p)) by RLVECT_1: 34

      .= (((1 * r) + (1 * r)) - ((1 + 1) * p)) by RLVECT_1:def 6

      .= (((1 * r) + (1 * r)) - ((1 * p) + (1 * p))) by RLVECT_1:def 6

      .= ((r + (1 * r)) - ((1 * p) + (1 * p))) by RLVECT_1:def 8

      .= ((r + r) - ((1 * p) + (1 * p))) by RLVECT_1:def 8

      .= ((r + r) - (p + (1 * p))) by RLVECT_1:def 8

      .= ((y + v) - (y + u)) by A1, RLVECT_1:def 8

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

      .= (v + ((y - y) - u)) by RLVECT_1: 27

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

      .= (v - u) by RLVECT_1: 14

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

      hence thesis by ANALOAF:def 1;

    end;

    theorem :: GEOMTRAP:9

    (u,v) '||' ((w # u),(w # v)) by Th8;

    theorem :: GEOMTRAP:10

    

     Th10: (2 * ((u # v) - u)) = (v - u) & (2 * (v - (u # v))) = (v - u)

    proof

      set p = (u # v);

      

       A1: (2 - 1) = 1;

      

       A2: (2 * (v - p)) = ((2 * v) - ((1 + 1) * p)) by RLVECT_1: 34

      .= ((2 * v) - ((1 * p) + (1 * p))) by RLVECT_1:def 6

      .= ((2 * v) - ((1 * p) + p)) by RLVECT_1:def 8

      .= ((2 * v) - (p + p)) by RLVECT_1:def 8

      .= ((2 * v) - (u + v)) by Def2

      .= (((2 * v) - v) - u) by RLVECT_1: 27

      .= (((2 * v) - (1 * v)) - u) by RLVECT_1:def 8

      .= ((1 * v) - u) by A1, RLVECT_1: 35

      .= (v - u) by RLVECT_1:def 8;

      

       A3: (1 - 2) = ( - 1);

      (2 * (p - u)) = (((1 + 1) * p) - (2 * u)) by RLVECT_1: 34

      .= (((1 * p) + (1 * p)) - (2 * u)) by RLVECT_1:def 6

      .= ((p + (1 * p)) - (2 * u)) by RLVECT_1:def 8

      .= ((p + p) - (2 * u)) by RLVECT_1:def 8

      .= ((u + v) - (2 * u)) by Def2

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

      .= (v + ((1 * u) - (2 * u))) by RLVECT_1:def 8

      .= (v + (( - 1) * u)) by A3, RLVECT_1: 35

      .= (v - u) by RLVECT_1: 16;

      hence thesis by A2;

    end;

    theorem :: GEOMTRAP:11

    

     Th11: (u,(u # v)) // ((u # v),v)

    proof

      set p = (u # v);

      (2 * (p - u)) = (v - u) by Th10

      .= (2 * (v - p)) by Th10;

      hence thesis by ANALOAF:def 1;

    end;

    theorem :: GEOMTRAP:12

    

     Th12: (u,v) // (u,(u # v)) & (u,v) // ((u # v),v)

    proof

      set p = (u # v);

      (1 * (v - u)) = (v - u) by RLVECT_1:def 8

      .= (2 * (p - u)) by Th10;

      hence (u,v) // (u,(u # v)) by ANALOAF:def 1;

      (1 * (v - u)) = (v - u) by RLVECT_1:def 8

      .= (2 * (v - p)) by Th10;

      hence thesis by ANALOAF:def 1;

    end;

    

     Lm1: (u,y) // (y,v) implies (v,y) // (y,u) & (u,y) // (u,v) & (y,v) // (u,v)

    proof

      assume

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

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

      hence

       A2: (v,y) // (y,u) by ANALOAF: 12;

      thus (u,y) // (u,v) by A1, ANALOAF: 13;

      (v,y) // (v,u) by A2, ANALOAF: 13;

      hence thesis by ANALOAF: 12;

    end;

    theorem :: GEOMTRAP:13

    

     Th13: (u,y) // (y,v) implies ((u # y),y) // (y,(y # v))

    proof

      set p = (u # y), q = (y # v);

      (u,p) // (p,y) by Th11;

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

      then

       A1: (u,y) // (p,y) by ANALOAF: 12;

      (y,q) // (q,v) by Th11;

      then (y,q) // (y,v) by Lm1;

      then

       A2: (y,v) // (y,q) by ANALOAF: 12;

      assume

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

      now

        assume that

         A4: u <> y and

         A5: y <> v;

        (y,v) // (p,y) by A3, A1, A4, ANALOAF: 11;

        hence thesis by A2, A5, ANALOAF: 11;

      end;

      hence thesis by ANALOAF: 9;

    end;

    theorem :: GEOMTRAP:14

    

     Th14: (u,v) // (u1,v1) implies (u,v) // ((u # u1),(v # v1))

    proof

      assume

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

      per cases ;

        suppose u = v or u1 = v1;

        hence thesis by Th8, ANALOAF: 9;

      end;

        suppose

         A2: u <> v & u1 <> v1;

        set p = (u # u1), q = (v # v1);

        consider a, b such that

         A3: 0 < a & 0 < b and

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

        

         A5: 0 < (a + b) & 0 < (b * 2) by A3, XREAL_1: 34, XREAL_1: 129;

        ((b * 2) * (q - p)) = (b * (2 * (q - p))) by RLVECT_1:def 7

        .= (b * (((1 + 1) * q) - (2 * p))) by RLVECT_1: 34

        .= (b * (((1 * q) + (1 * q)) - (2 * p))) by RLVECT_1:def 6

        .= (b * ((q + (1 * q)) - (2 * p))) by RLVECT_1:def 8

        .= (b * ((q + q) - (2 * p))) by RLVECT_1:def 8

        .= (b * ((v + v1) - (2 * p))) by Def2

        .= (b * (v + (v1 - ((1 + 1) * p)))) by RLVECT_1:def 3

        .= (b * (v + (v1 - ((1 * p) + (1 * p))))) by RLVECT_1:def 6

        .= (b * (v + (v1 - (p + (1 * p))))) by RLVECT_1:def 8

        .= (b * (v + (v1 - (p + p)))) by RLVECT_1:def 8

        .= (b * (v + (v1 - (u + u1)))) by Def2

        .= (b * (v + ((v1 - u1) - u))) by RLVECT_1: 27

        .= (b * ((v + (v1 - u1)) - u)) by RLVECT_1:def 3

        .= (b * ((v1 - u1) + (v - u))) by RLVECT_1:def 3

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

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

        hence thesis by A5, ANALOAF:def 1;

      end;

    end;

    

     Lm2: (u,v) // (u1,v1) implies (u,v) '||' ((u # v1),(v # u1))

    proof

      assume

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

      per cases ;

        suppose u = v;

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

        hence thesis;

      end;

        suppose u1 = v1;

        then (u,v) // ((u # v1),(v # u1)) by Th8;

        hence thesis;

      end;

        suppose u <> v & u1 <> v1;

        then

        consider a, b such that 0 < a and

         A2: 0 < b and

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

        

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

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

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

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

        set p = (u # v1), q = (v # u1), A = (b * 2), D = (b - a);

        

         A5: A <> 0 by A2;

        (A * (q - p)) = (b * (2 * (q - p))) by RLVECT_1:def 7

        .= (b * (((1 + 1) * q) - (2 * p))) by RLVECT_1: 34

        .= (b * (((1 * q) + (1 * q)) - (2 * p))) by RLVECT_1:def 6

        .= (b * ((q + (1 * q)) - (2 * p))) by RLVECT_1:def 8

        .= (b * ((q + q) - (2 * p))) by RLVECT_1:def 8

        .= (b * ((v + u1) - (2 * p))) by Def2

        .= (b * (v + (u1 - ((1 + 1) * p)))) by RLVECT_1:def 3

        .= (b * (v + (u1 - ((1 * p) + (1 * p))))) by RLVECT_1:def 6

        .= (b * (v + (u1 - (p + (1 * p))))) by RLVECT_1:def 8

        .= (b * (v + (u1 - (p + p)))) by RLVECT_1:def 8

        .= (b * (v + (u1 - (u + v1)))) by Def2

        .= (b * (v + ((u1 - v1) - u))) by RLVECT_1: 27

        .= (b * ((v + (u1 - v1)) - u)) by RLVECT_1:def 3

        .= (b * ((u1 - v1) + (v - u))) by RLVECT_1:def 3

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

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

        .= (D * (v - u));

        then (u,v) // (p,q) or (u,v) // (q,p) by A5, ANALMETR: 14;

        hence thesis;

      end;

    end;

    

     Lm3: (u1 # u2) = (v1 # v2) implies (v1 - u1) = ( - (v2 - u2))

    proof

      set p = (u1 # u2);

      

       A1: (p + p) = (u1 + u2) by Def2;

      assume (u1 # u2) = (v1 # v2);

      then

       A2: (p + p) = (v1 + v2) by Def2;

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

      .= u2 by A1, A2, RLSUB_2: 61;

      

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

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

      hence thesis by RLVECT_1: 6;

    end;

    

     Lm4: (u,v,u1,v1) are_Ort_wrt (w,y) implies (u,v,v1,u1) are_Ort_wrt (w,y)

    proof

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

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

      then

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

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

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

      hence thesis by A1, ANALMETR:def 3;

    end;

    

     Lm5: (u,v,u1,v1) are_Ort_wrt (w,y) implies (u1,v1,u,v) are_Ort_wrt (w,y)

    proof

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

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

      then ((v1 - u1),(v - u)) are_Ort_wrt (w,y) by ANALMETR: 4;

      hence thesis by ANALMETR:def 3;

    end;

    

     Lm6: Gen (w,y) implies (u,v,u1,u1) are_Ort_wrt (w,y)

    proof

      

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

      assume Gen (w,y);

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

      hence thesis by ANALMETR:def 3;

    end;

    

     Lm7: Gen (w,y) & (u,v,w1,v1) are_Ort_wrt (w,y) & (u,v,w1,v2) are_Ort_wrt (w,y) implies (u,v,v1,v2) are_Ort_wrt (w,y)

    proof

      assume that

       A1: Gen (w,y) and

       A2: (u,v,w1,v1) are_Ort_wrt (w,y) & (u,v,w1,v2) are_Ort_wrt (w,y);

      ((v - u),(v1 - w1)) are_Ort_wrt (w,y) & ((v - u),(v2 - w1)) are_Ort_wrt (w,y) by A2, ANALMETR:def 3;

      then

       A3: ((v - u),((v2 - w1) - (v1 - w1))) are_Ort_wrt (w,y) by A1, ANALMETR: 10;

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

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

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

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

      hence thesis by A3, ANALMETR:def 3;

    end;

    

     Lm8: Gen (w,y) & (u,v,u,v) are_Ort_wrt (w,y) implies u = v

    proof

      assume that

       A1: Gen (w,y) and

       A2: (u,v,u,v) are_Ort_wrt (w,y);

      ((v - u),(v - u)) are_Ort_wrt (w,y) by A2, ANALMETR:def 3;

      then (v - u) = ( 0. V) by A1, ANALMETR: 11;

      hence thesis by RLVECT_1: 21;

    end;

    

     Lm9: Gen (w,y) implies (u,v,u1,u1) are_Ort_wrt (w,y) & (u1,u1,u,v) are_Ort_wrt (w,y)

    proof

      

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

      assume Gen (w,y);

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

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

      hence thesis by Lm5;

    end;

    

     Lm10: Gen (w,y) & ((u1,v1) '||' (u,v) or (u,v) '||' (u1,v1)) & ((u2,v2,u,v) are_Ort_wrt (w,y) or (u,v,u2,v2) are_Ort_wrt (w,y)) & u <> v implies (u1,v1,u2,v2) are_Ort_wrt (w,y) & (u2,v2,u1,v1) are_Ort_wrt (w,y)

    proof

      assume that

       A1: Gen (w,y) and

       A2: (u1,v1) '||' (u,v) or (u,v) '||' (u1,v1) and

       A3: (u2,v2,u,v) are_Ort_wrt (w,y) or (u,v,u2,v2) are_Ort_wrt (w,y) and

       A4: u <> v;

      reconsider p9 = u, q9 = v, p19 = u1, q19 = v1, p29 = u2, q29 = v2 as Element of the carrier of ( AMSpace (V,w,y)) by ANALMETR: 19;

      reconsider S = ( AMSpace (V,w,y)) as OrtAfSp by A1, ANALMETR: 33;

      reconsider p = p9, q = q9, p1 = p19, q1 = q19, p2 = p29, q2 = q29 as Element of S;

      

       A5: (p2,q2) _|_ (p,q) or (p,q) _|_ (p2,q2) by A3, ANALMETR: 21;

      (p1,q1) // (p,q) or (p,q) // (p1,q1) by A2, Th4;

      then (p1,q1) _|_ (p2,q2) & (p2,q2) _|_ (p1,q1) by A4, A5, ANALMETR: 62;

      hence thesis by ANALMETR: 21;

    end;

    definition

      let V;

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

      :: GEOMTRAP:def3

      pred u,u1,v,v1 are_DTr_wrt w,y means (u,u1) // (v,v1) & (u,u1,(u # u1),(v # v1)) are_Ort_wrt (w,y) & (v,v1,(u # u1),(v # v1)) are_Ort_wrt (w,y);

    end

    theorem :: GEOMTRAP:15

     Gen (w,y) implies (u,u,v,v) are_DTr_wrt (w,y) by Lm5, Lm6, ANALOAF: 9;

    theorem :: GEOMTRAP:16

     Gen (w,y) implies (u,v,u,v) are_DTr_wrt (w,y) by Lm6, ANALOAF: 8;

    theorem :: GEOMTRAP:17

    

     Th17: (u,v,v,u) are_DTr_wrt (w,y) implies u = v by ANALOAF: 10;

    theorem :: GEOMTRAP:18

    

     Th18: Gen (w,y) & (v1,u,u,v2) are_DTr_wrt (w,y) implies v1 = u & u = v2

    proof

      assume that

       A1: Gen (w,y) and

       A2: (v1,u,u,v2) are_DTr_wrt (w,y);

      set a = (v1 # u), b = (u # v2);

      

       A3: (v1,u,a,b) are_Ort_wrt (w,y) by A2;

      

       A4: (u,v2,a,b) are_Ort_wrt (w,y) by A2;

      

       A5: (v1,u) // (u,v2) by A2;

      per cases ;

        suppose v1 = v2;

        hence thesis by A2, Th17;

      end;

        suppose v1 <> v2;

        then

         A6: a <> b by Th7;

        (u,v2) // (u,b) by Th12;

        then

         A7: (u,v2) '||' (u,b);

        

         A8: (a,u) // (u,b) by A5, Th13;

        then (u,b) // (a,b) by Lm1;

        then

         A9: (u,b) '||' (a,b);

        

         A10: u = v2

        proof

          assume

           A11: u <> v2;

          

           A12: u <> b

          proof

            assume u = b;

            then (u # v2) = (u # u);

            hence contradiction by A11, Th7;

          end;

          (u,b,a,b) are_Ort_wrt (w,y) by A1, A4, A7, A11, Lm10;

          then (u,b,u,b) are_Ort_wrt (w,y) by A1, A6, A9, Lm10;

          hence contradiction by A1, A12, Lm8;

        end;

        (v1,u) // (a,u) by Th12;

        then

         A13: (v1,u) '||' (a,u);

        (a,u) // (a,b) by A8, Lm1;

        then

         A14: (a,u) '||' (a,b);

        v1 = u

        proof

          assume

           A15: v1 <> u;

          

           A16: u <> a

          proof

            assume u = a;

            then (v1 # u) = (u # u);

            hence contradiction by A15, Th7;

          end;

          (a,u,a,b) are_Ort_wrt (w,y) by A1, A3, A13, A15, Lm10;

          then (a,u,a,u) are_Ort_wrt (w,y) by A1, A6, A14, Lm10;

          hence contradiction by A1, A16, Lm8;

        end;

        hence thesis by A10;

      end;

    end;

    theorem :: GEOMTRAP:19

    

     Th19: Gen (w,y) & (u,v,u1,v1) are_DTr_wrt (w,y) & (u,v,u2,v2) are_DTr_wrt (w,y) & u <> v implies (u1,v1,u2,v2) are_DTr_wrt (w,y)

    proof

      assume that

       A1: Gen (w,y) and

       A2: (u,v,u1,v1) are_DTr_wrt (w,y) and

       A3: (u,v,u2,v2) are_DTr_wrt (w,y) and

       A4: u <> v;

      set a = (u1 # v1), b = (u2 # v2);

      (u,v,(u # v),(u1 # v1)) are_Ort_wrt (w,y) & (u,v,(u # v),(u2 # v2)) are_Ort_wrt (w,y) by A2, A3;

      then

       A5: (u,v,a,b) are_Ort_wrt (w,y) by A1, Lm7;

      

       A6: (u,v) // (u2,v2) by A3;

      then (u,v) '||' (u2,v2);

      then

       A7: (u2,v2,a,b) are_Ort_wrt (w,y) by A1, A4, A5, Lm10;

      

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

      then (u,v) '||' (u1,v1);

      then

       A9: (u1,v1,a,b) are_Ort_wrt (w,y) by A1, A4, A5, Lm10;

      (u1,v1) // (u2,v2) by A4, A8, A6, ANALOAF: 11;

      hence thesis by A9, A7;

    end;

    theorem :: GEOMTRAP:20

    

     Th20: Gen (w,y) implies ex t be VECTOR of V st ((u,v,u1,t) are_DTr_wrt (w,y) or (u,v,t,u1) are_DTr_wrt (w,y))

    proof

      assume

       A1: Gen (w,y);

      set a = (u # v);

      per cases ;

        suppose

         A2: u = v;

        

         A3: (u1,u1,(u # u),(u1 # u1)) are_Ort_wrt (w,y) by A1, Lm5, Lm6;

        (u,u) // (u1,u1) & (u,u,(u # u),(u1 # u1)) are_Ort_wrt (w,y) by A1, Lm5, Lm6, ANALOAF: 9;

        then (u,u,u1,u1) are_DTr_wrt (w,y) by A3;

        hence thesis by A2;

      end;

        suppose

         A4: u <> v;

        a <> u

        proof

          assume a = u;

          then (u # u) = (u # v);

          hence contradiction by A4, Th7;

        end;

        then (u - a) <> ( 0. V) by RLVECT_1: 21;

        then

        consider r be Real such that

         A5: (((u1 - a) - (r * (u - a))),(u - a)) are_Ort_wrt (w,y) by A1, ANALMETR: 13;

        set b = (u1 - (r * (u - a)));

        set t = ((2 * b) - u1);

        (u1 + t) = ((1 + 1) * b) by RLSUB_2: 61

        .= ((1 * b) + (1 * b)) by RLVECT_1:def 6

        .= (b + (1 * b)) by RLVECT_1:def 8

        .= (b + b) by RLVECT_1:def 8;

        then

         A6: (u1 # t) = b by Def2;

        (u1 - b) = ((u1 - u1) + (r * (u - a))) by RLVECT_1: 29

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

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

        

        then

         A7: (u1 - t) = (2 * (r * (u - a))) by A6, Th10

        .= ((2 * r) * (u - a)) by RLVECT_1:def 7;

        

         A8: (u1 - (a + (r * (u - a)))) = ((u1 - (r * (u - a))) - a) by RLVECT_1: 27;

        then ((b - a),(u - a)) are_Ort_wrt (w,y) by A5, RLVECT_1: 27;

        then ((b - a),(u1 - t)) are_Ort_wrt (w,y) by A7, ANALMETR: 7;

        then

         A9: (a,b,t,u1) are_Ort_wrt (w,y) by ANALMETR:def 3;

        then

         A10: (t,u1,(u # v),(t # u1)) are_Ort_wrt (w,y) by A6, Lm5;

        

         A11: (u - v) = (2 * (u - (u # v))) by Th10;

        then (u1 - t) = (r * (u - v)) by A7, RLVECT_1:def 7;

        then (r * (u - v)) = (1 * (u1 - t)) by RLVECT_1:def 8;

        then (v,u) // (t,u1) or (v,u) // (u1,t) by ANALMETR: 14;

        then

         A12: (u,v) // (u1,t) or (u,v) // (t,u1) by ANALOAF: 12;

        (a,b,u1,t) are_Ort_wrt (w,y) by A9, Lm4;

        then

         A13: (u1,t,(u # v),(u1 # t)) are_Ort_wrt (w,y) by A6, Lm5;

        (b - a) = ((u1 - a) - (r * (u - a))) by A8, RLVECT_1: 27;

        then ((b - a),(u - v)) are_Ort_wrt (w,y) by A5, A11, ANALMETR: 7;

        then (a,b,v,u) are_Ort_wrt (w,y) by ANALMETR:def 3;

        then (a,b,u,v) are_Ort_wrt (w,y) by Lm4;

        then (u,v,(u # v),(u1 # t)) are_Ort_wrt (w,y) by A6, Lm5;

        then (u,v,u1,t) are_DTr_wrt (w,y) or (u,v,t,u1) are_DTr_wrt (w,y) by A13, A10, A12;

        hence thesis;

      end;

    end;

    theorem :: GEOMTRAP:21

    

     Th21: (u,v,u1,v1) are_DTr_wrt (w,y) implies (u1,v1,u,v) are_DTr_wrt (w,y) by ANALOAF: 12, Lm4;

    theorem :: GEOMTRAP:22

    

     Th22: (u,v,u1,v1) are_DTr_wrt (w,y) implies (v,u,v1,u1) are_DTr_wrt (w,y)

    proof

      assume

       A1: (u,v,u1,v1) are_DTr_wrt (w,y);

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

      then

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

       A3:

      now

        let u,u9,v,v9 be VECTOR of V;

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

        then (v,v9,u,u9) are_Ort_wrt (w,y) by Lm5;

        then (v,v9,u9,u) are_Ort_wrt (w,y) by Lm4;

        hence (u9,u,v,v9) are_Ort_wrt (w,y) by Lm5;

      end;

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

      then

       A4: (v1,u1,(v # u),(v1 # u1)) are_Ort_wrt (w,y) by A3;

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

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

      hence thesis by A2, A4;

    end;

    

     Lm11: Gen (w,y) & u <> v & (u,v) '||' (u,u1) & (u,v) '||' (u,v1) & (u,v) '||' (u,u2) & (u,v) '||' (u,v2) implies (u1,v1) '||' (u2,v2)

    proof

      assume that

       A1: Gen (w,y) and

       A2: u <> v and

       A3: (u,v) '||' (u,u1) and

       A4: (u,v) '||' (u,v1) and

       A5: (u,v) '||' (u,u2) and

       A6: (u,v) '||' (u,v2);

      reconsider p9 = u, q9 = v, p19 = u1, q19 = v1, p29 = u2, q29 = v2 as Element of ( Lambda ( OASpace V)) by ANALMETR: 16;

      reconsider S9 = ( OASpace V) as OAffinSpace by A1, Th1;

      reconsider S = ( Lambda S9) as AffinSpace by DIRAF: 41;

      reconsider p = p9, q = q9, p1 = p19, q1 = q19, p2 = p29, q2 = q29 as Element of the carrier of S;

      (p,q) // (p,p1) by A1, A3, Th3;

      then

       A7: LIN (p,q,p1) by AFF_1:def 1;

      (p,q) // (p,q1) by A1, A4, Th3;

      then

       A8: LIN (p,q,q1) by AFF_1:def 1;

      (p,q) // (p,q2) by A1, A6, Th3;

      then LIN (p,q,q2) by AFF_1:def 1;

      then

       A9: LIN (p1,q1,q2) by A2, A7, A8, AFF_1: 8;

      (p,q) // (p,p2) by A1, A5, Th3;

      then LIN (p,q,p2) by AFF_1:def 1;

      then LIN (p1,q1,p2) by A2, A7, A8, AFF_1: 8;

      then (p1,q1) // (p2,q2) by A9, AFF_1: 10;

      hence thesis by A1, Th3;

    end;

    theorem :: GEOMTRAP:23

    

     Th23: Gen (w,y) & (v,u1,v,u2) are_DTr_wrt (w,y) implies u1 = u2

    proof

      assume that

       A1: Gen (w,y) and

       A2: (v,u1,v,u2) are_DTr_wrt (w,y);

      

       A3: (v,u1,(v # u1),(v # u2)) are_Ort_wrt (w,y) by A2;

      

       A4: (v,u2,(v # u1),(v # u2)) are_Ort_wrt (w,y) by A2;

      (v,u1) // (v,u1) by ANALOAF: 8;

      then

       A5: (v,u1) '||' (v,u1);

      set b = (v # u1), c = (v # u2);

      

       A6: (v,u1) // (v,b) by Th12;

      then

       A7: (v,u1) '||' (v,b);

      

       A8: (v,u1) // (v,u2) by A2;

      (v,u2) // (v,b)

      proof

        per cases ;

          suppose v = b;

          hence thesis by ANALOAF: 9;

        end;

          suppose v <> b;

          then v <> u1;

          hence thesis by A8, A6, ANALOAF: 11;

        end;

      end;

      then

       A9: (v,u2) '||' (v,b);

      (v,u2) // (v,v) by ANALOAF: 9;

      then

       A10: (v,u2) '||' (v,v);

      

       A11: (v,u2) // (v,c) by Th12;

      then

       A12: (v,u2) '||' (v,c);

      

       A13: (v,u2) // (v,u1) by A8, ANALOAF: 12;

      (v,u1) // (v,c)

      proof

        per cases ;

          suppose v = c;

          hence thesis by ANALOAF: 9;

        end;

          suppose v <> c;

          then v <> u2;

          hence thesis by A13, A11, ANALOAF: 11;

        end;

      end;

      then

       A14: (v,u1) '||' (v,c);

      (v,u2) // (v,u2) by ANALOAF: 8;

      then

       A15: (v,u2) '||' (v,u2);

      (v,u1) // (v,v) by ANALOAF: 9;

      then

       A16: (v,u1) '||' (v,v);

      assume

       A17: u1 <> u2;

      per cases by A17;

        suppose

         A18: v <> u1;

        then (v,u1) '||' (b,c) by A1, A7, A5, A16, A14, Lm11;

        then (b,c,b,c) are_Ort_wrt (w,y) by A1, A3, A18, Lm10;

        hence thesis by A1, A17, Lm8, Th7;

      end;

        suppose

         A19: v <> u2;

        then (v,u2) '||' (b,c) by A1, A12, A15, A10, A9, Lm11;

        then (b,c,b,c) are_Ort_wrt (w,y) by A1, A4, A19, Lm10;

        hence thesis by A1, A17, Lm8, Th7;

      end;

    end;

    theorem :: GEOMTRAP:24

    

     Th24: Gen (w,y) & (u,v,u1,v1) are_DTr_wrt (w,y) & (u,v,u1,v2) are_DTr_wrt (w,y) implies (u = v or v1 = v2)

    proof

      assume that

       A1: Gen (w,y) and

       A2: (u,v,u1,v1) are_DTr_wrt (w,y) & (u,v,u1,v2) are_DTr_wrt (w,y);

      assume u <> v;

      then (u1,v1,u1,v2) are_DTr_wrt (w,y) by A1, A2, Th19;

      hence thesis by A1, Th23;

    end;

    theorem :: GEOMTRAP:25

    

     Th25: Gen (w,y) & u <> u1 & (u,u1,v,v1) are_DTr_wrt (w,y) & ((u,u1,v,v2) are_DTr_wrt (w,y) or (u,u1,v2,v) are_DTr_wrt (w,y)) implies v1 = v2

    proof

      assume that

       A1: Gen (w,y) and

       A2: u <> u1 & (u,u1,v,v1) are_DTr_wrt (w,y) and

       A3: (u,u1,v,v2) are_DTr_wrt (w,y) or (u,u1,v2,v) are_DTr_wrt (w,y);

      now

        assume (u,u1,v2,v) are_DTr_wrt (w,y);

        then

         A4: (v2,v,v,v1) are_DTr_wrt (w,y) by A1, A2, Th19;

        then v = v2 by A1, Th18;

        hence thesis by A1, A4, Th18;

      end;

      hence thesis by A1, A2, A3, Th24;

    end;

    theorem :: GEOMTRAP:26

    

     Th26: Gen (w,y) & (u,v,u1,v1) are_DTr_wrt (w,y) implies (u,v,(u # u1),(v # v1)) are_DTr_wrt (w,y)

    proof

      assume that

       A1: Gen (w,y) and

       A2: (u,v,u1,v1) are_DTr_wrt (w,y);

      set p = (u # u1), q = (v # v1), r = (u # v), s = (u1 # v1);

      

       A3: u = v & u1 = v1 implies (p,q,r,(p # q)) are_Ort_wrt (w,y) by A1, Lm9;

      (p # q) = (r # s) by Th6;

      then (r,s) // (r,(p # q)) by Th12;

      then

       A4: (r,s) '||' (r,(p # q));

      (u,v,r,s) are_Ort_wrt (w,y) & (u1,v1,r,s) are_Ort_wrt (w,y) by A2;

      then

       A5: r <> s implies (u1,v1,r,(p # q)) are_Ort_wrt (w,y) & (u,v,r,(p # q)) are_Ort_wrt (w,y) by A1, A4, Lm10;

       A6:

      now

        assume r = s;

        

        then r = (r # s)

        .= (p # q) by Th6;

        hence (u1,v1,r,(p # q)) are_Ort_wrt (w,y) & (u,v,r,(p # q)) are_Ort_wrt (w,y) by A1, Lm9;

      end;

      

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

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

      then (u1,v1) // ((u1 # u),(v1 # v)) by Th14;

      then (u1,v1) '||' (p,q);

      then

       A8: u = v & u1 <> v1 implies (p,q,r,(p # q)) are_Ort_wrt (w,y) by A1, A6, A5, Lm10;

      

       A9: (u,v) // ((u # u1),(v # v1)) by A7, Th14;

      then (u,v) '||' (p,q);

      then u <> v implies (p,q,r,(p # q)) are_Ort_wrt (w,y) by A1, A6, A5, Lm10;

      hence thesis by A9, A6, A5, A8, A3;

    end;

    theorem :: GEOMTRAP:27

    

     Th27: Gen (w,y) & (u,v,u1,v1) are_DTr_wrt (w,y) implies ((u,v,(u # v1),(v # u1)) are_DTr_wrt (w,y) or (u,v,(v # u1),(u # v1)) are_DTr_wrt (w,y))

    proof

      assume that

       A1: Gen (w,y) and

       A2: (u,v,u1,v1) are_DTr_wrt (w,y);

      set p = (u # v1), q = (v # u1), r = (u # v), s = (u1 # v1);

      

       A3: (u,v,r,s) are_Ort_wrt (w,y) by A2;

      

       A4: (p # q) = (r # s) by Th6;

      then (r,s) // (r,(p # q)) by Th12;

      then

       A5: (r,s) '||' (r,(p # q));

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

      then

       A6: (u,v) '||' (p,q) by Lm2;

      then

       A7: (u,v) // (p,q) or (u,v) // (q,p);

      per cases ;

        suppose u = v;

        hence thesis by A1, A2, Th26;

      end;

        suppose that

         A8: u <> v;

        per cases ;

          suppose

           A9: r = s;

          then

           A10: (q,p,r,(q # p)) are_Ort_wrt (w,y) by A1, A4, Lm9;

          (u,v,r,(p # q)) are_Ort_wrt (w,y) & (p,q,r,(p # q)) are_Ort_wrt (w,y) by A1, A4, A9, Lm9;

          hence thesis by A7, A10;

        end;

          suppose r <> s;

          then

           A11: (u,v,r,(p # q)) are_Ort_wrt (w,y) by A1, A3, A5, Lm10;

          then (r,(p # q),p,q) are_Ort_wrt (w,y) by A1, A6, A8, Lm10;

          then (r,(p # q),q,p) are_Ort_wrt (w,y) by Lm4;

          then

           A12: (q,p,r,(q # p)) are_Ort_wrt (w,y) by Lm5;

          (p,q,r,(p # q)) are_Ort_wrt (w,y) by A1, A6, A8, A11, Lm10;

          hence thesis by A7, A11, A12;

        end;

      end;

    end;

    theorem :: GEOMTRAP:28

    

     Th28: for u,u1,u2,v1,v2,t1,t2,w1,w2 be VECTOR of V holds (u = (u1 # t1) & u = (u2 # t2) & u = (v1 # w1) & u = (v2 # w2) & (u1,u2,v1,v2) are_DTr_wrt (w,y) implies (t1,t2,w1,w2) are_DTr_wrt (w,y))

    proof

      let u,u1,u2,v1,v2,t1,t2,w1,w2 be VECTOR of V;

      assume that

       A1: u = (u1 # t1) & u = (u2 # t2) and

       A2: u = (v1 # w1) & u = (v2 # w2) and

       A3: (u1,u2,v1,v2) are_DTr_wrt (w,y);

      

       A4: (u1,u2) // (v1,v2) by A3;

      set p = (u1 # u2), q = (v1 # v2), r = (t1 # t2), s = (w1 # w2);

      

       A5: (q # s) = (u # u) by A2, Th6

      .= u;

      (p # r) = (u # u) by A1, Th6

      .= u;

      

      then

       A6: (s - r) = ( - (q - p)) by A5, Lm3

      .= (( - 1) * (q - p)) by RLVECT_1: 16;

      

       A7: (u2 - u1) = ( - (t2 - t1)) & (v2 - v1) = ( - (w2 - w1)) by A1, A2, Lm3;

      

       A8: (t1,t2) // (w1,w2)

      proof

        per cases ;

          suppose u1 = u2;

          then t1 = t2 by A1, Th7;

          hence thesis by ANALOAF: 9;

        end;

          suppose v1 = v2;

          then w1 = w2 by A2, Th7;

          hence thesis by ANALOAF: 9;

        end;

          suppose u1 <> u2 & v1 <> v2;

          then

          consider a, b such that

           A9: 0 < a & 0 < b and

           A10: (a * (u2 - u1)) = (b * (v2 - v1)) by A4, ANALOAF:def 1;

          (a * (t2 - t1)) = (a * ( - ( - (t2 - t1)))) by RLVECT_1: 17

          .= ( - (b * ( - (w2 - w1)))) by A7, A10, RLVECT_1: 25

          .= (b * ( - ( - (w2 - w1)))) by RLVECT_1: 25

          .= (b * (w2 - w1)) by RLVECT_1: 17;

          hence thesis by A9, ANALOAF:def 1;

        end;

      end;

      (w2 - w1) = ( - (v2 - v1)) by A2, Lm3;

      then

       A11: (w2 - w1) = (( - 1) * (v2 - v1)) by RLVECT_1: 16;

      (v1,v2,p,q) are_Ort_wrt (w,y) by A3;

      then ((v2 - v1),(q - p)) are_Ort_wrt (w,y) by ANALMETR:def 3;

      then ((w2 - w1),(s - r)) are_Ort_wrt (w,y) by A6, A11, ANALMETR: 6;

      then

       A12: (w1,w2,r,s) are_Ort_wrt (w,y) by ANALMETR:def 3;

      (t2 - t1) = ( - (u2 - u1)) by A1, Lm3;

      then

       A13: (t2 - t1) = (( - 1) * (u2 - u1)) by RLVECT_1: 16;

      (u1,u2,p,q) are_Ort_wrt (w,y) by A3;

      then ((u2 - u1),(q - p)) are_Ort_wrt (w,y) by ANALMETR:def 3;

      then ((t2 - t1),(s - r)) are_Ort_wrt (w,y) by A6, A13, ANALMETR: 6;

      then (t1,t2,r,s) are_Ort_wrt (w,y) by ANALMETR:def 3;

      hence thesis by A8, A12;

    end;

    

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

    proof

      assume

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

      

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

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

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

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

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

      

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

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

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

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

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

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

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

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

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

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

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

    end;

    

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

    proof

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

      

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

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

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

    end;

    

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

    proof

      assume that

       A1: Gen (w,y) and

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

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

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

      then (( - b1) + a1) = 0 & (( - b2) + a2) = 0 by A1, ANALMETR:def 1;

      hence thesis;

    end;

    definition

      let V, w, y, u;

      :: GEOMTRAP:def4

      func pr1 (w,y,u) -> Real means

      : Def4: ex b st u = ((it * w) + (b * y));

      existence by A1, ANALMETR:def 1;

      uniqueness by A1, Lm14;

    end

    definition

      let V, w, y, u;

      :: GEOMTRAP:def5

      func pr2 (w,y,u) -> Real means

      : Def5: ex a st u = ((a * w) + (it * y));

      existence

      proof

        consider a, b such that

         A2: u = ((a * w) + (b * y)) by A1, ANALMETR:def 1;

        take b;

        thus thesis by A2;

      end;

      uniqueness by A1, Lm14;

    end

    

     Lm15: Gen (w,y) implies u = ((( pr1 (w,y,u)) * w) + (( pr2 (w,y,u)) * y))

    proof

      assume

       A1: Gen (w,y);

      then

      consider b such that

       A2: u = ((( pr1 (w,y,u)) * w) + (b * y)) by Def4;

      thus thesis by A1, Def5, A2;

    end;

    

     Lm16: Gen (w,y) & u = ((a * w) + (b * y)) implies a = ( pr1 (w,y,u)) & b = ( pr2 (w,y,u))

    proof

      assume that

       A1: Gen (w,y) and

       A2: u = ((a * w) + (b * y));

      u = ((( pr1 (w,y,u)) * w) + (( pr2 (w,y,u)) * y)) by A1, Lm15;

      hence thesis by A1, A2, Lm14;

    end;

    

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

    proof

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

      assume

       A1: Gen (w,y);

      then

       A2: u = ((p1u * w) + (p2u * y)) by Lm15;

      

       A3: v = ((p1v * w) + (p2v * y)) by A1, Lm15;

      

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

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

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

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

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

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

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

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

      (a * u) = (((a * p1u) * w) + ((a * p2u) * y)) by A2, Lm13;

      hence thesis by A1, Lm16;

    end;

    

     Lm18: Gen (w,y) implies (2 * ( pr1 (w,y,(u # v)))) = (( pr1 (w,y,u)) + ( pr1 (w,y,v))) & (2 * ( pr2 (w,y,(u # v)))) = (( pr2 (w,y,u)) + ( pr2 (w,y,v)))

    proof

      assume

       A1: Gen (w,y);

      set p = (u # v);

      (2 * (u # v)) = ((1 + 1) * p)

      .= ((1 * p) + (1 * p)) by RLVECT_1:def 6

      .= (p + (1 * p)) by RLVECT_1:def 8

      .= (p + p) by RLVECT_1:def 8

      .= (u + v) by Def2;

      then (2 * ( pr1 (w,y,(u # v)))) = ( pr1 (w,y,(u + v))) & (2 * ( pr2 (w,y,(u # v)))) = ( pr2 (w,y,(u + v))) by A1, Lm17;

      hence thesis by A1, Lm17;

    end;

    

     Lm19: (( - u) + ( - v)) = ( - (u + v))

    proof

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

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

      .= ((v + ( 0. V)) + ( - v)) by RLVECT_1: 5

      .= (v + ( - v)) by RLVECT_1: 4

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

      hence thesis by RLVECT_1:def 10;

    end;

    

     Lm20: ((u2 + (a2 * v)) - (u1 + (a1 * v))) = ((u2 - u1) + ((a2 - a1) * v))

    proof

      

      thus ((u2 + (a2 * v)) - (u1 + (a1 * v))) = (((u2 + (a2 * v)) - u1) - (a1 * v)) by RLVECT_1: 27

      .= (((a2 * v) + (u2 - u1)) - (a1 * v)) by RLVECT_1:def 3

      .= ((u2 - u1) + ((a2 * v) - (a1 * v))) by RLVECT_1:def 3

      .= ((u2 - u1) + ((a2 - a1) * v)) by RLVECT_1: 35;

    end;

    definition

      let V, w, y, u, v;

      :: GEOMTRAP:def6

      func PProJ (w,y,u,v) -> Real equals ((( pr1 (w,y,u)) * ( pr1 (w,y,v))) + (( pr2 (w,y,u)) * ( pr2 (w,y,v))));

      correctness ;

    end

    theorem :: GEOMTRAP:29

    for u, v holds ( PProJ (w,y,u,v)) = ( PProJ (w,y,v,u));

    theorem :: GEOMTRAP:30

    

     Th30: Gen (w,y) implies for u, v, v1 holds ( PProJ (w,y,u,(v + v1))) = (( PProJ (w,y,u,v)) + ( PProJ (w,y,u,v1))) & ( PProJ (w,y,u,(v - v1))) = (( PProJ (w,y,u,v)) - ( PProJ (w,y,u,v1))) & ( PProJ (w,y,(v - v1),u)) = (( PProJ (w,y,v,u)) - ( PProJ (w,y,v1,u))) & ( PProJ (w,y,(v + v1),u)) = (( PProJ (w,y,v,u)) + ( PProJ (w,y,v1,u)))

    proof

      assume

       A1: Gen (w,y);

      let u,v,v1 be VECTOR of V;

       A2:

      now

        let u,v,v1 be VECTOR of V;

        

         A3: ( PProJ (w,y,u,(v - v1))) = ((( pr1 (w,y,u)) * (( pr1 (w,y,v)) - ( pr1 (w,y,v1)))) + (( pr2 (w,y,u)) * ( pr2 (w,y,(v - v1))))) by A1, Lm17

        .= ((( pr1 (w,y,u)) * (( pr1 (w,y,v)) - ( pr1 (w,y,v1)))) + (( pr2 (w,y,u)) * (( pr2 (w,y,v)) - ( pr2 (w,y,v1))))) by A1, Lm17

        .= (( PProJ (w,y,u,v)) - ( PProJ (w,y,u,v1)));

        ( PProJ (w,y,u,(v + v1))) = ((( pr1 (w,y,u)) * (( pr1 (w,y,v)) + ( pr1 (w,y,v1)))) + (( pr2 (w,y,u)) * ( pr2 (w,y,(v + v1))))) by A1, Lm17

        .= ((( pr1 (w,y,u)) * (( pr1 (w,y,v)) + ( pr1 (w,y,v1)))) + (( pr2 (w,y,u)) * (( pr2 (w,y,v)) + ( pr2 (w,y,v1))))) by A1, Lm17

        .= (( PProJ (w,y,u,v)) + ( PProJ (w,y,u,v1)));

        hence ( PProJ (w,y,u,(v + v1))) = (( PProJ (w,y,u,v)) + ( PProJ (w,y,u,v1))) & ( PProJ (w,y,u,(v - v1))) = (( PProJ (w,y,u,v)) - ( PProJ (w,y,u,v1))) by A3;

      end;

      hence ( PProJ (w,y,u,(v + v1))) = (( PProJ (w,y,u,v)) + ( PProJ (w,y,u,v1))) & ( PProJ (w,y,u,(v - v1))) = (( PProJ (w,y,u,v)) - ( PProJ (w,y,u,v1)));

      

      thus ( PProJ (w,y,(v - v1),u)) = ( PProJ (w,y,u,(v - v1)))

      .= (( PProJ (w,y,u,v)) - ( PProJ (w,y,u,v1))) by A2

      .= (( PProJ (w,y,v,u)) - ( PProJ (w,y,v1,u)));

      

      thus ( PProJ (w,y,(v + v1),u)) = ( PProJ (w,y,u,(v + v1)))

      .= (( PProJ (w,y,u,v)) + ( PProJ (w,y,u,v1))) by A2

      .= (( PProJ (w,y,v,u)) + ( PProJ (w,y,v1,u)));

    end;

    theorem :: GEOMTRAP:31

    

     Th31: Gen (w,y) implies for u,v be VECTOR of V, a be Real holds ( PProJ (w,y,(a * u),v)) = (a * ( PProJ (w,y,u,v))) & ( PProJ (w,y,u,(a * v))) = (a * ( PProJ (w,y,u,v))) & ( PProJ (w,y,(a * u),v)) = (( PProJ (w,y,u,v)) * a) & ( PProJ (w,y,u,(a * v))) = (( PProJ (w,y,u,v)) * a)

    proof

      assume

       A1: Gen (w,y);

       A2:

      now

        let u,v be VECTOR of V, a be Real;

        ( PProJ (w,y,(a * u),v)) = (((a * ( pr1 (w,y,u))) * ( pr1 (w,y,v))) + (( pr2 (w,y,(a * u))) * ( pr2 (w,y,v)))) by A1, Lm17

        .= (((a * ( pr1 (w,y,u))) * ( pr1 (w,y,v))) + ((a * ( pr2 (w,y,u))) * ( pr2 (w,y,v)))) by A1, Lm17

        .= (a * ( PProJ (w,y,u,v)));

        hence ( PProJ (w,y,(a * u),v)) = (a * ( PProJ (w,y,u,v)));

      end;

      let u,v be VECTOR of V, a be Real;

      thus ( PProJ (w,y,(a * u),v)) = (a * ( PProJ (w,y,u,v))) by A2;

      

      thus ( PProJ (w,y,u,(a * v))) = ( PProJ (w,y,(a * v),u))

      .= (a * ( PProJ (w,y,v,u))) by A2

      .= (a * ( PProJ (w,y,u,v)));

      thus ( PProJ (w,y,(a * u),v)) = (( PProJ (w,y,u,v)) * a) by A2;

      

      thus ( PProJ (w,y,u,(a * v))) = ( PProJ (w,y,(a * v),u))

      .= (a * ( PProJ (w,y,v,u))) by A2

      .= (( PProJ (w,y,u,v)) * a);

    end;

    theorem :: GEOMTRAP:32

    

     Th32: Gen (w,y) implies for u,v be VECTOR of V holds ((u,v) are_Ort_wrt (w,y) iff ( PProJ (w,y,u,v)) = 0 )

    proof

      assume

       A1: Gen (w,y);

      let u,v be VECTOR of V;

      set a1 = ( pr1 (w,y,u)), a2 = ( pr2 (w,y,u)), b1 = ( pr1 (w,y,v)), b2 = ( pr2 (w,y,v));

      u = ((a1 * w) + (a2 * y)) & v = ((b1 * w) + (b2 * y)) by A1, Lm15;

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

    end;

    theorem :: GEOMTRAP:33

    

     Th33: Gen (w,y) implies for u,v,u1,v1 be VECTOR of V holds ((u,v,u1,v1) are_Ort_wrt (w,y) iff ( PProJ (w,y,(v - u),(v1 - u1))) = 0 )

    proof

      assume

       A1: Gen (w,y);

      let u,v,u1,v1 be VECTOR of V;

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

      hence thesis by A1, Th32;

    end;

    theorem :: GEOMTRAP:34

    

     Th34: Gen (w,y) implies for u,v,v1 be VECTOR of V holds (2 * ( PProJ (w,y,u,(v # v1)))) = (( PProJ (w,y,u,v)) + ( PProJ (w,y,u,v1)))

    proof

      assume

       A1: Gen (w,y);

      let u,v,v1 be VECTOR of V;

      set a1 = ( pr1 (w,y,u)), a2 = ( pr2 (w,y,u)), b1 = ( pr1 (w,y,v)), b2 = ( pr2 (w,y,v)), c1 = ( pr1 (w,y,v1)), c2 = ( pr2 (w,y,v1));

      

      thus (2 * ( PProJ (w,y,u,(v # v1)))) = ((a1 * (2 * ( pr1 (w,y,(v # v1))))) + (2 * (a2 * ( pr2 (w,y,(v # v1))))))

      .= ((a1 * (b1 + c1)) + (a2 * (2 * ( pr2 (w,y,(v # v1)))))) by A1, Lm18

      .= ((a1 * (b1 + c1)) + (a2 * (b2 + c2))) by A1, Lm18

      .= (( PProJ (w,y,u,v)) + ( PProJ (w,y,u,v1)));

    end;

    theorem :: GEOMTRAP:35

    

     Th35: Gen (w,y) implies for u,v be VECTOR of V st u <> v holds ( PProJ (w,y,(u - v),(u - v))) <> 0

    proof

      assume

       A1: Gen (w,y);

      let u,v be VECTOR of V;

      assume

       A2: u <> v;

      assume ( PProJ (w,y,(u - v),(u - v))) = 0 ;

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

      then (u - v) = ( 0. V) by A1, ANALMETR: 11;

      hence contradiction by A2, RLVECT_1: 21;

    end;

    theorem :: GEOMTRAP:36

    

     Th36: Gen (w,y) implies for p,q,u,v,v9 be VECTOR of V, A be Real st (p,q,u,v) are_DTr_wrt (w,y) & p <> q & A = ((( PProJ (w,y,(p - q),(p + q))) - (2 * ( PProJ (w,y,(p - q),u)))) * (( PProJ (w,y,(p - q),(p - q))) " )) & v9 = (u + (A * (p - q))) holds v = v9

    proof

      assume

       A1: Gen (w,y);

      let p,q,u,v,v9 be VECTOR of V, A be Real;

      assume that

       A2: (p,q,u,v) are_DTr_wrt (w,y) and

       A3: p <> q and

       A4: A = ((( PProJ (w,y,(p - q),(p + q))) - (2 * ( PProJ (w,y,(p - q),u)))) * (( PProJ (w,y,(p - q),(p - q))) " )) and

       A5: v9 = (u + (A * (p - q)));

      

       A6: ( PProJ (w,y,(p - q),(p - q))) <> 0 by A1, A3, Th35;

      

       A7: ( PProJ (w,y,(p - q),(A * (p - q)))) = (((( PProJ (w,y,(p - q),(p + q))) - (2 * ( PProJ (w,y,(p - q),u)))) * (( PProJ (w,y,(p - q),(p - q))) " )) * ( PProJ (w,y,(p - q),(p - q)))) by A1, A4, Th31

      .= ((( PProJ (w,y,(p - q),(p + q))) - (2 * ( PProJ (w,y,(p - q),u)))) * ((( PProJ (w,y,(p - q),(p - q))) " ) * ( PProJ (w,y,(p - q),(p - q)))))

      .= ((( PProJ (w,y,(p - q),(p + q))) - (2 * ( PProJ (w,y,(p - q),u)))) * 1) by A6, XCMPLX_0:def 7

      .= (( PProJ (w,y,(p - q),(p + q))) - (2 * ( PProJ (w,y,(p - q),u))));

      set s = (p # q);

      set X = ( PProJ (w,y,(p - q),((v9 # u) - s)));

      (2 * X) = (2 * (( PProJ (w,y,(p - q),(v9 # u))) - ( PProJ (w,y,(p - q),(p # q))))) by A1, Th30

      .= ((2 * ( PProJ (w,y,(p - q),(v9 # u)))) - (2 * ( PProJ (w,y,(p - q),(p # q)))))

      .= ((( PProJ (w,y,(p - q),v9)) + ( PProJ (w,y,(p - q),u))) - (2 * ( PProJ (w,y,(p - q),(p # q))))) by A1, Th34

      .= ((( PProJ (w,y,(p - q),v9)) + ( PProJ (w,y,(p - q),u))) - (( PProJ (w,y,(p - q),p)) + ( PProJ (w,y,(p - q),q)))) by A1, Th34

      .= ((( PProJ (w,y,(p - q),(u + (A * (p - q))))) + ( PProJ (w,y,(p - q),u))) - ( PProJ (w,y,(p - q),(p + q)))) by A1, A5, Th30

      .= (((( PProJ (w,y,(p - q),u)) + ( PProJ (w,y,(p - q),(A * (p - q))))) + ( PProJ (w,y,(p - q),u))) - ( PProJ (w,y,(p - q),(p + q)))) by A1, Th30;

      then (q,p,(p # q),(v9 # u)) are_Ort_wrt (w,y) by A1, A7, Th33;

      then (s,(v9 # u),q,p) are_Ort_wrt (w,y) by Lm5;

      then

       A8: (s,(v9 # u),p,q) are_Ort_wrt (w,y) by Lm4;

      set Y = ( PProJ (w,y,(v9 - u),((v9 # u) - s)));

      

       A9: (v9 - u) = (A * (p - q)) by A5, RLSUB_2: 61;

      (1 * (v9 - u)) = ((u + (A * (p - q))) - u) by A5, RLVECT_1:def 8

      .= (A * (p - q)) by RLSUB_2: 61;

      then (q,p) // (u,v9) or (q,p) // (v9,u) by ANALMETR: 14;

      then

       A10: (p,q) // (u,v9) or (p,q) // (v9,u) by ANALOAF: 12;

      

       A11: ( PProJ (w,y,(A * (p - q)),(A * (p - q)))) = (A * ( PProJ (w,y,(p - q),(A * (p - q))))) by A1, Th31

      .= (A * (((( PProJ (w,y,(p - q),(p + q))) - (2 * ( PProJ (w,y,(p - q),u)))) * (( PProJ (w,y,(p - q),(p - q))) " )) * ( PProJ (w,y,(p - q),(p - q))))) by A1, A4, Th31

      .= (A * ((( PProJ (w,y,(p - q),(p + q))) - (2 * ( PProJ (w,y,(p - q),u)))) * ((( PProJ (w,y,(p - q),(p - q))) " ) * ( PProJ (w,y,(p - q),(p - q))))))

      .= (A * ((( PProJ (w,y,(p - q),(p + q))) - (2 * ( PProJ (w,y,(p - q),u)))) * 1)) by A6, XCMPLX_0:def 7

      .= (A * (( PProJ (w,y,(p - q),(p + q))) - (2 * ( PProJ (w,y,(p - q),u)))));

      (2 * Y) = (2 * (( PProJ (w,y,(v9 - u),(v9 # u))) - ( PProJ (w,y,(v9 - u),(p # q))))) by A1, Th30

      .= ((2 * ( PProJ (w,y,(v9 - u),(v9 # u)))) - (2 * ( PProJ (w,y,(v9 - u),(p # q)))))

      .= ((( PProJ (w,y,(v9 - u),v9)) + ( PProJ (w,y,(v9 - u),u))) - (2 * ( PProJ (w,y,(v9 - u),(p # q))))) by A1, Th34

      .= ((( PProJ (w,y,(v9 - u),v9)) + ( PProJ (w,y,(v9 - u),u))) - (( PProJ (w,y,(v9 - u),p)) + ( PProJ (w,y,(v9 - u),q)))) by A1, Th34

      .= ((( PProJ (w,y,(v9 - u),(u + (A * (p - q))))) + ( PProJ (w,y,(v9 - u),u))) - ( PProJ (w,y,(v9 - u),(p + q)))) by A1, A5, Th30

      .= (((( PProJ (w,y,(v9 - u),u)) + ( PProJ (w,y,(v9 - u),(A * (p - q))))) + ( PProJ (w,y,(v9 - u),u))) - ( PProJ (w,y,(v9 - u),(p + q)))) by A1, Th30;

      

      then

       A12: (2 * Y) = (((( PProJ (w,y,(A * (p - q)),u)) + ((A * ( PProJ (w,y,(p - q),(p + q)))) - (A * (2 * ( PProJ (w,y,(p - q),u)))))) + ( PProJ (w,y,(A * (p - q)),u))) - ( PProJ (w,y,(A * (p - q)),(p + q)))) by A9, A11

      .= (((( PProJ (w,y,(A * (p - q)),u)) + (( PProJ (w,y,(A * (p - q)),(p + q))) - (2 * (A * ( PProJ (w,y,(p - q),u)))))) + ( PProJ (w,y,(A * (p - q)),u))) - ( PProJ (w,y,(A * (p - q)),(p + q)))) by A1, Th31

      .= (((( PProJ (w,y,(A * (p - q)),u)) + (( PProJ (w,y,(A * (p - q)),(p + q))) - (2 * ( PProJ (w,y,(A * (p - q)),u))))) + ( PProJ (w,y,(A * (p - q)),u))) - ( PProJ (w,y,(A * (p - q)),(p + q)))) by A1, Th31

      .= 0 ;

      then (u,v9,s,(v9 # u)) are_Ort_wrt (w,y) by A1, Th33;

      then (s,(v9 # u),u,v9) are_Ort_wrt (w,y) by Lm5;

      then (s,(v9 # u),v9,u) are_Ort_wrt (w,y) by Lm4;

      then (p,q,s,(u # v9)) are_Ort_wrt (w,y) & (u,v9,s,(u # v9)) are_Ort_wrt (w,y) & (p,q,s,(v9 # u)) are_Ort_wrt (w,y) & (v9,u,s,(v9 # u)) are_Ort_wrt (w,y) by A1, A8, A12, Lm5, Th33;

      then (p,q,u,v9) are_DTr_wrt (w,y) or (p,q,v9,u) are_DTr_wrt (w,y) by A10;

      hence thesis by A1, A2, A3, Th25;

    end;

    

     Lm21: Gen (w,y) implies for u,u9,u1,u2,t1,t2 be VECTOR of V, A1,A2 be Real st A1 = ((( PProJ (w,y,(u - u9),(u + u9))) - (2 * ( PProJ (w,y,(u - u9),u1)))) * (( PProJ (w,y,(u - u9),(u - u9))) " )) & A2 = ((( PProJ (w,y,(u - u9),(u + u9))) - (2 * ( PProJ (w,y,(u - u9),u2)))) * (( PProJ (w,y,(u - u9),(u - u9))) " )) & t1 = (u1 + (A1 * (u - u9))) & t2 = (u2 + (A2 * (u - u9))) holds (t2 - t1) = ((u2 - u1) + ((A2 - A1) * (u - u9))) & (A2 - A1) = ((( - 2) * ( PProJ (w,y,(u - u9),(u2 - u1)))) * (( PProJ (w,y,(u - u9),(u - u9))) " ))

    proof

      assume

       A1: Gen (w,y);

      let u,u9,u1,u2,t1,t2 be VECTOR of V, A1,A2 be Real such that

       A2: A1 = ((( PProJ (w,y,(u - u9),(u + u9))) - (2 * ( PProJ (w,y,(u - u9),u1)))) * (( PProJ (w,y,(u - u9),(u - u9))) " )) & A2 = ((( PProJ (w,y,(u - u9),(u + u9))) - (2 * ( PProJ (w,y,(u - u9),u2)))) * (( PProJ (w,y,(u - u9),(u - u9))) " )) & t1 = (u1 + (A1 * (u - u9))) & t2 = (u2 + (A2 * (u - u9)));

      thus (t2 - t1) = ((u2 - u1) + ((A2 - A1) * (u - u9))) & (A2 - A1) = ((( - 2) * ( PProJ (w,y,(u - u9),(u2 - u1)))) * (( PProJ (w,y,(u - u9),(u - u9))) " ))

      proof

        set uu = ((( PProJ (w,y,(u - u9),(u + u9))) - (2 * ( PProJ (w,y,(u - u9),u2)))) - (( PProJ (w,y,(u - u9),(u + u9))) - (2 * ( PProJ (w,y,(u - u9),u1)))));

        

         A3: ((2 * u1) - (2 * u2)) = ( - ((2 * u2) - (2 * u1))) by RLVECT_1: 33

        .= ( - (2 * (u2 - u1))) by RLVECT_1: 34

        .= (2 * ( - (u2 - u1))) by RLVECT_1: 25

        .= (( - 2) * (u2 - u1)) by RLVECT_1: 24;

        uu = ((( PProJ (w,y,(u - u9),(u + u9))) - ( PProJ (w,y,(u - u9),(2 * u2)))) - (( PProJ (w,y,(u - u9),(u + u9))) - (2 * ( PProJ (w,y,(u - u9),u1))))) by A1, Th31

        .= ((( PProJ (w,y,(u - u9),(u + u9))) - ( PProJ (w,y,(u - u9),(2 * u2)))) - (( PProJ (w,y,(u - u9),(u + u9))) - ( PProJ (w,y,(u - u9),(2 * u1))))) by A1, Th31

        .= (( PProJ (w,y,(u - u9),(2 * u1))) - ( PProJ (w,y,(u - u9),(2 * u2))))

        .= ( PProJ (w,y,(u - u9),((2 * u1) - (2 * u2)))) by A1, Th30;

        then uu = (( - 2) * ( PProJ (w,y,(u - u9),(u2 - u1)))) by A1, A3, Th31;

        hence thesis by A2, Lm20, XCMPLX_1: 40;

      end;

    end;

    theorem :: GEOMTRAP:37

    

     Th37: Gen (w,y) implies for u,u9,u1,u2,v1,v2,t1,t2,w1,w2 be VECTOR of V st u <> u9 & (u,u9,u1,t1) are_DTr_wrt (w,y) & (u,u9,u2,t2) are_DTr_wrt (w,y) & (u,u9,v1,w1) are_DTr_wrt (w,y) & (u,u9,v2,w2) are_DTr_wrt (w,y) & (u1,u2) // (v1,v2) holds (t1,t2) // (w1,w2)

    proof

      assume

       A1: Gen (w,y);

      let u,u9,u1,u2,v1,v2,t1,t2,w1,w2 be VECTOR of V such that

       A2: u <> u9 and

       A3: (u,u9,u1,t1) are_DTr_wrt (w,y) & (u,u9,u2,t2) are_DTr_wrt (w,y) and

       A4: (u,u9,v1,w1) are_DTr_wrt (w,y) & (u,u9,v2,w2) are_DTr_wrt (w,y) and

       A5: (u1,u2) // (v1,v2);

      set A1 = ((( PProJ (w,y,(u - u9),(u + u9))) - (2 * ( PProJ (w,y,(u - u9),u1)))) * (( PProJ (w,y,(u - u9),(u - u9))) " )), A2 = ((( PProJ (w,y,(u - u9),(u + u9))) - (2 * ( PProJ (w,y,(u - u9),u2)))) * (( PProJ (w,y,(u - u9),(u - u9))) " )), A3 = ((( PProJ (w,y,(u - u9),(u + u9))) - (2 * ( PProJ (w,y,(u - u9),v1)))) * (( PProJ (w,y,(u - u9),(u - u9))) " )), A4 = ((( PProJ (w,y,(u - u9),(u + u9))) - (2 * ( PProJ (w,y,(u - u9),v2)))) * (( PProJ (w,y,(u - u9),(u - u9))) " ));

      

       A6: (u1 + (A1 * (u - u9))) = t1 & (u2 + (A2 * (u - u9))) = t2 by A1, A2, A3, Th36;

      

       A7: (v1 + (A3 * (u - u9))) = w1 & (v2 + (A4 * (u - u9))) = w2 by A1, A2, A4, Th36;

      

       A8: t1 = (u1 + (A1 * (u - u9))) & t2 = (u2 + (A2 * (u - u9))) by A1, A2, A3, Th36;

      per cases ;

        suppose u1 = u2;

        then t1 = t2 by A1, A2, A3, Th24;

        hence thesis by ANALOAF:def 1;

      end;

        suppose v1 = v2;

        then w1 = w2 by A1, A2, A4, Th24;

        hence thesis by ANALOAF:def 1;

      end;

        suppose that

         A9: u1 <> u2 & v1 <> v2;

        set cc = (( PProJ (w,y,(u - u9),(u - u9))) " );

        set vv = (( - 2) * ( PProJ (w,y,(u - u9),(v2 - v1))));

        set uu = (( - 2) * ( PProJ (w,y,(u - u9),(u2 - u1))));

        

         A10: (w2 - w1) = ((v2 - v1) + ((A4 - A3) * (u - u9))) by A1, A7, Lm21;

        consider a, b such that

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

         A12: 0 < a & 0 < b by A5, A9, ANALOAF: 7;

        

         A13: (a * uu) = (( - 2) * (a * ( PProJ (w,y,(u - u9),(u2 - u1)))))

        .= (( - 2) * ( PProJ (w,y,(u - u9),(b * (v2 - v1))))) by A1, A11, Th31

        .= (( - 2) * (b * ( PProJ (w,y,(u - u9),(v2 - v1))))) by A1, Th31

        .= (b * vv);

        

         A14: (a * (A2 - A1)) = (a * (uu * cc)) by A1, A8, Lm21

        .= ((b * vv) * cc) by A13, XCMPLX_1: 4

        .= (b * (vv * cc))

        .= (b * (A4 - A3)) by A1, A7, Lm21;

        (t2 - t1) = ((u2 - u1) + ((A2 - A1) * (u - u9))) by A1, A6, Lm21;

        

        then (a * (t2 - t1)) = ((a * (u2 - u1)) + (a * ((A2 - A1) * (u - u9)))) by RLVECT_1:def 5

        .= ((b * (v2 - v1)) + ((b * (A4 - A3)) * (u - u9))) by A11, A14, RLVECT_1:def 7

        .= ((b * (v2 - v1)) + (b * ((A4 - A3) * (u - u9)))) by RLVECT_1:def 7

        .= (b * (w2 - w1)) by A10, RLVECT_1:def 5;

        hence thesis by A12, ANALOAF:def 1;

      end;

    end;

    theorem :: GEOMTRAP:38

     Gen (w,y) implies for u,u9,u1,u2,v1,t1,t2,w1 be VECTOR of V st u <> u9 & (u,u9,u1,t1) are_DTr_wrt (w,y) & (u,u9,u2,t2) are_DTr_wrt (w,y) & (u,u9,v1,w1) are_DTr_wrt (w,y) & v1 = (u1 # u2) holds w1 = (t1 # t2)

    proof

      assume

       A1: Gen (w,y);

      let u,u9,u1,u2,v1,t1,t2,w1 be VECTOR of V such that

       A2: u <> u9 and

       A3: (u,u9,u1,t1) are_DTr_wrt (w,y) & (u,u9,u2,t2) are_DTr_wrt (w,y) and

       A4: (u,u9,v1,w1) are_DTr_wrt (w,y) and

       A5: v1 = (u1 # u2);

      set G = ( PProJ (w,y,(u - u9),(u + u9))), H = ( PProJ (w,y,(u - u9),u1)), W = ( PProJ (w,y,(u - u9),u2)), I = ( PProJ (w,y,(u - u9),v1)), N = ( PProJ (w,y,(u - u9),(u - u9)));

      set A1 = ((G - (2 * H)) * (N " )), A2 = ((G - (2 * W)) * (N " )), A3 = ((G - (2 * I)) * (N " ));

      

       A6: (H + W) = ( PProJ (w,y,(u - u9),(u1 + u2))) by A1, Th30

      .= ( PProJ (w,y,(u - u9),(v1 + v1))) by A5, Def2

      .= (I + I) by A1, Th30;

      (v1 + (A3 * (u - u9))) = w1 by A1, A2, A4, Th36;

      

      then

       A7: (w1 + w1) = ((A3 * (u - u9)) + (v1 + (v1 + (A3 * (u - u9))))) by RLVECT_1:def 3

      .= ((A3 * (u - u9)) + ((v1 + v1) + (A3 * (u - u9)))) by RLVECT_1:def 3

      .= ((v1 + v1) + ((A3 * (u - u9)) + (A3 * (u - u9)))) by RLVECT_1:def 3

      .= ((v1 + v1) + ((A3 + A3) * (u - u9))) by RLVECT_1:def 6;

      (u1 + (A1 * (u - u9))) = t1 & (u2 + (A2 * (u - u9))) = t2 by A1, A2, A3, Th36;

      

      then

       A8: (t1 + t2) = ((A1 * (u - u9)) + (u1 + (u2 + (A2 * (u - u9))))) by RLVECT_1:def 3

      .= ((A1 * (u - u9)) + ((u1 + u2) + (A2 * (u - u9)))) by RLVECT_1:def 3

      .= ((u1 + u2) + ((A1 * (u - u9)) + (A2 * (u - u9)))) by RLVECT_1:def 3

      .= ((u1 + u2) + ((A1 + A2) * (u - u9))) by RLVECT_1:def 6

      .= ((v1 + v1) + ((A1 + A2) * (u - u9))) by A5, Def2;

      set vv = ((G - (2 * I)) + (G - (2 * I)));

      (A1 + A2) = (((G - (2 * H)) + (G - (2 * W))) * (N " ))

      .= (vv * (N " )) by A6

      .= (A3 + A3);

      hence thesis by A8, A7, Def2;

    end;

    theorem :: GEOMTRAP:39

    

     Th39: Gen (w,y) implies for u,u9,u1,u2,t1,t2 be VECTOR of V st u <> u9 & (u,u9,u1,t1) are_DTr_wrt (w,y) & (u,u9,u2,t2) are_DTr_wrt (w,y) holds (u,u9,(u1 # u2),(t1 # t2)) are_DTr_wrt (w,y)

    proof

      assume

       A1: Gen (w,y);

      let u,u9,u1,u2,t1,t2 be VECTOR of V such that

       A2: u <> u9 and

       A3: (u,u9,u1,t1) are_DTr_wrt (w,y) and

       A4: (u,u9,u2,t2) are_DTr_wrt (w,y);

      (u1,t1,u2,t2) are_DTr_wrt (w,y) by A1, A2, A3, A4, Th19;

      then

       A5: (u1,t1,(u1 # u2),(t1 # t2)) are_DTr_wrt (w,y) by A1, Th26;

      (u2,t2,u1,t1) are_DTr_wrt (w,y) by A1, A2, A3, A4, Th19;

      then

       A6: (u2,t2,(u2 # u1),(t2 # t1)) are_DTr_wrt (w,y) by A1, Th26;

      per cases ;

        suppose

         A7: u1 <> t1;

        (u1,t1,u,u9) are_DTr_wrt (w,y) by A3, Th21;

        hence thesis by A1, A5, A7, Th19;

      end;

        suppose

         A8: u2 <> t2;

        (u2,t2,u,u9) are_DTr_wrt (w,y) by A4, Th21;

        hence thesis by A1, A6, A8, Th19;

      end;

        suppose that

         A9: u1 = t1 and

         A10: u2 = t2;

        ((u # u9),((u1 # u2) # (t1 # t2)),(u1 # u2),(t1 # t2)) are_Ort_wrt (w,y) by A1, A9, A10, Lm6;

        then

         A11: ((u1 # u2),(t1 # t2),(u # u9),((u1 # u2) # (t1 # t2))) are_Ort_wrt (w,y) by Lm5;

        

         A12: (u,u9,(u # u9),(u1 # u2)) are_Ort_wrt (w,y)

        proof

          set uu9 = (u # u9);

          

           A13: (2 * (u1 # u2)) = ((1 + 1) * (u1 # u2))

          .= ((1 * (u1 # u2)) + (1 * (u1 # u2))) by RLVECT_1:def 6

          .= ((u1 # u2) + (1 * (u1 # u2))) by RLVECT_1:def 8

          .= ((u1 # u2) + (u1 # u2)) by RLVECT_1:def 8

          .= (u1 + u2) by Def2;

          

           A14: ( - (2 * uu9)) = ( - ((1 + 1) * uu9))

          .= ( - ((1 * uu9) + (1 * uu9))) by RLVECT_1:def 6

          .= ( - (uu9 + (1 * uu9))) by RLVECT_1:def 8

          .= ( - (uu9 + uu9)) by RLVECT_1:def 8

          .= (( - uu9) + ( - uu9)) by Lm19;

          (u,u9,uu9,(u2 # t2)) are_Ort_wrt (w,y) by A4;

          then ((u9 - u),(u2 - uu9)) are_Ort_wrt (w,y) by A10, ANALMETR:def 3;

          then

           A15: ((u9 - u),((2 " ) * (u2 - uu9))) are_Ort_wrt (w,y) by ANALMETR: 7;

          (u,u9,uu9,(u1 # t1)) are_Ort_wrt (w,y) by A3;

          then ((u9 - u),(u1 - uu9)) are_Ort_wrt (w,y) by A9, ANALMETR:def 3;

          then

           A16: ((u9 - u),((2 " ) * (u1 - uu9))) are_Ort_wrt (w,y) by ANALMETR: 7;

          ((u1 # u2) - uu9) = (((2 " ) * 2) * ((u1 # u2) - uu9)) by RLVECT_1:def 8

          .= ((2 " ) * (2 * ((u1 # u2) - uu9))) by RLVECT_1:def 7

          .= ((2 " ) * ((u1 + u2) - (2 * uu9))) by A13, RLVECT_1: 34

          .= ((2 " ) * (((u1 + u2) + ( - uu9)) + ( - uu9))) by A14, RLVECT_1:def 3

          .= ((2 " ) * (((u1 - uu9) + u2) + ( - uu9))) by RLVECT_1:def 3

          .= ((2 " ) * ((u1 - uu9) + (u2 - uu9))) by RLVECT_1:def 3

          .= (((2 " ) * (u1 - uu9)) + ((2 " ) * (u2 - uu9))) by RLVECT_1:def 5;

          then ((u9 - u),((u1 # u2) - uu9)) are_Ort_wrt (w,y) by A1, A16, A15, ANALMETR: 10;

          hence thesis by ANALMETR:def 3;

        end;

        (u,u9) // ((u1 # u2),(t1 # t2)) by A9, A10, ANALOAF: 9;

        hence thesis by A9, A10, A11, A12;

      end;

    end;

    theorem :: GEOMTRAP:40

    

     Th40: Gen (w,y) implies for u,u9,u1,u2,v1,v2,t1,t2,w1,w2 be VECTOR of V st u <> u9 & (u,u9,u1,t1) are_DTr_wrt (w,y) & (u,u9,u2,t2) are_DTr_wrt (w,y) & (u,u9,v1,w1) are_DTr_wrt (w,y) & (u,u9,v2,w2) are_DTr_wrt (w,y) & (u1,u2,v1,v2) are_Ort_wrt (w,y) holds (t1,t2,w1,w2) are_Ort_wrt (w,y)

    proof

      assume

       A1: Gen (w,y);

      let u,u9,u1,u2,v1,v2,t1,t2,w1,w2 be VECTOR of V such that

       A2: u <> u9 and

       A3: (u,u9,u1,t1) are_DTr_wrt (w,y) & (u,u9,u2,t2) are_DTr_wrt (w,y) and

       A4: (u,u9,v1,w1) are_DTr_wrt (w,y) & (u,u9,v2,w2) are_DTr_wrt (w,y) and

       A5: (u1,u2,v1,v2) are_Ort_wrt (w,y);

      set A1 = ((( PProJ (w,y,(u - u9),(u + u9))) - (2 * ( PProJ (w,y,(u - u9),u1)))) * (( PProJ (w,y,(u - u9),(u - u9))) " )), A2 = ((( PProJ (w,y,(u - u9),(u + u9))) - (2 * ( PProJ (w,y,(u - u9),u2)))) * (( PProJ (w,y,(u - u9),(u - u9))) " )), A3 = ((( PProJ (w,y,(u - u9),(u + u9))) - (2 * ( PProJ (w,y,(u - u9),v1)))) * (( PProJ (w,y,(u - u9),(u - u9))) " )), A4 = ((( PProJ (w,y,(u - u9),(u + u9))) - (2 * ( PProJ (w,y,(u - u9),v2)))) * (( PProJ (w,y,(u - u9),(u - u9))) " ));

      (u1 + (A1 * (u - u9))) = t1 & (u2 + (A2 * (u - u9))) = t2 by A1, A2, A3, Th36;

      then

       A6: (t2 - t1) = ((u2 - u1) + ((A2 - A1) * (u - u9))) by A1, Lm21;

      

       A7: t1 = (u1 + (A1 * (u - u9))) & t2 = (u2 + (A2 * (u - u9))) by A1, A2, A3, Th36;

      

       A8: (v1 + (A3 * (u - u9))) = w1 & (v2 + (A4 * (u - u9))) = w2 by A1, A2, A4, Th36;

      then (w2 - w1) = ((v2 - v1) + ((A4 - A3) * (u - u9))) by A1, Lm21;

      

      then

       A9: ( PProJ (w,y,(t2 - t1),(w2 - w1))) = (( PProJ (w,y,(u2 - u1),((v2 - v1) + ((A4 - A3) * (u - u9))))) + ( PProJ (w,y,((A2 - A1) * (u - u9)),((v2 - v1) + ((A4 - A3) * (u - u9)))))) by A1, A6, Th30

      .= ((( PProJ (w,y,(u2 - u1),(v2 - v1))) + ( PProJ (w,y,(u2 - u1),((A4 - A3) * (u - u9))))) + ( PProJ (w,y,((A2 - A1) * (u - u9)),((v2 - v1) + ((A4 - A3) * (u - u9)))))) by A1, Th30

      .= (( 0 + ( PProJ (w,y,(u2 - u1),((A4 - A3) * (u - u9))))) + ( PProJ (w,y,((A2 - A1) * (u - u9)),((v2 - v1) + ((A4 - A3) * (u - u9)))))) by A1, A5, Th33

      .= (( PProJ (w,y,(u2 - u1),((A4 - A3) * (u - u9)))) + (( PProJ (w,y,((A2 - A1) * (u - u9)),(v2 - v1))) + ( PProJ (w,y,((A2 - A1) * (u - u9)),((A4 - A3) * (u - u9)))))) by A1, Th30;

      set aa = ((( PProJ (w,y,(u - u9),(u - u9))) " ) * (( PProJ (w,y,(u - u9),(u2 - u1))) * ( PProJ (w,y,(u - u9),(v2 - v1)))));

      

       A10: ( PProJ (w,y,((A2 - A1) * (u - u9)),(v2 - v1))) = ( PProJ (w,y,(v2 - v1),((A2 - A1) * (u - u9))))

      .= (( PProJ (w,y,(v2 - v1),(u - u9))) * (A2 - A1)) by A1, Th31

      .= (( PProJ (w,y,(v2 - v1),(u - u9))) * ((( - 2) * ( PProJ (w,y,(u - u9),(u2 - u1)))) * (( PProJ (w,y,(u - u9),(u - u9))) " ))) by A1, A7, Lm21

      .= (( - 2) * aa);

      

       A11: ( PProJ (w,y,(u - u9),(u - u9))) <> 0 by A1, A2, Th35;

      

       A12: ( PProJ (w,y,(u2 - u1),((A4 - A3) * (u - u9)))) = (( PProJ (w,y,(u2 - u1),(u - u9))) * (A4 - A3)) by A1, Th31

      .= (( PProJ (w,y,(u2 - u1),(u - u9))) * ((( - 2) * ( PProJ (w,y,(u - u9),(v2 - v1)))) * (( PProJ (w,y,(u - u9),(u - u9))) " ))) by A1, A8, Lm21

      .= (( - 2) * aa);

      ( PProJ (w,y,((A2 - A1) * (u - u9)),((A4 - A3) * (u - u9)))) = ((A2 - A1) * ( PProJ (w,y,(u - u9),((A4 - A3) * (u - u9))))) by A1, Th31

      .= ((A2 - A1) * ((A4 - A3) * ( PProJ (w,y,(u - u9),(u - u9))))) by A1, Th31

      .= ((A2 - A1) * (((( - 2) * ( PProJ (w,y,(u - u9),(v2 - v1)))) * (( PProJ (w,y,(u - u9),(u - u9))) " )) * ( PProJ (w,y,(u - u9),(u - u9))))) by A1, A8, Lm21

      .= ((A2 - A1) * ((( - 2) * ( PProJ (w,y,(u - u9),(v2 - v1)))) * ((( PProJ (w,y,(u - u9),(u - u9))) " ) * ( PProJ (w,y,(u - u9),(u - u9))))))

      .= ((A2 - A1) * ((( - 2) * ( PProJ (w,y,(u - u9),(v2 - v1)))) * 1)) by A11, XCMPLX_0:def 7

      .= ((( - 2) * (A2 - A1)) * ( PProJ (w,y,(u - u9),(v2 - v1))))

      .= ((( - 2) * ((( - 2) * ( PProJ (w,y,(u - u9),(u2 - u1)))) * (( PProJ (w,y,(u - u9),(u - u9))) " ))) * ( PProJ (w,y,(u - u9),(v2 - v1)))) by A1, A7, Lm21

      .= (4 * aa);

      hence thesis by A1, A9, A12, A10, Th33;

    end;

    theorem :: GEOMTRAP:41

    

     Th41: for u,u9,u1,u2,v1,v2,t1,t2,w1,w2 be VECTOR of V holds ( Gen (w,y) & u <> u9 & (u,u9,u1,t1) are_DTr_wrt (w,y) & (u,u9,u2,t2) are_DTr_wrt (w,y) & (u,u9,v1,w1) are_DTr_wrt (w,y) & (u,u9,v2,w2) are_DTr_wrt (w,y) & (u1,u2,v1,v2) are_DTr_wrt (w,y) implies (t1,t2,w1,w2) are_DTr_wrt (w,y))

    proof

      let u,u9,u1,u2,v1,v2,t1,t2,w1,w2 be VECTOR of V;

      assume that

       A1: Gen (w,y) & u <> u9 and

       A2: (u,u9,u1,t1) are_DTr_wrt (w,y) & (u,u9,u2,t2) are_DTr_wrt (w,y) and

       A3: (u,u9,v1,w1) are_DTr_wrt (w,y) & (u,u9,v2,w2) are_DTr_wrt (w,y) and

       A4: (u1,u2,v1,v2) are_DTr_wrt (w,y);

      set uu = (u1 # u2), vv = (v1 # v2);

      

       A5: (u,u9,uu,(t1 # t2)) are_DTr_wrt (w,y) & (u,u9,vv,(w1 # w2)) are_DTr_wrt (w,y) by A1, A2, A3, Th39;

      (v1,v2,uu,vv) are_Ort_wrt (w,y) by A4;

      then

       A6: (w1,w2,(t1 # t2),(w1 # w2)) are_Ort_wrt (w,y) by A1, A3, A5, Th40;

      (u1,u2,uu,vv) are_Ort_wrt (w,y) by A4;

      then

       A7: (t1,t2,(t1 # t2),(w1 # w2)) are_Ort_wrt (w,y) by A1, A2, A5, Th40;

      (u1,u2) // (v1,v2) by A4;

      then (t1,t2) // (w1,w2) by A1, A2, A3, Th37;

      hence thesis by A7, A6;

    end;

    definition

      let V;

      let w, y;

      :: GEOMTRAP:def7

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

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

      existence

      proof

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

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

        consider P be Relation of VV, VV such that

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

        take P;

        let x,z be object;

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

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

        hence thesis by A1;

      end;

      uniqueness

      proof

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

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

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

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

        proof

          let x,z be object;

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

          hence thesis by A3;

        end;

        hence thesis by RELAT_1:def 2;

      end;

    end

    theorem :: GEOMTRAP:42

    

     Th42: [ [u, v], [u1, v1]] in ( DTrapezium (V,w,y)) iff (u,v,u1,v1) are_DTr_wrt (w,y)

    proof

      now

        assume [ [u, v], [u1, v1]] in ( DTrapezium (V,w,y));

        then

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

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

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

         A3: (u9,v9,u19,v19) are_DTr_wrt (w,y) by Def7;

        

         A4: u1 = u19 by A2, XTUPLE_0: 1;

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

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

      end;

      hence thesis by Def7;

    end;

    definition

      let V;

      :: GEOMTRAP:def8

      func MidPoint (V) -> BinOp of the carrier of V means

      : Def8: for u, v holds (it . (u,v)) = (u # v);

      existence

      proof

        deffunc F( VECTOR of V, VECTOR of V) = ($1 # $2);

        ex B be BinOp of the carrier of V st for u, v holds (B . (u,v)) = F(u,v) from BINOP_1:sch 4;

        hence thesis;

      end;

      uniqueness

      proof

        deffunc F( VECTOR of V, VECTOR of V) = ($1 # $2);

        for o1,o2 be BinOp of the carrier of V st (for a,b be Element of V holds (o1 . (a,b)) = F(a,b)) & (for a,b be Element of V holds (o2 . (a,b)) = F(a,b)) holds o1 = o2 from BINOP_2:sch 2;

        hence thesis;

      end;

    end

    definition

      struct ( AffinStruct, MidStr) AfMidStruct (# the carrier -> set,

the MIDPOINT -> BinOp of the carrier,

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

       attr strict strict;

    end

    registration

      cluster non empty strict for AfMidStruct;

      existence

      proof

        set D = the non empty set, m = the BinOp of D, c = the Relation of [:D, D:];

        take AfMidStruct (# D, m, c #);

        thus the carrier of AfMidStruct (# D, m, c #) is non empty;

        thus thesis;

      end;

    end

    definition

      let V, w, y;

      :: GEOMTRAP:def9

      func DTrSpace (V,w,y) -> strict AfMidStruct equals AfMidStruct (# the carrier of V, ( MidPoint V), ( DTrapezium (V,w,y)) #);

      correctness ;

    end

    registration

      let V, w, y;

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

      coherence ;

    end

    definition

      ::$Canceled

    end

    registration

      let AMS be non empty AfMidStruct;

      cluster the AffinStruct of AMS -> non empty;

      coherence ;

    end

    definition

      let AMS be non empty AfMidStruct, a,b be Element of AMS;

      :: GEOMTRAP:def11

      func a # b -> Element of AMS equals (the MIDPOINT of AMS . (a,b));

      correctness ;

    end

    reserve a,b,c,d,a1,a2,b1,c1,d1,d2,p,q for Element of ( DTrSpace (V,w,y));

    theorem :: GEOMTRAP:43

    for x be set holds x is Element of the carrier of ( DTrSpace (V,w,y)) iff x is VECTOR of V;

    theorem :: GEOMTRAP:44

    

     Th44: u = a & v = b & u1 = a1 & v1 = b1 implies ((a,b) // (a1,b1) iff (u,v,u1,v1) are_DTr_wrt (w,y))

    proof

      assume

       A1: u = a & v = b & u1 = a1 & v1 = b1;

      hereby

        assume (a,b) // (a1,b1);

        then [ [a, b], [a1, b1]] in ( DTrapezium (V,w,y)) by ANALOAF:def 2;

        hence (u,v,u1,v1) are_DTr_wrt (w,y) by A1, Th42;

      end;

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

      then [ [a, b], [a1, b1]] in ( DTrapezium (V,w,y)) by A1, Th42;

      hence (a,b) // (a1,b1) by ANALOAF:def 2;

    end;

    theorem :: GEOMTRAP:45

     Gen (w,y) & u = a & v = b implies (u # v) = (a # b) by Def8;

    

     Lm22: Gen (w,y) & (a,b) // (b,c) implies a = b & b = c

    proof

      assume that

       A1: Gen (w,y) and

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

      reconsider u = a, v = b, u1 = c as VECTOR of V;

      (u,v,v,u1) are_DTr_wrt (w,y) by A2, Th44;

      hence thesis by A1, Th18;

    end;

    

     Lm23: Gen (w,y) & (a,b) // (a1,b1) & (a,b) // (c1,d1) & a <> b implies (a1,b1) // (c1,d1)

    proof

      assume that

       A1: Gen (w,y) and

       A2: (a,b) // (a1,b1) & (a,b) // (c1,d1) and

       A3: a <> b;

      reconsider u = a, v = b, u1 = a1, v1 = b1, u2 = c1, v2 = d1 as VECTOR of V;

      (u,v,u1,v1) are_DTr_wrt (w,y) & (u,v,u2,v2) are_DTr_wrt (w,y) by A2, Th44;

      then (u1,v1,u2,v2) are_DTr_wrt (w,y) by A1, A3, Th19;

      hence thesis by Th44;

    end;

    

     Lm24: (a,b) // (c,d) implies (c,d) // (a,b) & (b,a) // (d,c)

    proof

      reconsider u = a, v = b, u1 = c, v1 = d as VECTOR of V;

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

      then (u,v,u1,v1) are_DTr_wrt (w,y) by Th44;

      then (v,u,v1,u1) are_DTr_wrt (w,y) & (u1,v1,u,v) are_DTr_wrt (w,y) by Th21, Th22;

      hence thesis by Th44;

    end;

    

     Lm25: Gen (w,y) implies ex d st (a,b) // (c,d) or (a,b) // (d,c)

    proof

      reconsider u = a, v = b, u1 = c as VECTOR of V;

      assume Gen (w,y);

      then

      consider t be VECTOR of V such that

       A1: (u,v,u1,t) are_DTr_wrt (w,y) or (u,v,t,u1) are_DTr_wrt (w,y) by Th20;

      reconsider d = t as Element of ( DTrSpace (V,w,y));

      (a,b) // (c,d) or (a,b) // (d,c) by A1, Th44;

      hence thesis;

    end;

    

     Lm26: Gen (w,y) & (a,b) // (c,d1) & (a,b) // (c,d2) implies a = b or d1 = d2

    proof

      assume that

       A1: Gen (w,y) and

       A2: (a,b) // (c,d1) & (a,b) // (c,d2);

      reconsider u = a, v = b, u1 = c, v1 = d1, v2 = d2 as VECTOR of V;

      (u,v,u1,v1) are_DTr_wrt (w,y) & (u,v,u1,v2) are_DTr_wrt (w,y) by A2, Th44;

      hence thesis by A1, Th24;

    end;

    

     Lm27: (a # b) = (b # a)

    proof

      reconsider u = a, v = b as VECTOR of V;

      

      thus (a # b) = (u # v) by Def8

      .= (b # a) by Def8;

    end;

    

     Lm28: (a # a) = a

    proof

      reconsider u = a as VECTOR of V;

      (u # u) = u;

      hence thesis by Def8;

    end;

    

     Lm29: ((a # b) # (c # d)) = ((a # c) # (b # d))

    proof

      reconsider u = a, u1 = b, v = c, v1 = d as VECTOR of V;

      set ab = (a # b), cd = (c # d), ac = (a # c), bd = (b # d), uu1 = (u # u1), vv1 = (v # v1), uv = (u # v), u1v1 = (u1 # v1);

      

       A1: ac = uv & bd = u1v1 by Def8;

      ab = uu1 & cd = vv1 by Def8;

      

      hence (ab # cd) = (uu1 # vv1) by Def8

      .= (uv # u1v1) by Th6

      .= (ac # bd) by A1, Def8;

    end;

    

     Lm30: ex p st (p # a) = b

    proof

      reconsider u = a, v = b as VECTOR of V;

      consider u1 such that

       A1: (u # u1) = v by Th5;

      reconsider p = u1 as Element of ( DTrSpace (V,w,y));

      (p # a) = (u # u1) by Def8;

      hence thesis by A1;

    end;

    

     Lm31: (a # a1) = (a # a2) implies a1 = a2

    proof

      assume

       A1: (a # a1) = (a # a2);

      reconsider u = a, u1 = a1, u2 = a2 as VECTOR of V;

      (u # u1) = (a # a1) & (u # u2) = (a # a2) by Def8;

      hence thesis by A1, Th7;

    end;

    

     Lm32: Gen (w,y) & (a,b) // (c,d) implies (a,b) // ((a # c),(b # d))

    proof

      assume that

       A1: Gen (w,y) and

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

      reconsider u = a, v = b, u1 = c, v1 = d as VECTOR of V;

      (u,v,u1,v1) are_DTr_wrt (w,y) by A2, Th44;

      then

       A3: (u,v,(u # u1),(v # v1)) are_DTr_wrt (w,y) by A1, Th26;

      (a # c) = (u # u1) & (b # d) = (v # v1) by Def8;

      hence thesis by A3, Th44;

    end;

    

     Lm33: Gen (w,y) & (a,b) // (c,d) implies ((a,b) // ((a # d),(b # c)) or (a,b) // ((b # c),(a # d)))

    proof

      assume that

       A1: Gen (w,y) and

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

      reconsider u = a, v = b, u1 = c, v1 = d as VECTOR of V;

      (u,v,u1,v1) are_DTr_wrt (w,y) by A2, Th44;

      then

       A3: (u,v,(u # v1),(v # u1)) are_DTr_wrt (w,y) or (u,v,(v # u1),(u # v1)) are_DTr_wrt (w,y) by A1, Th27;

      (a # d) = (u # v1) & (b # c) = (v # u1) by Def8;

      hence thesis by A3, Th44;

    end;

    

     Lm34: (a,b) // (c,d) & (a # a1) = p & (b # b1) = p & (c # c1) = p & (d # d1) = p implies (a1,b1) // (c1,d1)

    proof

      assume that

       A1: (a,b) // (c,d) & (a # a1) = p and

       A2: (b # b1) = p & (c # c1) = p and

       A3: (d # d1) = p;

      reconsider u1 = a, u2 = b, v1 = c, v2 = d, u = p, t1 = a1, t2 = b1, w1 = c1, w2 = d1 as VECTOR of V;

      

       A4: u = (u2 # t2) & u = (v1 # w1) by A2, Def8;

      

       A5: u = (v2 # w2) by A3, Def8;

      (u1,u2,v1,v2) are_DTr_wrt (w,y) & u = (u1 # t1) by A1, Def8, Th44;

      then (t1,t2,w1,w2) are_DTr_wrt (w,y) by A4, A5, Th28;

      hence thesis by Th44;

    end;

    

     Lm35: Gen (w,y) & p <> q & (p,q) // (a,a1) & (p,q) // (b,b1) & (p,q) // (c,c1) & (p,q) // (d,d1) & (a,b) // (c,d) implies (a1,b1) // (c1,d1)

    proof

      assume that

       A1: Gen (w,y) & p <> q and

       A2: (p,q) // (a,a1) & (p,q) // (b,b1) and

       A3: (p,q) // (c,c1) & (p,q) // (d,d1) and

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

      reconsider u = p, u9 = q, u1 = a, u2 = b, v1 = c, v2 = d, t1 = a1, t2 = b1, w1 = c1, w2 = d1 as VECTOR of V;

      

       A5: (u,u9,v1,w1) are_DTr_wrt (w,y) & (u,u9,v2,w2) are_DTr_wrt (w,y) by A3, Th44;

      

       A6: (u1,u2,v1,v2) are_DTr_wrt (w,y) by A4, Th44;

      (u,u9,u1,t1) are_DTr_wrt (w,y) & (u,u9,u2,t2) are_DTr_wrt (w,y) by A2, Th44;

      then (t1,t2,w1,w2) are_DTr_wrt (w,y) by A1, A5, A6, Th41;

      hence thesis by Th44;

    end;

    definition

      let IT be non empty AfMidStruct;

      :: GEOMTRAP:def12

      attr IT is MidOrdTrapSpace-like means

      : Def11: for a,b,c,d,a1,b1,c1,d1,p,q be Element of IT holds (a # b) = (b # a) & (a # a) = a & ((a # b) # (c # d)) = ((a # c) # (b # d)) & (ex p be Element of IT st (p # a) = b) & ((a # b) = (a # c) implies b = c) & ((a,b) // (c,d) implies (a,b) // ((a # c),(b # d))) & ((a,b) // (c,d) implies ((a,b) // ((a # d),(b # c)) or (a,b) // ((b # c),(a # d)))) & ((a,b) // (c,d) & (a # a1) = p & (b # b1) = p & (c # c1) = p & (d # d1) = p implies (a1,b1) // (c1,d1)) & (p <> q & (p,q) // (a,a1) & (p,q) // (b,b1) & (p,q) // (c,c1) & (p,q) // (d,d1) & (a,b) // (c,d) implies (a1,b1) // (c1,d1)) & ((a,b) // (b,c) implies a = b & b = c) & ((a,b) // (a1,b1) & (a,b) // (c1,d1) & a <> b implies (a1,b1) // (c1,d1)) & ((a,b) // (c,d) implies (c,d) // (a,b) & (b,a) // (d,c)) & (ex d be Element of IT st (a,b) // (c,d) or (a,b) // (d,c)) & ((a,b) // (c,p) & (a,b) // (c,q) implies a = b or p = q);

    end

    registration

      cluster strict MidOrdTrapSpace-like for non empty AfMidStruct;

      existence

      proof

        consider V such that

         A1: ex w, y st Gen (w,y) by ANALMETR: 3;

        consider w,y be VECTOR of V such that

         A2: Gen (w,y) by A1;

        set X = ( DTrSpace (V,w,y));

        X is MidOrdTrapSpace-like by Lm27, Lm28, Lm29, Lm30, Lm31, A2, Lm32, Lm33, Lm34, Lm35, Lm22, Lm23, Lm24, Lm25, Lm26;

        hence thesis;

      end;

    end

    definition

      mode MidOrdTrapSpace is MidOrdTrapSpace-like non empty AfMidStruct;

    end

    theorem :: GEOMTRAP:46

     Gen (w,y) implies ( DTrSpace (V,w,y)) is MidOrdTrapSpace

    proof

      set X = ( DTrSpace (V,w,y));

      assume

       A1: Gen (w,y);

      X is MidOrdTrapSpace-like by Lm27, Lm28, Lm29, Lm30, Lm31, A1, Lm32, Lm33, Lm34, Lm35, Lm22, Lm23, Lm24, Lm25, Lm26;

      hence thesis;

    end;

    set MOS = the MidOrdTrapSpace;

    set X = the AffinStruct of MOS;

     Lm36:

    now

      let a,b,c,d,a1,b1,c1,d1,p,q be Element of X;

      reconsider a9 = a, b9 = b, c9 = c, d9 = d, a19 = a1, b19 = b1, c19 = c1, d19 = d1, p9 = p, q9 = q as Element of MOS;

       A1:

      now

        let a,b,c,d be Element of X, a9,b9,c9,d9 be Element of the carrier of MOS such that

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

         A3:

        now

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

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

          hence (a,b) // (c,d) by ANALOAF:def 2;

        end;

        now

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

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

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

        end;

        hence (a,b) // (c,d) iff (a9,b9) // (c9,d9) by A3;

      end;

      hereby

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

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

        hence a = b & b = c by Def11;

      end;

      hereby

        assume that

         A4: (a,b) // (a1,b1) & (a,b) // (c1,d1) and

         A5: a <> b;

        (a9,b9) // (a19,b19) & (a9,b9) // (c19,d19) by A1, A4;

        then (a19,b19) // (c19,d19) by A5, Def11;

        hence (a1,b1) // (c1,d1) by A1;

      end;

      hereby

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

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

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

        hence (c,d) // (a,b) & (b,a) // (d,c) by A1;

      end;

      thus ex d be Element of X st (a,b) // (c,d) or (a,b) // (d,c)

      proof

        consider x9 be Element of MOS such that

         A6: (a9,b9) // (c9,x9) or (a9,b9) // (x9,c9) by Def11;

        reconsider x = x9 as Element of X;

        take x;

        thus thesis by A1, A6;

      end;

      assume (a,b) // (c,p) & (a,b) // (c,q);

      then (a9,b9) // (c9,p9) & (a9,b9) // (c9,q9) by A1;

      hence a = b or p = q by Def11;

    end;

    definition

      let IT be non empty AffinStruct;

      :: GEOMTRAP:def13

      attr IT is OrdTrapSpace-like means

      : Def12: for a,b,c,d,a1,b1,c1,d1,p,q be Element of IT holds ((a,b) // (b,c) implies a = b & b = c) & ((a,b) // (a1,b1) & (a,b) // (c1,d1) & a <> b implies (a1,b1) // (c1,d1)) & ((a,b) // (c,d) implies (c,d) // (a,b) & (b,a) // (d,c)) & (ex d be Element of IT st (a,b) // (c,d) or (a,b) // (d,c)) & ((a,b) // (c,p) & (a,b) // (c,q) implies a = b or p = q);

    end

    registration

      cluster strict OrdTrapSpace-like for non empty AffinStruct;

      existence by Def12, Lm36;

    end

    definition

      mode OrdTrapSpace is OrdTrapSpace-like non empty AffinStruct;

    end

    registration

      let MOS be MidOrdTrapSpace;

      cluster the AffinStruct of MOS -> OrdTrapSpace-like;

      coherence

      proof

        set X = the AffinStruct of MOS;

         the AffinStruct of MOS is OrdTrapSpace-like

        proof

          let a,b,c,d,a1,b1,c1,d1,p,q be Element of X;

          reconsider a9 = a, b9 = b, c9 = c, d9 = d, a19 = a1, b19 = b1, c19 = c1, d19 = d1, p9 = p, q9 = q as Element of MOS;

           A1:

          now

            let a,b,c,d be Element of X, a9,b9,c9,d9 be Element of the carrier of MOS such that

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

            hereby

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

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

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

            end;

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

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

            hence (a,b) // (c,d) by ANALOAF:def 2;

          end;

          hereby

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

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

            hence a = b & b = c by Def11;

          end;

          hereby

            assume that

             A3: (a,b) // (a1,b1) & (a,b) // (c1,d1) and

             A4: a <> b;

            (a9,b9) // (a19,b19) & (a9,b9) // (c19,d19) by A1, A3;

            then (a19,b19) // (c19,d19) by A4, Def11;

            hence (a1,b1) // (c1,d1) by A1;

          end;

          hereby

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

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

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

            hence (c,d) // (a,b) & (b,a) // (d,c) by A1;

          end;

          thus ex d be Element of X st (a,b) // (c,d) or (a,b) // (d,c)

          proof

            consider x9 be Element of MOS such that

             A5: (a9,b9) // (c9,x9) or (a9,b9) // (x9,c9) by Def11;

            reconsider x = x9 as Element of X;

            take x;

            thus thesis by A1, A5;

          end;

          assume (a,b) // (c,p) & (a,b) // (c,q);

          then (a9,b9) // (c9,p9) & (a9,b9) // (c9,q9) by A1;

          hence a = b or p = q by Def11;

        end;

        hence thesis;

      end;

    end

    reserve OTS for OrdTrapSpace;

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

    reserve a9,b9,c9,d9,a19,b19,d19 for Element of ( Lambda OTS);

    theorem :: GEOMTRAP:47

    

     Th47: for x be set holds (x is Element of OTS iff x is Element of ( Lambda OTS))

    proof

      let x be set;

      ( Lambda OTS) = AffinStruct (# the carrier of OTS, ( lambda the CONGR of OTS) #) by DIRAF:def 2;

      hence thesis;

    end;

    theorem :: GEOMTRAP:48

    

     Th48: a = a9 & b = b9 & c = c9 & d = d9 implies ((a9,b9) // (c9,d9) iff (a,b) // (c,d) or (a,b) // (d,c))

    proof

      

       A1: ( Lambda OTS) = AffinStruct (# the carrier of OTS, ( lambda the CONGR of OTS) #) by DIRAF:def 2;

      assume

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

      hereby

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

        then [ [a9, b9], [c9, d9]] in ( lambda the CONGR of OTS) by A1, ANALOAF:def 2;

        then [ [a, b], [c, d]] in the CONGR of OTS or [ [a, b], [d, c]] in the CONGR of OTS by A2, DIRAF:def 1;

        hence (a,b) // (c,d) or (a,b) // (d,c) by ANALOAF:def 2;

      end;

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

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

      then [ [a, b], [c, d]] in the CONGR of ( Lambda OTS) by A1, DIRAF:def 1;

      hence thesis by A2, ANALOAF:def 2;

    end;

    

     Lm37: for a9, b9, c9 holds ex d9 st (a9,b9) // (c9,d9)

    proof

      let a9, b9, c9;

      reconsider a = a9, b = b9, c = c9 as Element of OTS by Th47;

      consider d such that

       A1: (a,b) // (c,d) or (a,b) // (d,c) by Def12;

      reconsider d9 = d as Element of ( Lambda OTS) by Th47;

      take d9;

      thus thesis by A1, Th48;

    end;

    

     Lm38: (a9,b9) // (c9,d9) implies (c9,d9) // (a9,b9)

    proof

      reconsider a = a9, b = b9, c = c9, d = d9 as Element of the carrier of OTS by Th47;

      assume

       A1: (a9,b9) // (c9,d9);

      per cases by A1, Th48;

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

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

        hence thesis by Th48;

      end;

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

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

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

        hence thesis by Th48;

      end;

    end;

    

     Lm39: a19 <> b19 & (a19,b19) // (a9,b9) & (a19,b19) // (c9,d9) implies (a9,b9) // (c9,d9)

    proof

      reconsider a1 = a19, b1 = b19, a = a9, b = b9, c = c9, d = d9 as Element of OTS by Th47;

      assume that

       A1: a19 <> b19 and

       A2: (a19,b19) // (a9,b9) and

       A3: (a19,b19) // (c9,d9);

      

       A4: (a1,b1) // (c,d) or (a1,b1) // (d,c) by A3, Th48;

      (a1,b1) // (a,b) or (a1,b1) // (b,a) by A2, Th48;

      then (a,b) // (c,d) or (a,b) // (d,c) or (b,a) // (c,d) or (b,a) // (d,c) by A1, A4, Def12;

      then (a,b) // (c,d) or (a,b) // (d,c) by Def12;

      hence thesis by Th48;

    end;

    

     Lm40: (a9,b9) // (c9,d9) & (a9,b9) // (c9,d19) implies a9 = b9 or d9 = d19

    proof

      reconsider a = a9, b = b9, c = c9, d = d9, d1 = d19 as Element of OTS by Th47;

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

      then

       A1: (a,b) // (c,d) & (a,b) // (c,d1) or (a,b) // (c,d) & (a,b) // (d1,c) or (a,b) // (d,c) & (a,b) // (c,d1) or (a,b) // (d,c) & (a,b) // (d1,c) by Th48;

      assume

       A2: a9 <> b9;

      then d = d1 or (d1,c) // (c,d) or (d,c) // (c,d1) or (b,a) // (c,d) & (b,a) // (c,d1) by A1, Def12;

      then d = d1 or c = d & c = d1 by A2, Def12;

      hence thesis;

    end;

    

     Lm41: (a,b) // (a,b)

    proof

      consider c such that

       A1: (a,b) // (a,c) or (a,b) // (c,a) by Def12;

      per cases by A1;

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

        then

         A2: (c,a) // (a,b) by Def12;

        then c = a by Def12;

        hence thesis by A2, Def12;

      end;

        suppose

         A3: (a,b) // (a,c);

        per cases ;

          suppose

           A4: a <> c;

          (a,c) // (a,b) by A3, Def12;

          hence thesis by A4, Def12;

        end;

          suppose a = c;

          then (a,a) // (a,b) by A3, Def12;

          hence thesis by Def12;

        end;

      end;

    end;

    

     Lm42: (a9,b9) // (b9,a9)

    proof

      reconsider a = a9, b = b9 as Element of OTS by Th47;

      (a,b) // (a,b) by Lm41;

      hence thesis by Th48;

    end;

    definition

      let IT be non empty AffinStruct;

      :: GEOMTRAP:def14

      attr IT is TrapSpace-like means for a9,b9,c9,d9,p9,q9 be Element of IT holds (a9,b9) // (b9,a9) & ((a9,b9) // (c9,d9) & (a9,b9) // (c9,q9) implies a9 = b9 or d9 = q9) & (p9 <> q9 & (p9,q9) // (a9,b9) & (p9,q9) // (c9,d9) implies (a9,b9) // (c9,d9)) & ((a9,b9) // (c9,d9) implies (c9,d9) // (a9,b9)) & ex x9 be Element of IT st (a9,b9) // (c9,x9);

    end

    

     Lm43: for OTS be OrdTrapSpace holds ( Lambda OTS) is TrapSpace-like by Lm42, Lm40, Lm39, Lm38, Lm37;

    registration

      cluster strict TrapSpace-like for non empty AffinStruct;

      existence

      proof

        set TS = ( Lambda the OrdTrapSpace);

        TS is TrapSpace-like by Lm43;

        hence thesis;

      end;

    end

    definition

      mode TrapSpace is TrapSpace-like non empty AffinStruct;

    end

    registration

      let OTS be OrdTrapSpace;

      cluster ( Lambda OTS) -> TrapSpace-like;

      correctness by Lm43;

    end

    definition

      let IT be non empty AffinStruct;

      :: GEOMTRAP:def15

      attr IT is Regular means for p,q,a,a1,b,b1,c,c1,d,d1 be Element of IT st p <> q & (p,q) // (a,a1) & (p,q) // (b,b1) & (p,q) // (c,c1) & (p,q) // (d,d1) & (a,b) // (c,d) holds (a1,b1) // (c1,d1);

    end

    registration

      cluster strict Regular for non empty OrdTrapSpace;

      existence

      proof

        set MOTS = the MidOrdTrapSpace;

        set X = the AffinStruct of MOTS;

         A1:

        now

          let a,b,c,d be Element of X, a9,b9,c9,d9 be Element of the carrier of MOTS such that

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

          hereby

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

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

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

          end;

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

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

          hence (a,b) // (c,d) by ANALOAF:def 2;

        end;

        X is Regular

        proof

          let p,q,a,a1,b,b1,c,c1,d,d1 be Element of X such that

           A3: p <> q and

           A4: (p,q) // (a,a1) & (p,q) // (b,b1) and

           A5: (p,q) // (c,c1) & (p,q) // (d,d1) and

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

          reconsider a9 = a, b9 = b, c9 = c, d9 = d, a19 = a1, b19 = b1, c19 = c1, d19 = d1, p9 = p, q9 = q as Element of MOTS;

          

           A7: (p9,q9) // (c9,c19) & (p9,q9) // (d9,d19) by A1, A5;

          

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

          (p9,q9) // (a9,a19) & (p9,q9) // (b9,b19) by A1, A4;

          then (a19,b19) // (c19,d19) by A3, A7, A8, Def11;

          hence (a1,b1) // (c1,d1) by A1;

        end;

        hence thesis;

      end;

    end

    registration

      let MOS be MidOrdTrapSpace;

      cluster the AffinStruct of MOS -> Regular;

      correctness

      proof

        set X = the AffinStruct of MOS;

        now

          let p,q,a,a1,b,b1,c,c1,d,d1 be Element of X;

          assume that

           A1: p <> q and

           A2: (p,q) // (a,a1) & (p,q) // (b,b1) and

           A3: (p,q) // (c,c1) & (p,q) // (d,d1) and

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

          reconsider a9 = a, b9 = b, c9 = c, d9 = d, a19 = a1, b19 = b1, c19 = c1, d19 = d1, p9 = p, q9 = q as Element of MOS;

           A5:

          now

            let a,b,c,d be Element of X, a9,b9,c9,d9 be Element of the carrier of MOS such that

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

            hereby

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

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

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

            end;

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

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

            hence (a,b) // (c,d) by ANALOAF:def 2;

          end;

          then

           A7: (p9,q9) // (c9,c19) & (p9,q9) // (d9,d19) by A3;

          

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

          (p9,q9) // (a9,a19) & (p9,q9) // (b9,b19) by A2, A5;

          then (a19,b19) // (c19,d19) by A1, A7, A8, Def11;

          hence (a1,b1) // (c1,d1) by A5;

        end;

        hence thesis;

      end;

    end