dirort.miz



    begin

    reserve V for RealLinearSpace;

    reserve x,y for VECTOR of V;

    notation

      let AS be non empty OrtStr;

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

      synonym a,b '//' c,d for a,b _|_ c,d;

    end

    theorem :: DIRORT:1

    

     Th1: Gen (x,y) implies (for u,u1,v,v1,w be Element of ( CESpace (V,x,y)) holds (((u,u) '//' (v,w)) & ((u,v) '//' (w,w)) & ((u,v) '//' (u1,v1) & (u,v) '//' (v1,u1) implies u = v or u1 = v1) & ((u,v) '//' (u1,v1) & (u,v) '//' (u1,w) implies (u,v) '//' (v1,w) or (u,v) '//' (w,v1)) & ((u,v) '//' (u1,v1) implies (v,u) '//' (v1,u1)) & ((u,v) '//' (u1,v1) & (u,v) '//' (v1,w) implies (u,v) '//' (u1,w)) & ((u,u1) '//' (v,v1) implies (v,v1) '//' (u,u1) or (v,v1) '//' (u1,u)))) & (for u,v,w be Element of ( CESpace (V,x,y)) holds ex u1 be Element of ( CESpace (V,x,y)) st w <> u1 & (w,u1) '//' (u,v)) & for u,v,w be Element of ( CESpace (V,x,y)) holds ex u1 be Element of ( CESpace (V,x,y)) st w <> u1 & (u,v) '//' (w,u1)

    proof

      assume

       A1: Gen (x,y);

      set S = ( CESpace (V,x,y));

      

       A2: S = OrtStr (# the carrier of V, ( CORTE (V,x,y)) #) by ANALORT:def 7;

      thus for u,u1,v,v1,w be Element of S holds (u,u) '//' (v,w) & (u,v) '//' (w,w) & ((u,v) '//' (u1,v1) & (u,v) '//' (v1,u1) implies u = v or u1 = v1) & ((u,v) '//' (u1,v1) & (u,v) '//' (u1,w) implies (u,v) '//' (v1,w) or (u,v) '//' (w,v1)) & ((u,v) '//' (u1,v1) implies (v,u) '//' (v1,u1)) & ((u,v) '//' (u1,v1) & (u,v) '//' (v1,w) implies (u,v) '//' (u1,w)) & ((u,u1) '//' (v,v1) implies (v,v1) '//' (u,u1) or (v,v1) '//' (u1,u))

      proof

        let u,u1,v,v1,w be Element of S;

        reconsider u9 = u, v9 = v, w9 = w, u19 = u1, v19 = v1 as Element of V by A2;

        (u9,u9,v9,w9) are_COrte_wrt (x,y) by ANALORT: 20;

        hence (u,u) '//' (v,w) by ANALORT: 54;

        (u9,v9,w9,w9) are_COrte_wrt (x,y) by ANALORT: 22;

        hence (u,v) '//' (w,w) by ANALORT: 54;

        (u9,v9,u19,v19) are_COrte_wrt (x,y) & (u9,v9,v19,u19) are_COrte_wrt (x,y) implies u9 = v9 or u19 = v19 by A1, ANALORT: 30;

        hence (u,v) '//' (u1,v1) & (u,v) '//' (v1,u1) implies u = v or u1 = v1 by ANALORT: 54;

        (u9,v9,u19,v19) are_COrte_wrt (x,y) & (u9,v9,u19,w9) are_COrte_wrt (x,y) implies (u9,v9,v19,w9) are_COrte_wrt (x,y) or (u9,v9,w9,v19) are_COrte_wrt (x,y) by A1, ANALORT: 32;

        hence (u,v) '//' (u1,v1) & (u,v) '//' (u1,w) implies (u,v) '//' (v1,w) or (u,v) '//' (w,v1) by ANALORT: 54;

        (u9,v9,u19,v19) are_COrte_wrt (x,y) implies (v9,u9,v19,u19) are_COrte_wrt (x,y) by ANALORT: 34;

        hence (u,v) '//' (u1,v1) implies (v,u) '//' (v1,u1) by ANALORT: 54;

        (u9,v9,u19,v19) are_COrte_wrt (x,y) & (u9,v9,v19,w9) are_COrte_wrt (x,y) implies (u9,v9,u19,w9) are_COrte_wrt (x,y) by A1, ANALORT: 36;

        hence (u,v) '//' (u1,v1) & (u,v) '//' (v1,w) implies (u,v) '//' (u1,w) by ANALORT: 54;

        (u9,u19,v9,v19) are_COrte_wrt (x,y) implies (v9,v19,u9,u19) are_COrte_wrt (x,y) or (v9,v19,u19,u9) are_COrte_wrt (x,y) by A1, ANALORT: 18;

        hence (u,u1) '//' (v,v1) implies (v,v1) '//' (u,u1) or (v,v1) '//' (u1,u) by ANALORT: 54;

      end;

      thus for u,v,w be Element of S holds ex u1 be Element of S st w <> u1 & (w,u1) '//' (u,v)

      proof

        let u,v,w be Element of S;

        reconsider u9 = u, v9 = v, w9 = w as Element of V by A2;

        consider u19 be Element of V such that

         A3: w9 <> u19 and

         A4: (w9,u19,u9,v9) are_COrte_wrt (x,y) by A1, ANALORT: 38;

        reconsider u1 = u19 as Element of S by A2;

        (w,u1) '//' (u,v) by A4, ANALORT: 54;

        hence thesis by A3;

      end;

      let u,v,w be Element of S;

      reconsider u9 = u, v9 = v, w9 = w as Element of V by A2;

      consider u19 be Element of V such that

       A5: w9 <> u19 and

       A6: (u9,v9,w9,u19) are_COrte_wrt (x,y) by A1, ANALORT: 40;

      reconsider u1 = u19 as Element of S by A2;

      (u,v) '//' (w,u1) by A6, ANALORT: 54;

      hence thesis by A5;

    end;

    theorem :: DIRORT:2

    

     Th2: Gen (x,y) implies (for u,u1,v,v1,w be Element of ( CMSpace (V,x,y)) holds (((u,u) '//' (v,w)) & ((u,v) '//' (w,w)) & ((u,v) '//' (u1,v1) & (u,v) '//' (v1,u1) implies u = v or u1 = v1) & ((u,v) '//' (u1,v1) & (u,v) '//' (u1,w) implies (u,v) '//' (v1,w) or (u,v) '//' (w,v1)) & ((u,v) '//' (u1,v1) implies (v,u) '//' (v1,u1)) & ((u,v) '//' (u1,v1) & (u,v) '//' (v1,w) implies (u,v) '//' (u1,w)) & ((u,u1) '//' (v,v1) implies (v,v1) '//' (u,u1) or (v,v1) '//' (u1,u)))) & (for u,v,w be Element of ( CMSpace (V,x,y)) holds ex u1 be Element of ( CMSpace (V,x,y)) st w <> u1 & (w,u1) '//' (u,v)) & for u,v,w be Element of ( CMSpace (V,x,y)) holds ex u1 be Element of ( CMSpace (V,x,y)) st w <> u1 & (u,v) '//' (w,u1)

    proof

      assume

       A1: Gen (x,y);

      set S = ( CMSpace (V,x,y));

      

       A2: S = OrtStr (# the carrier of V, ( CORTM (V,x,y)) #) by ANALORT:def 8;

      thus for u,u1,v,v1,w be Element of S holds (u,u) '//' (v,w) & (u,v) '//' (w,w) & ((u,v) '//' (u1,v1) & (u,v) '//' (v1,u1) implies u = v or u1 = v1) & ((u,v) '//' (u1,v1) & (u,v) '//' (u1,w) implies (u,v) '//' (v1,w) or (u,v) '//' (w,v1)) & ((u,v) '//' (u1,v1) implies (v,u) '//' (v1,u1)) & ((u,v) '//' (u1,v1) & (u,v) '//' (v1,w) implies (u,v) '//' (u1,w)) & ((u,u1) '//' (v,v1) implies (v,v1) '//' (u,u1) or (v,v1) '//' (u1,u))

      proof

        let u,u1,v,v1,w be Element of S;

        reconsider u9 = u, v9 = v, w9 = w, u19 = u1, v19 = v1 as Element of V by A2;

        (u9,u9,v9,w9) are_COrtm_wrt (x,y) by ANALORT: 21;

        hence (u,u) '//' (v,w) by ANALORT: 55;

        (u9,v9,w9,w9) are_COrtm_wrt (x,y) by ANALORT: 23;

        hence (u,v) '//' (w,w) by ANALORT: 55;

        (u9,v9,u19,v19) are_COrtm_wrt (x,y) & (u9,v9,v19,u19) are_COrtm_wrt (x,y) implies u9 = v9 or u19 = v19 by A1, ANALORT: 31;

        hence (u,v) '//' (u1,v1) & (u,v) '//' (v1,u1) implies u = v or u1 = v1 by ANALORT: 55;

        (u9,v9,u19,v19) are_COrtm_wrt (x,y) & (u9,v9,u19,w9) are_COrtm_wrt (x,y) implies (u9,v9,v19,w9) are_COrtm_wrt (x,y) or (u9,v9,w9,v19) are_COrtm_wrt (x,y) by A1, ANALORT: 33;

        hence (u,v) '//' (u1,v1) & (u,v) '//' (u1,w) implies (u,v) '//' (v1,w) or (u,v) '//' (w,v1) by ANALORT: 55;

        (u9,v9,u19,v19) are_COrtm_wrt (x,y) implies (v9,u9,v19,u19) are_COrtm_wrt (x,y) by ANALORT: 35;

        hence (u,v) '//' (u1,v1) implies (v,u) '//' (v1,u1) by ANALORT: 55;

        (u9,v9,u19,v19) are_COrtm_wrt (x,y) & (u9,v9,v19,w9) are_COrtm_wrt (x,y) implies (u9,v9,u19,w9) are_COrtm_wrt (x,y) by A1, ANALORT: 37;

        hence (u,v) '//' (u1,v1) & (u,v) '//' (v1,w) implies (u,v) '//' (u1,w) by ANALORT: 55;

        (u9,u19,v9,v19) are_COrtm_wrt (x,y) implies (v9,v19,u9,u19) are_COrtm_wrt (x,y) or (v9,v19,u19,u9) are_COrtm_wrt (x,y) by A1, ANALORT: 19;

        hence (u,u1) '//' (v,v1) implies (v,v1) '//' (u,u1) or (v,v1) '//' (u1,u) by ANALORT: 55;

      end;

      thus for u,v,w be Element of S holds ex u1 be Element of S st w <> u1 & (w,u1) '//' (u,v)

      proof

        let u,v,w be Element of S;

        reconsider u9 = u, v9 = v, w9 = w as Element of V by A2;

        consider u19 be Element of V such that

         A3: w9 <> u19 and

         A4: (w9,u19,u9,v9) are_COrtm_wrt (x,y) by A1, ANALORT: 39;

        reconsider u1 = u19 as Element of S by A2;

        (w,u1) '//' (u,v) by A4, ANALORT: 55;

        hence thesis by A3;

      end;

      let u,v,w be Element of S;

      reconsider u9 = u, v9 = v, w9 = w as Element of V by A2;

      consider u19 be Element of V such that

       A5: w9 <> u19 and

       A6: (u9,v9,w9,u19) are_COrtm_wrt (x,y) by A1, ANALORT: 41;

      reconsider u1 = u19 as Element of S by A2;

      (u,v) '//' (w,u1) by A6, ANALORT: 55;

      hence thesis by A5;

    end;

    definition

      let IT be non empty OrtStr;

      :: DIRORT:def1

      attr IT is Oriented_Orthogonality_Space-like means

      : Def1: (for u,u1,v,v1,w be Element of IT holds (((u,u) '//' (v,w)) & ((u,v) '//' (w,w)) & ((u,v) '//' (u1,v1) & (u,v) '//' (v1,u1) implies u = v or u1 = v1) & ((u,v) '//' (u1,v1) & (u,v) '//' (u1,w) implies (u,v) '//' (v1,w) or (u,v) '//' (w,v1)) & ((u,v) '//' (u1,v1) implies (v,u) '//' (v1,u1)) & ((u,v) '//' (u1,v1) & (u,v) '//' (v1,w) implies (u,v) '//' (u1,w)) & ((u,u1) '//' (v,v1) implies (v,v1) '//' (u,u1) or (v,v1) '//' (u1,u)))) & (for u,v,w be Element of IT holds ex u1 be Element of IT st w <> u1 & (w,u1) '//' (u,v)) & for u,v,w be Element of IT holds ex u1 be Element of IT st w <> u1 & (u,v) '//' (w,u1);

    end

    registration

      cluster Oriented_Orthogonality_Space-like for non empty OrtStr;

      existence

      proof

        consider V, x, y such that

         A1: Gen (x,y) by ANALMETR: 3;

        take C = ( CESpace (V,x,y));

        thus (for u,u1,v,v1,w be Element of C holds (((u,u) '//' (v,w)) & ((u,v) '//' (w,w)) & ((u,v) '//' (u1,v1) & (u,v) '//' (v1,u1) implies u = v or u1 = v1) & ((u,v) '//' (u1,v1) & (u,v) '//' (u1,w) implies (u,v) '//' (v1,w) or (u,v) '//' (w,v1)) & ((u,v) '//' (u1,v1) implies (v,u) '//' (v1,u1)) & ((u,v) '//' (u1,v1) & (u,v) '//' (v1,w) implies (u,v) '//' (u1,w)) & ((u,u1) '//' (v,v1) implies (v,v1) '//' (u,u1) or (v,v1) '//' (u1,u)))) & (for u,v,w be Element of C holds ex u1 be Element of C st w <> u1 & (w,u1) '//' (u,v)) & for u,v,w be Element of C holds ex u1 be Element of C st w <> u1 & (u,v) '//' (w,u1) by A1, Th1;

      end;

    end

    definition

      mode Oriented_Orthogonality_Space is Oriented_Orthogonality_Space-like non empty OrtStr;

    end

    theorem :: DIRORT:3

    

     Th3: Gen (x,y) implies ( CMSpace (V,x,y)) is Oriented_Orthogonality_Space

    proof

      assume

       A1: Gen (x,y);

      then

       A2: for u,v,w be Element of ( CMSpace (V,x,y)) holds ex u1 be Element of ( CMSpace (V,x,y)) st w <> u1 & (w,u1) '//' (u,v) by Th2;

      

       A3: for u,v,w be Element of ( CMSpace (V,x,y)) holds ex u1 be Element of ( CMSpace (V,x,y)) st w <> u1 & (u,v) '//' (w,u1) by A1, Th2;

      for u,u1,v,v1,w,w1,w2 be Element of ( CMSpace (V,x,y)) holds (u,u) '//' (v,w) & (u,v) '//' (w,w) & ((u,v) '//' (u1,v1) & (u,v) '//' (v1,u1) implies u = v or u1 = v1) & ((u,v) '//' (u1,v1) & (u,v) '//' (u1,w) implies (u,v) '//' (v1,w) or (u,v) '//' (w,v1)) & ((u,v) '//' (u1,v1) implies (v,u) '//' (v1,u1)) & ((u,v) '//' (u1,v1) & (u,v) '//' (v1,w) implies (u,v) '//' (u1,w)) & ((u,u1) '//' (v,v1) implies (v,v1) '//' (u,u1) or (v,v1) '//' (u1,u)) by A1, Th2;

      hence thesis by A2, A3, Def1;

    end;

    theorem :: DIRORT:4

    

     Th4: Gen (x,y) implies ( CESpace (V,x,y)) is Oriented_Orthogonality_Space

    proof

      assume

       A1: Gen (x,y);

      then

       A2: for u,v,w be Element of ( CESpace (V,x,y)) holds ex u1 be Element of ( CESpace (V,x,y)) st w <> u1 & (w,u1) '//' (u,v) by Th1;

      

       A3: for u,v,w be Element of ( CESpace (V,x,y)) holds ex u1 be Element of ( CESpace (V,x,y)) st w <> u1 & (u,v) '//' (w,u1) by A1, Th1;

      for u,u1,v,v1,w,w1,w2 be Element of ( CESpace (V,x,y)) holds (u,u) '//' (v,w) & (u,v) '//' (w,w) & ((u,v) '//' (u1,v1) & (u,v) '//' (v1,u1) implies u = v or u1 = v1) & ((u,v) '//' (u1,v1) & (u,v) '//' (u1,w) implies (u,v) '//' (v1,w) or (u,v) '//' (w,v1)) & ((u,v) '//' (u1,v1) implies (v,u) '//' (v1,u1)) & ((u,v) '//' (u1,v1) & (u,v) '//' (v1,w) implies (u,v) '//' (u1,w)) & ((u,u1) '//' (v,v1) implies (v,v1) '//' (u,u1) or (v,v1) '//' (u1,u)) by A1, Th1;

      hence thesis by A2, A3, Def1;

    end;

    reserve AS for Oriented_Orthogonality_Space;

    reserve u,u1,u2,u3,v,v1,v2,v3,w,w1 for Element of AS;

    theorem :: DIRORT:5

    for u,v,w be Element of AS holds ex u1 be Element of AS st (u1,w) '//' (u,v) & u1 <> w

    proof

      let u, v, w;

      consider u1 such that

       A1: u1 <> w and

       A2: (w,u1) '//' (v,u) by Def1;

      (u1,w) '//' (u,v) by A2, Def1;

      hence thesis by A1;

    end;

    theorem :: DIRORT:6

    for u,v,w be Element of AS holds ex u1 be Element of AS st u <> u1 & ((v,w) '//' (u,u1) or (v,w) '//' (u1,u))

    proof

      let u, v, w;

      consider u1 such that

       A1: u <> u1 and

       A2: (u,u1) '//' (v,w) by Def1;

      (v,w) '//' (u,u1) or (v,w) '//' (u1,u) by A2, Def1;

      hence thesis by A1;

    end;

    definition

      let AS be Oriented_Orthogonality_Space;

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

      :: DIRORT:def2

      pred a,b _|_ c,d means (a,b) '//' (c,d) or (a,b) '//' (d,c);

    end

    definition

      let AS be Oriented_Orthogonality_Space;

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

      :: DIRORT:def3

      pred a,b // c,d means ex e,f be Element of AS st e <> f & (e,f) '//' (a,b) & (e,f) '//' (c,d);

    end

    definition

      let IT be Oriented_Orthogonality_Space;

      :: DIRORT:def4

      attr IT is bach_transitive means for u,u1,u2,v,v1,v2,w,w1 be Element of IT holds ((u,u1) '//' (v,v1) & (w,w1) '//' (v,v1) & (w,w1) '//' (u2,v2) implies (w = w1 or v = v1 or (u,u1) '//' (u2,v2)));

    end

    definition

      let IT be Oriented_Orthogonality_Space;

      :: DIRORT:def5

      attr IT is right_transitive means for u,u1,u2,v,v1,v2,w,w1 be Element of IT holds ((u,u1) '//' (v,v1) & (v,v1) '//' (w,w1) & (u2,v2) '//' (w,w1) implies (w = w1 or v = v1 or (u,u1) '//' (u2,v2)));

    end

    definition

      let IT be Oriented_Orthogonality_Space;

      :: DIRORT:def6

      attr IT is left_transitive means for u,u1,u2,v,v1,v2,w,w1 be Element of IT holds ((u,u1) '//' (v,v1) & (v,v1) '//' (w,w1) & (u,u1) '//' (u2,v2) implies (u = u1 or v = v1 or (u2,v2) '//' (w,w1)));

    end

    definition

      let IT be Oriented_Orthogonality_Space;

      :: DIRORT:def7

      attr IT is Euclidean_like means for u,u1,v,v1 be Element of IT holds ((u,u1) '//' (v,v1) implies (v,v1) '//' (u1,u));

    end

    definition

      let IT be Oriented_Orthogonality_Space;

      :: DIRORT:def8

      attr IT is Minkowskian_like means for u,u1,v,v1 be Element of IT holds ((u,u1) '//' (v,v1) implies (v,v1) '//' (u,u1));

    end

    theorem :: DIRORT:7

    (u,u1) // (w,w) & (w,w) // (u,u1)

    proof

      set v = the Element of AS;

      consider v1 such that

       A1: v1 <> v and

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

      (v,v1) '//' (w,w) by Def1;

      hence thesis by A1, A2;

    end;

    theorem :: DIRORT:8

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

    theorem :: DIRORT:9

    (u,u1) // (v,v1) implies (u1,u) // (v1,v)

    proof

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

      then

      consider w, w1 such that

       A1: w <> w1 and

       A2: (w,w1) '//' (u,u1) and

       A3: (w,w1) '//' (v,v1);

      

       A4: (w1,w) '//' (v1,v) by A3, Def1;

      (w1,w) '//' (u1,u) by A2, Def1;

      hence thesis by A1, A4;

    end;

    theorem :: DIRORT:10

    AS is left_transitive iff for v, v1, w, w1, u2, v2 holds ((v,v1) // (u2,v2) & (v,v1) '//' (w,w1) & v <> v1 implies (u2,v2) '//' (w,w1))

    proof

      

       A1: (for v, v1, w, w1, u2, v2 holds ((v,v1) // (u2,v2) & (v,v1) '//' (w,w1) & v <> v1 implies (u2,v2) '//' (w,w1))) implies for u,u1,u2,v,v1,v2,w,w1 be Element of AS holds ((u,u1) '//' (v,v1) & (v,v1) '//' (w,w1) & (u,u1) '//' (u2,v2) implies (u = u1 or v = v1 or (u2,v2) '//' (w,w1)))

      proof

        assume

         A2: for v, v1, w, w1, u2, v2 holds ((v,v1) // (u2,v2) & (v,v1) '//' (w,w1) & v <> v1 implies (u2,v2) '//' (w,w1));

        let u, u1, u2, v, v1, v2, w, w1;

        assume that

         A3: (u,u1) '//' (v,v1) and

         A4: (v,v1) '//' (w,w1) and

         A5: (u,u1) '//' (u2,v2);

        now

          assume that

           A6: u <> u1 and v <> v1;

          (v,v1) // (u2,v2) by A3, A5, A6;

          hence thesis by A2, A4;

        end;

        hence thesis;

      end;

      thus thesis by A1;

    end;

    theorem :: DIRORT:11

    AS is bach_transitive iff for u, u1, u2, v, v1, v2 holds ((u,u1) '//' (v,v1) & (v,v1) // (u2,v2) & v <> v1 implies (u,u1) '//' (u2,v2))

    proof

      

       A1: (for u, u1, u2, v, v1, v2 holds ((u,u1) '//' (v,v1) & (v,v1) // (u2,v2) & v <> v1 implies (u,u1) '//' (u2,v2))) implies for u,u1,u2,v,v1,v2,w,w1 be Element of AS holds ((u,u1) '//' (v,v1) & (w,w1) '//' (v,v1) & (w,w1) '//' (u2,v2) implies (w = w1 or v = v1 or (u,u1) '//' (u2,v2)))

      proof

        assume

         A2: for u, u1, u2, v, v1, v2 holds ((u,u1) '//' (v,v1) & (v,v1) // (u2,v2) & v <> v1 implies (u,u1) '//' (u2,v2));

        let u, u1, u2, v, v1, v2, w, w1;

        assume that

         A3: (u,u1) '//' (v,v1) and

         A4: (w,w1) '//' (v,v1) and

         A5: (w,w1) '//' (u2,v2);

        now

          assume that

           A6: w <> w1 and v <> v1;

          (v,v1) // (u2,v2) by A4, A5, A6;

          hence thesis by A2, A3;

        end;

        hence thesis;

      end;

      thus thesis by A1;

    end;

    theorem :: DIRORT:12

    AS is bach_transitive implies for u, u1, v, v1, w, w1 holds ((u,u1) // (v,v1) & (v,v1) // (w,w1) & v <> v1 implies (u,u1) // (w,w1))

    proof

      assume

       A1: AS is bach_transitive;

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

      assume that

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

       A3: (v,v1) // (w,w1) and

       A4: v <> v1;

      consider v2, v3 such that

       A5: v2 <> v3 and

       A6: (v2,v3) '//' (u,u1) and

       A7: (v2,v3) '//' (v,v1) by A2;

      (v2,v3) '//' (w,w1) by A1, A3, A4, A7;

      hence thesis by A5, A6;

    end;

    theorem :: DIRORT:13

    

     Th13: Gen (x,y) & AS = ( CESpace (V,x,y)) implies AS is Euclidean_like left_transitive right_transitive bach_transitive

    proof

      assume that

       A1: Gen (x,y) and

       A2: AS = ( CESpace (V,x,y));

      

       A3: ( CESpace (V,x,y)) = OrtStr (# the carrier of V, ( CORTE (V,x,y)) #) by ANALORT:def 7;

       A4:

      now

        let u,u1,u2,v,v1,v2,w,w1 be Element of AS;

        thus (u,u1) '//' (v,v1) & (v,v1) '//' (w,w1) & (u2,v2) '//' (w,w1) implies (w = w1 or v = v1 or (u,u1) '//' (u2,v2))

        proof

          reconsider u9 = u, v9 = v, w9 = w, u19 = u1, v19 = v1, w19 = w1, u29 = u2, v29 = v2 as Element of V by A2, A3;

          (u9,u19,v9,v19) are_COrte_wrt (x,y) & (v9,v19,w9,w19) are_COrte_wrt (x,y) & (u29,v29,w9,w19) are_COrte_wrt (x,y) implies (w9 = w19 or v9 = v19 or (u9,u19,u29,v29) are_COrte_wrt (x,y)) by A1, ANALORT: 44;

          hence thesis by A2, ANALORT: 54;

        end;

      end;

       A5:

      now

        let u,u1,v,v1 be Element of AS;

        thus (u,u1) '//' (v,v1) implies (v,v1) '//' (u1,u)

        proof

          reconsider u9 = u, v9 = v, u19 = u1, v19 = v1 as Element of V by A2, A3;

          (u9,u19,v9,v19) are_COrte_wrt (x,y) implies (v9,v19,u19,u9) are_COrte_wrt (x,y) by A1, ANALORT: 18;

          hence thesis by A2, ANALORT: 54;

        end;

      end;

       A6:

      now

        let u,u1,u2,v,v1,v2,w,w1 be Element of AS;

        thus (u,u1) '//' (v,v1) & (v,v1) '//' (w,w1) & (u,u1) '//' (u2,v2) implies (u = u1 or v = v1 or (u2,v2) '//' (w,w1))

        proof

          reconsider u9 = u, v9 = v, w9 = w, u19 = u1, v19 = v1, w19 = w1, u29 = u2, v29 = v2 as Element of V by A2, A3;

          (u9,u19,v9,v19) are_COrte_wrt (x,y) & (v9,v19,w9,w19) are_COrte_wrt (x,y) & (u9,u19,u29,v29) are_COrte_wrt (x,y) implies (u9 = u19 or v9 = v19 or (u29,v29,w9,w19) are_COrte_wrt (x,y)) by A1, ANALORT: 46;

          hence thesis by A2, ANALORT: 54;

        end;

      end;

      now

        let u,u1,u2,v,v1,v2,w,w1 be Element of AS;

        thus (u,u1) '//' (v,v1) & (w,w1) '//' (v,v1) & (w,w1) '//' (u2,v2) implies (w = w1 or v = v1 or (u,u1) '//' (u2,v2))

        proof

          reconsider u9 = u, v9 = v, w9 = w, u19 = u1, v19 = v1, w19 = w1, u29 = u2, v29 = v2 as Element of V by A2, A3;

          (u9,u19,v9,v19) are_COrte_wrt (x,y) & (w9,w19,v9,v19) are_COrte_wrt (x,y) & (w9,w19,u29,v29) are_COrte_wrt (x,y) implies (w9 = w19 or v9 = v19 or (u9,u19,u29,v29) are_COrte_wrt (x,y)) by A1, ANALORT: 42;

          hence thesis by A2, ANALORT: 54;

        end;

      end;

      hence thesis by A4, A6, A5;

    end;

    registration

      cluster Euclidean_like left_transitive right_transitive bach_transitive for Oriented_Orthogonality_Space;

      existence

      proof

        consider V, x, y such that

         A1: Gen (x,y) by ANALMETR: 3;

        reconsider AS = ( CESpace (V,x,y)) as Oriented_Orthogonality_Space by A1, Th4;

        take AS;

        thus thesis by A1, Th13;

      end;

    end

    theorem :: DIRORT:14

    

     Th14: Gen (x,y) & AS = ( CMSpace (V,x,y)) implies AS is Minkowskian_like left_transitive right_transitive bach_transitive

    proof

      assume that

       A1: Gen (x,y) and

       A2: AS = ( CMSpace (V,x,y));

      

       A3: ( CMSpace (V,x,y)) = OrtStr (# the carrier of V, ( CORTM (V,x,y)) #) by ANALORT:def 8;

       A4:

      now

        let u,u1,u2,v,v1,v2,w,w1 be Element of AS;

        thus (u,u1) '//' (v,v1) & (v,v1) '//' (w,w1) & (u2,v2) '//' (w,w1) implies (w = w1 or v = v1 or (u,u1) '//' (u2,v2))

        proof

          reconsider u9 = u, v9 = v, w9 = w, u19 = u1, v19 = v1, w19 = w1, u29 = u2, v29 = v2 as Element of V by A2, A3;

          (u9,u19,v9,v19) are_COrtm_wrt (x,y) & (v9,v19,w9,w19) are_COrtm_wrt (x,y) & (u29,v29,w9,w19) are_COrtm_wrt (x,y) implies (w9 = w19 or v9 = v19 or (u9,u19,u29,v29) are_COrtm_wrt (x,y)) by A1, ANALORT: 45;

          hence thesis by A2, ANALORT: 55;

        end;

      end;

       A5:

      now

        let u,u1,v,v1 be Element of AS;

        thus (u,u1) '//' (v,v1) implies (v,v1) '//' (u,u1)

        proof

          reconsider u9 = u, v9 = v, u19 = u1, v19 = v1 as Element of V by A2, A3;

          (u9,u19,v9,v19) are_COrtm_wrt (x,y) implies (v9,v19,u9,u19) are_COrtm_wrt (x,y) by A1, ANALORT: 19;

          hence thesis by A2, ANALORT: 55;

        end;

      end;

       A6:

      now

        let u,u1,u2,v,v1,v2,w,w1 be Element of AS;

        thus (u,u1) '//' (v,v1) & (v,v1) '//' (w,w1) & (u,u1) '//' (u2,v2) implies (u = u1 or v = v1 or (u2,v2) '//' (w,w1))

        proof

          reconsider u9 = u, v9 = v, w9 = w, u19 = u1, v19 = v1, w19 = w1, u29 = u2, v29 = v2 as Element of V by A2, A3;

          (u9,u19,v9,v19) are_COrtm_wrt (x,y) & (v9,v19,w9,w19) are_COrtm_wrt (x,y) & (u9,u19,u29,v29) are_COrtm_wrt (x,y) implies (u9 = u19 or v9 = v19 or (u29,v29,w9,w19) are_COrtm_wrt (x,y)) by A1, ANALORT: 47;

          hence thesis by A2, ANALORT: 55;

        end;

      end;

      now

        let u,u1,u2,v,v1,v2,w,w1 be Element of AS;

        thus (u,u1) '//' (v,v1) & (w,w1) '//' (v,v1) & (w,w1) '//' (u2,v2) implies (w = w1 or v = v1 or (u,u1) '//' (u2,v2))

        proof

          reconsider u9 = u, v9 = v, w9 = w, u19 = u1, v19 = v1, w19 = w1, u29 = u2, v29 = v2 as Element of V by A2, A3;

          (u9,u19,v9,v19) are_COrtm_wrt (x,y) & (w9,w19,v9,v19) are_COrtm_wrt (x,y) & (w9,w19,u29,v29) are_COrtm_wrt (x,y) implies (w9 = w19 or v9 = v19 or (u9,u19,u29,v29) are_COrtm_wrt (x,y)) by A1, ANALORT: 43;

          hence thesis by A2, ANALORT: 55;

        end;

      end;

      hence thesis by A4, A6, A5;

    end;

    registration

      cluster Minkowskian_like left_transitive right_transitive bach_transitive for Oriented_Orthogonality_Space;

      existence

      proof

        consider V, x, y such that

         A1: Gen (x,y) by ANALMETR: 3;

        reconsider AS = ( CMSpace (V,x,y)) as Oriented_Orthogonality_Space by A1, Th3;

        take AS;

        thus thesis by A1, Th14;

      end;

    end

    theorem :: DIRORT:15

    

     Th15: AS is left_transitive implies AS is right_transitive

    proof

      (for u,u1,u2,v,v1,v2,w,w1 be Element of AS holds (((u,u1) '//' (v,v1) & (v,v1) '//' (w,w1) & (u,u1) '//' (u2,v2)) implies (u = u1 or v = v1 or (u2,v2) '//' (w,w1)))) implies for u,u1,u2,v,v1,v2,w,w1 be Element of AS holds ((u,u1) '//' (v,v1) & (v,v1) '//' (w,w1) & (u2,v2) '//' (w,w1) implies (w = w1 or v = v1 or (u,u1) '//' (u2,v2)))

      proof

        assume

         A1: for u,u1,u2,v,v1,v2,w,w1 be Element of AS holds ((u,u1) '//' (v,v1) & (v,v1) '//' (w,w1) & (u,u1) '//' (u2,v2) implies (u = u1 or v = v1 or (u2,v2) '//' (w,w1)));

        let u, u1, u2, v, v1, v2, w, w1;

        assume that

         A2: (u,u1) '//' (v,v1) and

         A3: (v,v1) '//' (w,w1) and

         A4: (u2,v2) '//' (w,w1);

        

         A5: (w = w1 or v = v1 or (u,u1) '//' (u2,v2) or (u,u1) '//' (v2,u2)) implies (w = w1 or v = v1 or (u,u1) '//' (u2,v2))

        proof

          now

             A6:

            now

              assume (v2,u2) '//' (w,w1);

              then (u2,v2) '//' (w1,w) by Def1;

              then u2 = v2 or w = w1 by A4, Def1;

              hence thesis;

            end;

            u = u1 implies thesis by Def1;

            hence thesis by A1, A2, A3, A6;

          end;

          hence thesis;

        end;

         A7:

        now

          assume that

           A8: (w,w1) '//' (v,v1) and

           A9: (v,v1) '//' (u,u1) and

           A10: (w,w1) '//' (v2,u2);

          w = w1 or v = v1 or (v2,u2) '//' (u,u1) by A1, A8, A9, A10;

          hence thesis by A5, Def1;

        end;

         A11:

        now

          assume that

           A12: (w,w1) '//' (v1,v) and

           A13: (v,v1) '//' (u,u1) and

           A14: (w,w1) '//' (v2,u2);

          (v1,v) '//' (u1,u) by A13, Def1;

          then w = w1 or v = v1 or (v2,u2) '//' (u1,u) by A1, A12, A14;

          then w = w1 or v = v1 or (u2,v2) '//' (u,u1) by Def1;

          hence thesis by A5, Def1;

        end;

         A15:

        now

          assume that

           A16: (w,w1) '//' (v1,v) and

           A17: (v,v1) '//' (u,u1) and

           A18: (w,w1) '//' (u2,v2);

          (v1,v) '//' (u1,u) by A17, Def1;

          then w = w1 or v = v1 or (u2,v2) '//' (u1,u) by A1, A16, A18;

          then w = w1 or v = v1 or (v2,u2) '//' (u,u1) by Def1;

          hence thesis by A5, Def1;

        end;

         A19:

        now

          assume that

           A20: (w,w1) '//' (v1,v) and

           A21: (v,v1) '//' (u1,u) and

           A22: (w,w1) '//' (v2,u2);

          (v1,v) '//' (u,u1) by A21, Def1;

          then w = w1 or v = v1 or (v2,u2) '//' (u,u1) by A1, A20, A22;

          hence thesis by A5, Def1;

        end;

         A23:

        now

          assume that

           A24: (w,w1) '//' (v1,v) and

           A25: (v,v1) '//' (u1,u) and

           A26: (w,w1) '//' (u2,v2);

          (v1,v) '//' (u,u1) by A25, Def1;

          then w = w1 or v1 = v or (u2,v2) '//' (u,u1) by A1, A24, A26;

          hence thesis by A5, Def1;

        end;

         A27:

        now

          assume that

           A28: (w,w1) '//' (v,v1) and

           A29: (v,v1) '//' (u1,u) and

           A30: (w,w1) '//' (v2,u2);

          w = w1 or v = v1 or (v2,u2) '//' (u1,u) by A1, A28, A29, A30;

          then w = w1 or v = v1 or (u1,u) '//' (u2,v2) or (u1,u) '//' (v2,u2) by Def1;

          hence thesis by A5, Def1;

        end;

         A31:

        now

          assume that

           A32: (w,w1) '//' (v,v1) and

           A33: (v,v1) '//' (u1,u) and

           A34: (w,w1) '//' (u2,v2);

          w = w1 or v = v1 or (u2,v2) '//' (u1,u) by A1, A32, A33, A34;

          then w = w1 or v = v1 or (u1,u) '//' (u2,v2) or (u1,u) '//' (v2,u2) by Def1;

          hence thesis by A5, Def1;

        end;

        now

          assume that

           A35: (w,w1) '//' (v,v1) and

           A36: (v,v1) '//' (u,u1) and

           A37: (w,w1) '//' (u2,v2);

          w = w1 or v = v1 or (u2,v2) '//' (u,u1) by A1, A35, A36, A37;

          hence thesis by A5, Def1;

        end;

        hence thesis by A2, A3, A4, A7, A31, A27, A15, A11, A23, A19, Def1;

      end;

      hence thesis;

    end;

    theorem :: DIRORT:16

    AS is left_transitive implies AS is bach_transitive

    proof

      (for u,u1,u2,v,v1,v2,w,w1 be Element of AS holds (((u,u1) '//' (v,v1) & (v,v1) '//' (w,w1) & (u,u1) '//' (u2,v2)) implies (u = u1 or v = v1 or (u2,v2) '//' (w,w1)))) implies for u,u1,u2,v,v1,v2,w,w1 be Element of AS holds ((u,u1) '//' (v,v1) & (w,w1) '//' (v,v1) & (w,w1) '//' (u2,v2) implies (w = w1 or v = v1 or (u,u1) '//' (u2,v2)))

      proof

        assume

         A1: for u,u1,u2,v,v1,v2,w,w1 be Element of AS holds ((u,u1) '//' (v,v1) & (v,v1) '//' (w,w1) & (u,u1) '//' (u2,v2) implies (u = u1 or v = v1 or (u2,v2) '//' (w,w1)));

        let u, u1, u2, v, v1, v2, w, w1;

        

         A2: AS is left_transitive implies AS is right_transitive by Th15;

        then

         A3: (u,u1) '//' (v,v1) & (v,v1) '//' (w1,w) & (u2,v2) '//' (w1,w) implies thesis by A1;

        assume that

         A4: (u,u1) '//' (v,v1) and

         A5: (w,w1) '//' (v,v1) and

         A6: (w,w1) '//' (u2,v2);

        

         A7: (v = v1 or w = w1 or (u,u1) '//' (u2,v2) or (u,u1) '//' (v2,u2)) implies (w = w1 or v = v1 or (u,u1) '//' (u2,v2))

        proof

           A8:

          now

            assume that

             A9: (u,u1) '//' (v2,u2) and

             A10: u <> u1 and

             A11: v <> v1 and w <> w1;

             A12:

            now

              assume

               A13: (u2,v2) '//' (u,u1);

              then

               A14: (u2,v2) '//' (w,w1) by A2, A1, A4, A5, A10, A11;

               A15:

              now

                assume (u2,v2) '//' (w1,w);

                then w = w1 or u2 = v2 by A14, Def1;

                hence thesis;

              end;

              (w1,w) '//' (v2,u2) by A6, Def1;

              then (u2,v2) '//' (w1,w) or u2 = v2 by A2, A1, A9, A10, A13;

              hence thesis by A15;

            end;

             A16:

            now

              

               A17: (w1,w) '//' (v1,v) by A5, Def1;

              assume

               A18: (u2,v2) '//' (u1,u);

              (u1,u) '//' (v1,v) by A4, Def1;

              then

               A19: (u2,v2) '//' (w1,w) by A2, A1, A10, A11, A18, A17;

               A20:

              now

                assume (u2,v2) '//' (w,w1);

                then w = w1 or u2 = v2 by A19, Def1;

                hence thesis;

              end;

              (u1,u) '//' (u2,v2) by A9, Def1;

              then (u2,v2) '//' (w,w1) or u2 = v2 by A2, A1, A6, A10, A18;

              hence thesis by A20;

            end;

            (v2,u2) '//' (u,u1) or (v2,u2) '//' (u1,u) by A9, Def1;

            hence thesis by A16, A12, Def1;

          end;

          assume v = v1 or w = w1 or (u,u1) '//' (u2,v2) or (u,u1) '//' (v2,u2);

          hence thesis by A8, Def1;

        end;

         A21:

        now

          assume that

           A22: (u,u1) '//' (v,v1) and

           A23: (v,v1) '//' (w,w1) and

           A24: (u2,v2) '//' (w1,w);

          (v2,u2) '//' (w,w1) by A24, Def1;

          hence thesis by A2, A1, A7, A22, A23;

        end;

         A25:

        now

          assume that

           A26: (u,u1) '//' (v,v1) and

           A27: (v,v1) '//' (w1,w) and

           A28: (u2,v2) '//' (w,w1);

          (v2,u2) '//' (w1,w) by A28, Def1;

          hence thesis by A2, A1, A7, A26, A27;

        end;

        (u,u1) '//' (v,v1) & (v,v1) '//' (w,w1) & (u2,v2) '//' (w,w1) implies thesis by A2, A1;

        hence thesis by A4, A5, A6, A21, A3, A25, Def1;

      end;

      hence thesis;

    end;

    theorem :: DIRORT:17

    AS is bach_transitive implies (AS is right_transitive iff for u, u1, v, v1, u2, v2 holds ((u,u1) '//' (u2,v2) & (v,v1) '//' (u2,v2) & u2 <> v2 implies (u,u1) // (v,v1)))

    proof

      

       A1: (for u,u1,u2,v,v1,v2,w,w1 be Element of AS holds (((u,u1) '//' (v,v1) & (v,v1) '//' (w,w1) & (u2,v2) '//' (w,w1)) implies (w = w1 or v = v1 or (u,u1) '//' (u2,v2)))) implies for u, u1, v, v1, u2, v2 holds ((u,u1) '//' (u2,v2) & (v,v1) '//' (u2,v2) & u2 <> v2 implies (u,u1) // (v,v1))

      proof

        set w = the Element of AS;

        assume

         A2: for u,u1,u2,v,v1,v2,w,w1 be Element of AS holds (u,u1) '//' (v,v1) & (v,v1) '//' (w,w1) & (u2,v2) '//' (w,w1) implies (w = w1 or v = v1 or (u,u1) '//' (u2,v2));

        let u, u1, v, v1, u2, v2;

        assume that

         A3: (u,u1) '//' (u2,v2) and

         A4: (v,v1) '//' (u2,v2) and

         A5: u2 <> v2;

        consider w1 such that

         A6: w <> w1 and

         A7: (w,w1) '//' (u,u1) by Def1;

         A8:

        now

          set w = the Element of AS;

          assume

           A9: u = u1;

          consider w1 such that

           A10: w <> w1 and

           A11: (w,w1) '//' (v,v1) by Def1;

          (w,w1) '//' (u,u) by Def1;

          hence thesis by A9, A10, A11;

        end;

        now

          assume u <> u1;

          then (w,w1) '//' (v,v1) by A2, A3, A4, A5, A7;

          hence thesis by A6, A7;

        end;

        hence thesis by A8;

      end;

      assume

       A12: AS is bach_transitive;

      (for u, u1, v, v1, u2, v2 holds (((u,u1) '//' (u2,v2) & (v,v1) '//' (u2,v2) & u2 <> v2) implies (u,u1) // (v,v1))) implies for u,u1,u2,v,v1,v2,w,w1 be Element of AS holds ((u,u1) '//' (v,v1) & (v,v1) '//' (w,w1) & (u2,v2) '//' (w,w1) implies (w = w1 or v = v1 or (u,u1) '//' (u2,v2)))

      proof

        assume

         A13: for u, u1, v, v1, u2, v2 holds (u,u1) '//' (u2,v2) & (v,v1) '//' (u2,v2) & u2 <> v2 implies (u,u1) // (v,v1);

        let u, u1, u2, v, v1, v2, w, w1;

        assume that

         A14: (u,u1) '//' (v,v1) and

         A15: (v,v1) '//' (w,w1) and

         A16: (u2,v2) '//' (w,w1);

        now

          assume that

           A17: w <> w1 and v <> v1;

          (v,v1) // (u2,v2) by A13, A15, A16, A17;

          then ex u3, v3 st u3 <> v3 & (u3,v3) '//' (v,v1) & (u3,v3) '//' (u2,v2);

          hence thesis by A12, A14;

        end;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: DIRORT:18

    AS is right_transitive & (AS is Euclidean_like or AS is Minkowskian_like) implies AS is left_transitive

    proof

      assume

       A1: AS is right_transitive;

      (for u,u1,v,v1 be Element of AS holds ((u,u1) '//' (v,v1) implies (v,v1) '//' (u,u1)) or for u,u1,v,v1 be Element of AS holds ((u,u1) '//' (v,v1) implies (v,v1) '//' (u1,u))) implies for u,u1,u2,v,v1,v2,w,w1 be Element of AS holds ((u,u1) '//' (v,v1) & (v,v1) '//' (w,w1) & (u,u1) '//' (u2,v2) implies (u = u1 or v = v1 or (u2,v2) '//' (w,w1)))

      proof

        assume

         A2: for u,u1,v,v1 be Element of AS holds ((u,u1) '//' (v,v1) implies (v,v1) '//' (u,u1)) or for u,u1,v,v1 be Element of AS holds ((u,u1) '//' (v,v1) implies (v,v1) '//' (u1,u));

        let u, u1, u2, v, v1, v2, w, w1;

        assume that

         A3: (u,u1) '//' (v,v1) and

         A4: (v,v1) '//' (w,w1) and

         A5: (u,u1) '//' (u2,v2);

         A6:

        now

          assume

           A7: for u,u1,v,v1 be Element of AS holds ((u,u1) '//' (v,v1) implies (v,v1) '//' (u1,u));

          now

            (w,w1) '//' (v1,v) by A4, A7;

            then

             A8: (w1,w) '//' (v,v1) by Def1;

            

             A9: (u2,v2) '//' (u1,u) by A5, A7;

            assume that

             A10: u <> u1 and

             A11: v <> v1;

            (v,v1) '//' (u1,u) by A3, A7;

            then (w1,w) '//' (u2,v2) by A1, A10, A11, A8, A9;

            hence thesis by A7;

          end;

          hence thesis;

        end;

        now

          assume

           A12: for u,u1,v,v1 be Element of AS holds ((u,u1) '//' (v,v1) implies (v,v1) '//' (u,u1));

          now

            

             A13: (u2,v2) '//' (u,u1) by A5, A12;

            

             A14: (w,w1) '//' (v,v1) by A4, A12;

            assume that

             A15: u <> u1 and

             A16: v <> v1;

            (v,v1) '//' (u,u1) by A3, A12;

            then (w,w1) '//' (u2,v2) by A1, A15, A16, A14, A13;

            hence thesis by A12;

          end;

          hence thesis;

        end;

        hence thesis by A2, A6;

      end;

      hence thesis;

    end;