:: Oriented Metric-Affine Plane - Part I
::  by Jaroslaw Zajkowski
::
:: Received October 24, 1991
:: Copyright (c) 1991 Association of Mizar Users

environ

 vocabularies RLVECT_1, ARYTM_1, ANALMETR, FUNCT_3, ANALOAF, SYMSP_1, RELAT_1,
      ANALORT, ARYTM, ALGSTR_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, REAL_1, RELSET_1, NUMBERS, STRUCT_0,
      ALGSTR_0, RLVECT_1, ANALOAF, ANALMETR, GEOMTRAP;
 constructors DOMAIN_1, XXREAL_0, REAL_1, MEMBERED, TDGROUP, ANALMETR,
      GEOMTRAP;
 registrations RELSET_1, MEMBERED, STRUCT_0, TDGROUP;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions STRUCT_0, RLVECT_1;
 theorems GEOMTRAP, RELAT_1, RLVECT_1, ANALOAF, ANALMETR, ZFMISC_1, XCMPLX_0,
      XCMPLX_1, XREAL_1;
 schemes RELSET_1;

begin

definition
  let V be Abelian (non empty addLoopStr), v,w be Element of V;
  redefine func v + w;
  commutativity by RLVECT_1:def 5;
end;

reserve V for RealLinearSpace,
  u,u1,u2,v,v1,v2,w,w1,x,y for VECTOR of V,
  a,a1,a2,b,b1,b2,c1,c2,n,k1,k2 for Real;

Lm1: v1 = b1*x + b2*y & v2 = c1*x + c2*y implies
v1 + v2 = (b1 + c1)*x + (b2 + c2)*y & v1 - v2 = (b1 - c1)*x + (b2 - c2)*y
proof
  assume that
A1: v1 = b1*x + b2*y and
A2: v2 = c1*x + c2*y;
  thus v1 + v2 = ((b1*x + b2*y) + c1*x) + c2*y by A1,A2,RLVECT_1:def 6
    .= ((b1*x + c1*x) + b2*y) + c2*y by RLVECT_1:def 6
    .= ((b1 + c1)*x + b2*y) + c2*y by RLVECT_1:def 9
    .= (b1 + c1)*x + (b2*y + c2*y) by RLVECT_1:def 6
    .= (b1 + c1)*x + (b2 + c2)*y by RLVECT_1:def 9;
  thus v1 - v2 = (b1*x + b2*y)+(-(c1*x) + -(c2*y)) by A1,A2,RLVECT_1:45
    .= (b1*x + b2*y)+(c1*(-x) + -(c2*y)) by RLVECT_1:39
    .= (b1*x + b2*y)+(c1*(-x) + c2*(-y)) by RLVECT_1:39
    .= (b1*x + b2*y)+((-c1)*x + c2*(-y)) by RLVECT_1:38
    .= (b1*x + b2*y)+((-c1)*x + (-c2)*y) by RLVECT_1:38
    .= ((b1*x + b2*y) + (-c1)*x) + (-c2)*y by RLVECT_1:def 6
    .= ((b1*x + (-c1)*x) + b2*y) + (-c2)*y by RLVECT_1:def 6
    .= ((b1 + (-c1))*x + b2*y) + (-c2)*y by RLVECT_1:def 9
    .= (b1 + (-c1))*x + (b2*y + (-c2)*y) by RLVECT_1:def 6
    .= (b1 - c1)*x + (b2 + (-c2))*y by RLVECT_1:def 9
    .= (b1 - c1)*x + (b2 - c2)*y;
end;

Lm2: v = b1*x + b2*y implies a*v = (a*b1)*x + (a*b2)*y
proof
  assume v= b1*x + b2*y;
  hence a*v = a*(b1*x) + a*(b2*y) by RLVECT_1:def 9
    .= (a*b1)*x + a*(b2*y) by RLVECT_1:def 9
    .= (a*b1)*x + (a*b2)*y by RLVECT_1:def 9;
end;

Lm3: Gen x,y & a1*x + a2*y = b1*x + b2*y implies a1=b1 & a2=b2
proof
  assume that
A1: Gen x,y and
A2: a1*x+a2*y=b1*x+b2*y;
  0.V = (a1*x+a2*y)-(b1*x+b2*y) by A2,RLVECT_1:28
    .= (a1-b1)*x+(a2-b2)*y by Lm1;
  then -b1 + a1 =0 & -b2 + a2 = 0 by A1,ANALMETR:def 1;
  hence thesis;
end;

Lm4: Gen x,y implies x<>0.V & y<>0.V
proof
  assume
A1: Gen x,y;
A2: x<>0.V
  proof
    assume
A3: x=0.V;
    consider a,b such that
A4: a=1 and
A5: b=0;
    a*x+b*y=0.V+0*y by A3,A5,RLVECT_1:23
      .=0.V+0.V by RLVECT_1:23
      .=0.V by RLVECT_1:10;
    hence contradiction by A1,A4,ANALMETR:def 1;
  end;
  y<>0.V
  proof
    assume
A6: y=0.V;
    consider a,b such that
A7: a=0 and
A8: b=1;
    a*x+b*y=0.V+1*0.V by A6,A7,A8,RLVECT_1:23
      .=0.V+0.V by RLVECT_1:23
      .=0.V by RLVECT_1:10;
    hence thesis by A1,A8,ANALMETR:def 1;
  end;
  hence thesis by A2;
end;

Lm5: Gen x,y implies u = pr1(x,y,u)*x + pr2(x,y,u)*y
proof
  assume
A1: Gen x,y;
  then ex b st u = (pr1(x,y,u))*x + b*y by GEOMTRAP:def 4;
  hence thesis by A1,GEOMTRAP:def 5;
end;

Lm6: (Gen x,y & u=k1*x+k2*y) implies k1=pr1(x,y,u) & k2=pr2(x,y,u)
proof
  assume
A1: Gen x,y & u=k1*x+k2*y;
  then u = pr1(x,y,u)*x + pr2(x,y,u)*y by Lm5;
  hence thesis by A1,Lm3;
end;

Lm7: Gen x,y implies ( pr1(x,y,u+v) = pr1(x,y,u)+pr1(x,y,v) &
pr2(x,y,u+v) = pr2(x,y,u)+pr2(x,y,v) & pr1(x,y,u-v) = pr1(x,y,u)-pr1(x,y,v) &
pr2(x,y,u-v) = pr2(x,y,u)-pr2(x,y,v) & pr1(x,y,a*u) = a*pr1(x,y,u) &
pr2(x,y,a*u) = a*pr2(x,y,u))
proof
  assume
A1: Gen x,y;
  set p1u = pr1(x,y,u), p2u = pr2(x,y,u), p1v = pr1(x,y,v), p2v = pr2(x,y,v);
A2: u = p1u*x + p2u*y & v = p1v*x + p2v*y by A1,Lm5;
  then u + v = (p1u*x + p2u*y + p1v*x) + p2v*y by RLVECT_1:def 6
    .= ((p1u*x + p1v*x) + p2u*y) + p2v*y by RLVECT_1:def 6
    .= (p1u*x + p1v*x) + (p2u*y + p2v*y) by RLVECT_1:def 6
    .= (p1u + p1v)*x + (p2u*y + p2v*y) by RLVECT_1:def 9
    .= (p1u + p1v)*x + (p2u + p2v)*y by RLVECT_1:def 9;
  hence pr1(x,y,u+v) = p1u + p1v & pr2(x,y,u+v) = p2u + p2v by A1,Lm6;
  u - v = (p1u - p1v)*x + (p2u - p2v)*y by A2,Lm1;
  hence pr1(x,y,u-v) = p1u - p1v & pr2(x,y,u-v) = p2u - p2v by A1,Lm6;
  a*u = (a*p1u)*x + (a*p2u)*y by A2,Lm2;
  hence pr1(x,y,a*u) = a*pr1(x,y,u) & pr2(x,y,a*u) = a*pr2(x,y,u) by A1,Lm6;
end;

definition
  let V,x,y;
  let u;
  func Ortm(x,y,u) -> VECTOR of V equals

  pr1(x,y,u)*x + (-pr2(x,y,u))*y;
  correctness;
end;

theorem Th1:
  Gen x,y implies Ortm(x,y,u+v)=Ortm(x,y,u)+Ortm(x,y,v)
proof
  assume
A1: Gen x,y;
  hence Ortm(x,y,u+v)= (pr1(x,y,u)+pr1(x,y,v))*x + (-pr2(x,y,u+v))*y by Lm7
    .=(pr1(x,y,u) + pr1(x,y,v))*x + (-(pr2(x,y,u) + pr2(x,y,v)))*y by A1,Lm7
    .=pr1(x,y,u)*x + pr1(x,y,v)*x + (-(pr2(x,y,u) + pr2(x,y,v)))*y
  by RLVECT_1:def 9
    .=pr1(x,y,u)*x + pr1(x,y,v)*x + (pr2(x,y,u) + pr2(x,y,v))*(-y)
  by RLVECT_1:38
    .=pr1(x,y,u)*x + pr1(x,y,v)*x + (-((pr2(x,y,u) + pr2(x,y,v))*y))
  by RLVECT_1:39
    .=pr1(x,y,u)*x + pr1(x,y,v)*x + (-(pr2(x,y,u)*y +pr2(x,y,v)*y))
  by RLVECT_1:def 9
    .=pr1(x,y,u)*x + pr1(x,y,v)*x + (-(pr2(x,y,u)*y) + (-(pr2(x,y,v)*y)))
  by RLVECT_1:45
    .=pr1(x,y,u)*x + (pr1(x,y,v)*x + (-(pr2(x,y,u)*y) + (-(pr2(x,y,v)*y))))
  by RLVECT_1:def 6
    .=pr1(x,y,u)*x + ((-(pr2(x,y,u)*y)) + (pr1(x,y,v)*x + (-pr2(x,y,v)*y)))
  by RLVECT_1:def 6
    .=pr1(x,y,u)*x + (-(pr2(x,y,u)*y)) + (pr1(x,y,v)*x + (-pr2(x,y,v)*y))
  by RLVECT_1:def 6
    .=pr1(x,y,u)*x + (pr2(x,y,u)*(-y)) + (pr1(x,y,v)*x + (-pr2(x,y,v)*y))
  by RLVECT_1:39
    .=pr1(x,y,u)*x + (pr2(x,y,u)*(-y)) + (pr1(x,y,v)*x + (pr2(x,y,v)*(-y)))
  by RLVECT_1:39
    .=pr1(x,y,u)*x + (-pr2(x,y,u))*y + (pr1(x,y,v)*x + (pr2(x,y,v)*(-y)))
  by RLVECT_1:38
    .=Ortm(x,y,u) + Ortm(x,y,v) by RLVECT_1:38;
end;

theorem Th2:
  Gen x,y implies Ortm(x,y,n*u)= n*Ortm(x,y,u)
proof
  assume
A1: Gen x,y;
  hence Ortm(x,y,n*u)=n*pr1(x,y,u)*x + (-pr2(x,y,n*u))*y by Lm7
    .=n*pr1(x,y,u)*x + (-(n*pr2(x,y,u)))*y by A1,Lm7
    .=n*pr1(x,y,u)*x + (n*pr2(x,y,u)*(-y)) by RLVECT_1:38
    .=n*pr1(x,y,u)*x + (-(n*pr2(x,y,u)*y)) by RLVECT_1:39
    .=n*pr1(x,y,u)*x + (-(n*(pr2(x,y,u)*y))) by RLVECT_1:def 9
    .=n*pr1(x,y,u)*x + n*(-pr2(x,y,u)*y) by RLVECT_1:39
    .=n*(pr1(x,y,u)*x) + n*(-pr2(x,y,u)*y) by RLVECT_1:def 9
    .=n*((pr1(x,y,u)*x) + (-pr2(x,y,u)*y)) by RLVECT_1:def 9
    .=n*((pr1(x,y,u)*x) + (pr2(x,y,u)*(-y))) by RLVECT_1:39
    .=n*Ortm(x,y,u) by RLVECT_1:38;
end;

theorem
  Gen x,y implies Ortm(x,y,0.V) = 0.V
proof
  assume
A1: Gen x,y;
  consider u;
  thus Ortm(x,y,0.V) = Ortm(x,y,0*u) by RLVECT_1:23
    .= 0*Ortm(x,y,u) by A1,Th2
    .= 0.V by RLVECT_1:23;
end;

theorem Th4:
  Gen x,y implies Ortm(x,y,-u) = -Ortm(x,y,u)
proof
  assume
A1: Gen x,y;
  then
A2: -u=-(pr1(x,y,u)*x + pr2(x,y,u)*y) by Lm5
    .=-(pr1(x,y,u)*x) + (-(pr2(x,y,u)*y)) by RLVECT_1:45
    .=pr1(x,y,u)*(-x) + (-(pr2(x,y,u)*y)) by RLVECT_1:39
    .=(-pr1(x,y,u))*x + (-(pr2(x,y,u)*y)) by RLVECT_1:38
    .=(-pr1(x,y,u))*x + pr2(x,y,u)*(-y) by RLVECT_1:39
    .=(-pr1(x,y,u))*x + (-pr2(x,y,u))*y by RLVECT_1:38;
  hence Ortm(x,y,-u)=(-pr1(x,y,u))*x + (-pr2(x,y,-u))*y by A1,Lm6
    .=(-pr1(x,y,u))*x + (-(-pr2(x,y,u)))*y by A1,A2,Lm6
    .=pr1(x,y,u)*(-x) + (-(-pr2(x,y,u)))*y by RLVECT_1:38
    .=-(pr1(x,y,u)*x) + (-(-pr2(x,y,u)))*y by RLVECT_1:39
    .=-(pr1(x,y,u)*x) + (-pr2(x,y,u))*(-y) by RLVECT_1:38
    .=-(pr1(x,y,u)*x) + (-((-pr2(x,y,u))*y)) by RLVECT_1:39
    .=-Ortm(x,y,u) by RLVECT_1:45;
end;

theorem Th5:
  Gen x,y implies Ortm(x,y,u-v)=Ortm(x,y,u)-Ortm(x,y,v)
proof
  assume
A1: Gen x,y;
  hence Ortm(x,y,u-v)=Ortm(x,y,u) + Ortm(x,y,(-v)) by Th1
    .=Ortm(x,y,u) - Ortm(x,y,v) by A1,Th4;
end;

theorem Th6:
  Gen x,y & Ortm(x,y,u)=Ortm(x,y,v) implies u=v
proof
  assume
A1: Gen x,y & Ortm(x,y,u)=Ortm(x,y,v);
  then pr1(x,y,u)*x + (-pr2(x,y,u))*y - (pr1(x,y,v)*x + (-pr2(x,y,v))*y)
  =0.V by RLVECT_1:28;
  then pr1(x,y,u)*x + (-pr2(x,y,u))*y - (pr1(x,y,v)*x) - (-pr2(x,y,v))*y
  =0.V by RLVECT_1:41;
  then pr1(x,y,u)*x + (-(pr1(x,y,v))*x) + ((-pr2(x,y,u))*y) - (-pr2(x,y,v))*y
  =0.V by RLVECT_1:def 6;
  then pr1(x,y,u)*x - pr1(x,y,v)*x + ((-pr2(x,y,u))*y - (-pr2(x,y,v))*y)
  =0.V by RLVECT_1:def 6;
  then (pr1(x,y,u) - pr1(x,y,v))*x + ((-pr2(x,y,u))*y - (-pr2(x,y,v))*y)
  =0.V by RLVECT_1:49;
  then (pr1(x,y,u) - pr1(x,y,v))*x + ((-pr2(x,y,u)) - (-pr2(x,y,v)))*y
  =0.V by RLVECT_1:49;
  then pr1(x,y,u) - pr1(x,y,v)=0 & (-pr2(x,y,u)) - (-pr2(x,y,v))=0
  by A1,ANALMETR:def 1;
  hence u=pr1(x,y,v)*x + pr2(x,y,v)*y by A1,Lm5
    .=v by A1,Lm5;
end;

theorem Th7:
  Gen x,y implies Ortm(x,y,Ortm(x,y,u))=u
proof
  assume
A1: Gen x,y;
  hence Ortm(x,y,Ortm(x,y,u))=
  pr1(x,y,u)*x+(-pr2(x,y,pr1(x,y,u)*x+(-pr2(x,y,u))*y))*y by GEOMTRAP:def 4
    .=pr1(x,y,u)*x+(-(-pr2(x,y,u)))*y by A1,GEOMTRAP:def 5
    .=u by A1,Lm5;
end;

theorem Th8:
  Gen x,y implies ex v st u=Ortm(x,y,v)
proof
  assume
A1: Gen x,y;
  take Ortm(x,y,u);
  thus thesis by A1,Th7;
end;

definition
  let V,x,y;
  let u;
  func Orte(x,y,u) -> VECTOR of V equals

  pr2(x,y,u)*x + (-pr1(x,y,u))*y;
  correctness;
end;

theorem Th9:
  Gen x,y implies Orte(x,y,-v)= -Orte(x,y,v)
proof
  assume
A1: Gen x,y;
  then
A2: -v=-(pr1(x,y,v)*x + pr2(x,y,v)*y) by Lm5
    .=-(pr1(x,y,v)*x) + (-(pr2(x,y,v)*y)) by RLVECT_1:45
    .=pr1(x,y,v)*(-x) + (-(pr2(x,y,v)*y)) by RLVECT_1:39
    .=(-pr1(x,y,v))*x + (-(pr2(x,y,v)*y)) by RLVECT_1:38
    .=(-pr1(x,y,v))*x + pr2(x,y,v)*(-y) by RLVECT_1:39
    .=(-pr1(x,y,v))*x + (-pr2(x,y,v))*y by RLVECT_1:38;
  hence Orte(x,y,-v)=(-pr2(x,y,v))*x + (-pr1(x,y,-v))*y by A1,Lm6
    .=(-pr2(x,y,v))*x + (-(-pr1(x,y,v)))*y by A1,A2,Lm6
    .=pr2(x,y,v)*(-x) + (-(-pr1(x,y,v)))*y by RLVECT_1:38
    .=-(pr2(x,y,v)*x) + (-(-pr1(x,y,v)))*y by RLVECT_1:39
    .=-(pr2(x,y,v)*x) + (-pr1(x,y,v))*(-y) by RLVECT_1:38
    .=-(pr2(x,y,v)*x) + (-((-pr1(x,y,v))*y)) by RLVECT_1:39
    .=-Orte(x,y,v) by RLVECT_1:45;
end;

theorem Th10:
  Gen x,y implies Orte(x,y,u+v)=Orte(x,y,u) + Orte(x,y,v)
proof
  assume
A1: Gen x,y;
  hence Orte(x,y,u+v)=(pr2(x,y,u+v))*x + (-(pr1(x,y,u)+pr1(x,y,v)))*y by Lm7
    .=(pr2(x,y,u)+pr2(x,y,v))*x + (-(pr1(x,y,u)+pr1(x,y,v)))*y by A1,Lm7
    .=pr2(x,y,u)*x + pr2(x,y,v)*x + (-(pr1(x,y,u)+pr1(x,y,v)))*y
  by RLVECT_1:def 9
    .=pr2(x,y,u)*x + pr2(x,y,v)*x + (pr1(x,y,u)+pr1(x,y,v))*(-y)
  by RLVECT_1:38
    .=pr2(x,y,u)*x + pr2(x,y,v)*x + (-((pr1(x,y,u)+pr1(x,y,v))*y))
  by RLVECT_1:39
    .=pr2(x,y,u)*x + pr2(x,y,v)*x + (-(pr1(x,y,u)*y +pr1(x,y,v)*y))
  by RLVECT_1:def 9
    .=pr2(x,y,u)*x + pr2(x,y,v)*x + (-(pr1(x,y,u)*y) +(-(pr1(x,y,v)*y)))
  by RLVECT_1:45
    .=pr2(x,y,u)*x + (pr2(x,y,v)*x + (-(pr1(x,y,u)*y) +(-(pr1(x,y,v)*y))))
  by RLVECT_1:def 6
    .=pr2(x,y,u)*x + (-(pr1(x,y,u)*y) + (pr2(x,y,v)*x +(-(pr1(x,y,v)*y))))
  by RLVECT_1:def 6
    .=pr2(x,y,u)*x + (-(pr1(x,y,u)*y)) + (pr2(x,y,v)*x +(-(pr1(x,y,v)*y)))
  by RLVECT_1:def 6
    .=pr2(x,y,u)*x + (pr1(x,y,u)*(-y)) + (pr2(x,y,v)*x +(-(pr1(x,y,v)*y)))
  by RLVECT_1:39
    .=pr2(x,y,u)*x + (pr1(x,y,u)*(-y)) + (pr2(x,y,v)*x +(pr1(x,y,v)*(-y)))
  by RLVECT_1:39
    .=pr2(x,y,u)*x + ((-pr1(x,y,u))*y) + (pr2(x,y,v)*x +(pr1(x,y,v)*(-y)))
  by RLVECT_1:38
    .=Orte(x,y,u) + Orte(x,y,v) by RLVECT_1:38;
end;

theorem Th11:
  Gen x,y implies Orte(x,y,u-v)=Orte(x,y,u)-Orte(x,y,v)
proof
  assume
A1: Gen x,y;
  hence Orte(x,y,u-v)=Orte(x,y,u) + Orte(x,y,(-v)) by Th10
    .=Orte(x,y,u) - Orte(x,y,v) by A1,Th9;
end;

theorem Th12:
  Gen x,y implies Orte(x,y,n*u)=n*Orte(x,y,u)
proof
  assume
A1: Gen x,y;
  hence Orte(x,y,n*u)=n*pr2(x,y,u)*x + (-pr1(x,y,n*u))*y by Lm7
    .=n*pr2(x,y,u)*x + (-(n*pr1(x,y,u)))*y by A1,Lm7
    .=n*pr2(x,y,u)*x + (n*pr1(x,y,u))*(-y) by RLVECT_1:38
    .=n*pr2(x,y,u)*x + (-(n*pr1(x,y,u)*y)) by RLVECT_1:39
    .=n*pr2(x,y,u)*x + (-(n*(pr1(x,y,u)*y))) by RLVECT_1:def 9
    .=n*pr2(x,y,u)*x + n*(-(pr1(x,y,u)*y)) by RLVECT_1:39
    .=n*(pr2(x,y,u)*x) + n*(-(pr1(x,y,u)*y)) by RLVECT_1:def 9
    .=n*(pr2(x,y,u)*x + (-(pr1(x,y,u)*y))) by RLVECT_1:def 9
    .=n*(pr2(x,y,u)*x + (pr1(x,y,u)*(-y))) by RLVECT_1:39
    .=n*Orte(x,y,u) by RLVECT_1:38;
end;

theorem Th13:
  Gen x,y & Orte(x,y,u)=Orte(x,y,v) implies u=v
proof
  assume
A1: Gen x,y & Orte(x,y,u)=Orte(x,y,v);
  then pr2(x,y,u)*x + (-pr1(x,y,u))*y - (pr2(x,y,v)*x + (-pr1(x,y,v))*y)
  =0.V by RLVECT_1:28;
  then pr2(x,y,u)*x + (-pr1(x,y,u))*y - (pr2(x,y,v)*x) - (-pr1(x,y,v))*y
  =0.V by RLVECT_1:41;
  then pr2(x,y,u)*x + (-(pr2(x,y,v))*x) + ((-pr1(x,y,u))*y) - (-pr1(x,y,v))*y
  =0.V by RLVECT_1:def 6;
  then pr2(x,y,u)*x - pr2(x,y,v)*x + ((-pr1(x,y,u))*y - (-pr1(x,y,v))*y)
  =0.V by RLVECT_1:def 6;
  then (pr2(x,y,u) - pr2(x,y,v))*x + ((-pr1(x,y,u))*y - (-pr1(x,y,v))*y)
  =0.V by RLVECT_1:49;
  then (pr2(x,y,u) - pr2(x,y,v))*x + ((-pr1(x,y,u)) - (-pr1(x,y,v)))*y
  =0.V by RLVECT_1:49;
  then pr2(x,y,u) - pr2(x,y,v)=0 & (-pr1(x,y,u)) - (-pr1(x,y,v))=0
  by A1,ANALMETR:def 1;
  hence u=pr1(x,y,v)*x + pr2(x,y,v)*y by A1,Lm5
    .=v by A1,Lm5;
end;

theorem Th14:
  Gen x,y implies Orte(x,y,Orte(x,y,u)) = -u
proof
  assume
A1: Gen x,y;
  hence Orte(x,y,Orte(x,y,u))=(-pr1(x,y,u))*x+
  (-pr1(x,y,pr2(x,y,u)*x+(-pr1(x,y,u))*y))*y by GEOMTRAP:def 5
    .=(-pr1(x,y,u))*x+(-pr2(x,y,u))*y by A1,GEOMTRAP:def 4
    .=pr1(x,y,u)*(-x)+(-pr2(x,y,u))*y by RLVECT_1:38
    .=-(pr1(x,y,u)*x)+(-pr2(x,y,u))*y by RLVECT_1:39
    .=-(pr1(x,y,u)*x)+pr2(x,y,u)*(-y) by RLVECT_1:38
    .=-(pr1(x,y,u)*x)+(-(pr2(x,y,u)*y)) by RLVECT_1:39
    .=-(pr1(x,y,u)*x+pr2(x,y,u)*y) by RLVECT_1:45
    .=-u by A1,Lm5;
end;

theorem Th15:
  Gen x,y implies ex v st Orte(x,y,v) = u
proof
  assume
A1: Gen x,y;
  take v= -Orte(x,y,u);
  thus Orte(x,y,v) = -Orte(x,y,Orte(x,y,u)) by A1,Th9
    .= -(-u) by A1,Th14
    .= u by RLVECT_1:30;
end;

definition
  let V;
  let x,y,u,v,u1,v1;
  pred u,v,u1,v1 are_COrte_wrt x,y means
  :Def3:
  Orte(x,y,u),Orte(x,y,v) // u1,v1;
  pred u,v,u1,v1 are_COrtm_wrt x,y means
  :Def4:
  Ortm(x,y,u),Ortm(x,y,v) // u1,v1;
end;

theorem Th16:
  Gen x,y implies (u,v // u1,v1 implies
  Orte(x,y,u),Orte(x,y,v) // Orte(x,y,u1),Orte(x,y,v1))
proof
  assume
A1: Gen x,y;
  assume
A2: u,v // u1,v1;
  now
    assume u<>v & u1<>v1;
    then consider a,b such that
A3: 0<a & 0<b and
A4: a*(v-u)=b*(v1-u1) by A2,ANALOAF:def 1;
    a*(Orte(x,y,v)-Orte(x,y,u)) = a*(Orte(x,y,v-u)) by A1,Th11
      .= Orte(x,y,b*(v1-u1)) by A1,A4,Th12
      .= b*(Orte(x,y,v1-u1)) by A1,Th12
      .=b*(Orte(x,y,v1)-Orte(x,y,u1)) by A1,Th11;
    hence Orte(x,y,u),Orte(x,y,v) // Orte(x,y,u1),Orte(x,y,v1)
    by A3,ANALOAF:def 1;
  end;
  hence thesis by ANALOAF:18;
end;

theorem Th17:
  Gen x,y implies (u,v // u1,v1 implies
  Ortm(x,y,u),Ortm(x,y,v) // Ortm(x,y,u1),Ortm(x,y,v1))
proof
  assume
A1: Gen x,y;
  assume
A2: u,v // u1,v1;
  now
    assume
A3: u<>v;
    now
      assume u1<>v1;
      then consider a,b such that
A4:   0<a & 0<b and
A5:   a*(v-u)=b*(v1-u1) by A2,A3,ANALOAF:def 1;
      a*(Ortm(x,y,v)-Ortm(x,y,u)) = a*(Ortm(x,y,v-u)) by A1,Th5
        .= Ortm(x,y,b*(v1-u1)) by A1,A5,Th2
        .= b*(Ortm(x,y,v1-u1)) by A1,Th2
        .=b*(Ortm(x,y,v1)-Ortm(x,y,u1)) by A1,Th5;
      hence thesis by A4,ANALOAF:def 1;
    end;
    hence thesis by ANALOAF:18;
  end;
  hence thesis by ANALOAF:18;
end;

theorem Th18:
  Gen x,y implies (u,u1,v,v1 are_COrte_wrt x,y implies
  v,v1,u1,u are_COrte_wrt x,y)
proof
  assume
A1: Gen x,y;
  assume u,u1,v,v1 are_COrte_wrt x,y;
  then Orte(x,y,u),Orte(x,y,u1) // v,v1 by Def3;
  then v,v1 // Orte(x,y,u),Orte(x,y,u1) by ANALOAF:21;
  then Orte(x,y,v),Orte(x,y,v1) //
  Orte(x,y,Orte(x,y,u)),Orte(x,y,Orte(x,y,u1)) by A1,Th16;
  then Orte(x,y,v),Orte(x,y,v1) // -u,Orte(x,y,Orte(x,y,u1)) by A1,Th14;
  then Orte(x,y,v),Orte(x,y,v1) // -u,-u1 by A1,Th14;
  then
A2: -u,-u1 // Orte(x,y,v),Orte(x,y,v1) by ANALOAF:21;
  -u1-(-u)=u+(-u1) by RLVECT_1:30
    .=u-u1;
  then
A3: -u,-u1 // u1,u by ANALOAF:24;
A4: now
    assume -u<>-u1;
    then Orte(x,y,v),Orte(x,y,v1) // u1,u by A2,A3,ANALOAF:20;
    hence thesis by Def3;
  end;
  now
    assume -u=-u1;
    then u=-(-u1) by RLVECT_1:30
      .= u1 by RLVECT_1:30;
    then Orte(x,y,v),Orte(x,y,v1) // u1,u by ANALOAF:18;
    hence thesis by Def3;
  end;
  hence thesis by A4;
end;

theorem Th19:
  Gen x,y implies (u,u1,v,v1 are_COrtm_wrt x,y implies
  v,v1,u,u1 are_COrtm_wrt x,y)
proof
  assume
A1: Gen x,y;
  assume u,u1,v,v1 are_COrtm_wrt x,y;
  then Ortm(x,y,u),Ortm(x,y,u1) // v,v1 by Def4;
  then v,v1 // Ortm(x,y,u),Ortm(x,y,u1) by ANALOAF:21;
  then Ortm(x,y,v),Ortm(x,y,v1) //
  Ortm(x,y,Ortm(x,y,u)),Ortm(x,y,Ortm(x,y,u1)) by A1,Th17;
  then Ortm(x,y,v),Ortm(x,y,v1) // u,Ortm(x,y,Ortm(x,y,u1)) by A1,Th7;
  then Ortm(x,y,v),Ortm(x,y,v1) // u,u1 by A1,Th7;
  hence thesis by Def4;
end;

theorem Th20:
  u,u,v,w are_COrte_wrt x,y
proof
  Orte(x,y,u),Orte(x,y,u) // v,w by ANALOAF:18;
  hence u,u,v,w are_COrte_wrt x,y by Def3;
end;

theorem
  u,u,v,w are_COrtm_wrt x,y
proof
  Ortm(x,y,u),Ortm(x,y,u) // v,w by ANALOAF:18;
  hence u,u,v,w are_COrtm_wrt x,y by Def4;
end;

theorem
  u,v,w,w are_COrte_wrt x,y
proof
  Orte(x,y,u),Orte(x,y,v) // w,w by ANALOAF:18;
  hence u,v,w,w are_COrte_wrt x,y by Def3;
end;

theorem
  u,v,w,w are_COrtm_wrt x,y
proof
  Ortm(x,y,u),Ortm(x,y,v) // w,w by ANALOAF:18;
  hence u,v,w,w are_COrtm_wrt x,y by Def4;
end;

theorem Th24:
  Gen x,y implies u,v,Orte(x,y,u),Orte(x,y,v) are_Ort_wrt x,y
proof
  assume
A1: Gen x,y;
  set w = Orte(x,y,v) - Orte(x,y,u);
A2: w = Orte(x,y,v-u) by A1,Th11
    .= pr2(x,y,v-u)*x + (-pr1(x,y,v-u))*y;
  PProJ(x,y,v-u,w) = pr1(x,y,v-u)*pr1(x,y,w) + pr2(x,y,v-u)*pr2(x,y,w)
  by GEOMTRAP:def 6
    .= pr1(x,y,v-u)*pr2(x,y,v-u) + pr2(x,y,v-u)*pr2(x,y,w)
  by A1,A2,Lm6
    .= pr1(x,y,v-u)*pr2(x,y,v-u) + (-pr1(x,y,v-u))*pr2(x,y,v-u) by A1,A2,Lm6
    .= 0;
  then v-u,w are_Ort_wrt x,y by A1,GEOMTRAP:34;
  hence thesis by ANALMETR:def 3;
end;

theorem
  u,v,Orte(x,y,u),Orte(x,y,v) are_COrte_wrt x,y
proof
  Orte(x,y,u),Orte(x,y,v) // Orte(x,y,u),Orte(x,y,v) by ANALOAF:17;
  hence u,v,Orte(x,y,u),Orte(x,y,v) are_COrte_wrt x,y by Def3;
end;

theorem
  u,v,Ortm(x,y,u),Ortm(x,y,v) are_COrtm_wrt x,y
proof
  Ortm(x,y,u),Ortm(x,y,v) // Ortm(x,y,u),Ortm(x,y,v) by ANALOAF:17;
  hence u,v,Ortm(x,y,u),Ortm(x,y,v) are_COrtm_wrt x,y by Def4;
end;

theorem
  Gen x,y implies (u,v // u1,v1 iff ex u2,v2 st u2<>v2 &
  u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y)
proof
  assume
A1: Gen x,y;
  (u,v // u1,v1 iff ex u2,v2 st u2<>v2 &
  u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y)
  proof
A2: u,v // u1,v1 implies ex u2,v2 st u2<>v2 &
    u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y
    proof
      assume
A3:   u,v // u1,v1;
A4:   now
        assume
A5:     u=v & u1=v1;
        take u2=0.V,v2=x;
        Orte(x,y,u2),Orte(x,y,v2) // u,v & Orte(x,y,u2),Orte(x,y,v2) // u1,v1
        by A5,ANALOAF:18;
        then
A6:     u2,v2,u1,v1 are_COrte_wrt x,y & u2,v2,u,v are_COrte_wrt x,y by Def3;
        u2<>v2 by A1,Lm4;
        hence thesis by A6;
      end;
A7:   now
        assume
A8:     u<>v;
        consider u2 such that
A9:     Orte(x,y,u2)=u by A1,Th15;
        consider v2 such that
A10:    Orte(x,y,v2)=v by A1,Th15;
        Orte(x,y,u2),Orte(x,y,v2) // u,v by A9,A10,ANALOAF:17;
        then
A11:    u2,v2,u,v are_COrte_wrt x,y by Def3;
        u2,v2,u1,v1 are_COrte_wrt x,y by A3,A9,A10,Def3;
        hence thesis by A8,A9,A10,A11;
      end;
      now
        assume
A12:    u1<>v1;
        consider u2 such that
A13:    Orte(x,y,u2)=u1 by A1,Th15;
        consider v2 such that
A14:    Orte(x,y,v2)=v1 by A1,Th15;
        Orte(x,y,u2),Orte(x,y,v2) // u1,v1 by A13,A14,ANALOAF:17;
        then
A15:    u2,v2,u1,v1 are_COrte_wrt x,y by Def3;
        Orte(x,y,u2),Orte(x,y,v2) // u,v by A3,A13,A14,ANALOAF:21;
        then u2,v2,u,v are_COrte_wrt x,y by Def3;
        hence thesis by A12,A13,A14,A15;
      end;
      hence thesis by A4,A7;
    end;
    (ex u2,v2 st u2<>v2 & u2,v2,u,v are_COrte_wrt x,y &
    u2,v2,u1,v1 are_COrte_wrt x,y) implies u,v // u1,v1
    proof
      given u2,v2 such that
A16:  u2<>v2 & u2,v2,u,v are_COrte_wrt x,y & u2,v2,u1,v1 are_COrte_wrt x,y;
      Orte(x,y,u2),Orte(x,y,v2) // u,v &
      Orte(x,y,u2),Orte(x,y,v2) // u1,v1 by A16,Def3;
      hence thesis by A1,A16,Th13,ANALOAF:20;
    end;
    hence thesis by A2;
  end;
  hence thesis;
end;

theorem
  Gen x,y implies (u,v // u1,v1 iff ex u2,v2 st u2<>v2 &
  u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y)
proof
  assume
A1: Gen x,y;
  (u,v // u1,v1 iff ex u2,v2 st u2<>v2 &
  u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y)
  proof
A2: u,v // u1,v1 implies ex u2,v2 st u2<>v2 &
    u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y
    proof
      assume
A3:   u,v // u1,v1;
A4:   now
        assume
A5:     u=v & u1=v1;
        take u2=0.V,v2=x;
        Ortm(x,y,u2),Ortm(x,y,v2) // u,v & Ortm(x,y,u2),Ortm(x,y,v2) // u1,v1
        by A5,ANALOAF:18;
        then
A6:     u2,v2,u1,v1 are_COrtm_wrt x,y & u2,v2,u,v are_COrtm_wrt x,y by Def4;
        u2<>v2 by A1,Lm4;
        hence thesis by A6;
      end;
A7:   now
        assume
A8:     u<>v;
        consider u2 such that
A9:     Ortm(x,y,u2)=u by A1,Th8;
        consider v2 such that
A10:    Ortm(x,y,v2)=v by A1,Th8;
        Ortm(x,y,u2),Ortm(x,y,v2) // u,v by A9,A10,ANALOAF:17;
        then
A11:    u2,v2,u,v are_COrtm_wrt x,y by Def4;
        u2,v2,u1,v1 are_COrtm_wrt x,y by A3,A9,A10,Def4;
        hence thesis by A8,A9,A10,A11;
      end;
      now
        assume
A12:    u1<>v1;
        consider u2 such that
A13:    Ortm(x,y,u2)=u1 by A1,Th8;
        consider v2 such that
A14:    Ortm(x,y,v2)=v1 by A1,Th8;
        Ortm(x,y,u2),Ortm(x,y,v2) // u1,v1 by A13,A14,ANALOAF:17;
        then
A15:    u2,v2,u1,v1 are_COrtm_wrt x,y by Def4;
        Ortm(x,y,u2),Ortm(x,y,v2) // u,v by A3,A13,A14,ANALOAF:21;
        then u2,v2,u,v are_COrtm_wrt x,y by Def4;
        hence thesis by A12,A13,A14,A15;
      end;
      hence thesis by A4,A7;
    end;
    (ex u2,v2 st u2<>v2 & u2,v2,u,v are_COrtm_wrt x,y &
    u2,v2,u1,v1 are_COrtm_wrt x,y) implies u,v // u1,v1
    proof
      given u2,v2 such that
A16:  u2<>v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y;
      Ortm(x,y,u2),Ortm(x,y,v2) // u,v &
      Ortm(x,y,u2),Ortm(x,y,v2) // u1,v1 by A16,Def4;
      hence thesis by A1,A16,Th6,ANALOAF:20;
    end;
    hence thesis by A2;
  end;
  hence thesis;
end;

theorem
  Gen x,y implies (u,v,u1,v1 are_Ort_wrt x,y iff
  u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y)
proof
  assume
A1: Gen x,y;
A2: now
    assume u=v;
    then v-u=0.V by RLVECT_1:28;
    then v-u,v1-u1 are_Ort_wrt x,y by A1,ANALMETR:9;
    hence u,v,u1,v1 are_Ort_wrt x,y by ANALMETR:def 3;
  end;
  now
    assume
A3: u<>v;
    set u2=Orte(x,y,u),v2=Orte(x,y,v);
A4: v-u<>0.V by A3,RLVECT_1:35;
    u,v,u2,v2 are_Ort_wrt x,y by A1,Th24;
    then
A5: v-u,v2-u2 are_Ort_wrt x,y by ANALMETR:def 3;
A6: now
      assume u,v,u1,v1 are_Ort_wrt x,y;
      then v-u,v1-u1 are_Ort_wrt x,y by ANALMETR:def 3;
      then ex a,b st
      a*(v2-u2)=b*(v1-u1) & (a<>0 or b<>0) by A1,A4,A5,ANALMETR:13;
      then u2,v2 // u1,v1 or u2,v2 // v1,u1 by ANALMETR:18;
      hence u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y by Def3;
    end;
    now
      assume u,v,u1,v1 are_COrte_wrt x,y or u,v,v1,u1 are_COrte_wrt x,y;
      then u2,v2 // u1,v1 or u2,v2 // v1,u1 by Def3;
      then consider a,b such that
A7:   a*(v2-u2)=b*(v1-u1) and
A8:   a<>0 or b<>0 by ANALMETR:18;
A9:   now
        assume
A10:    b=0;
        then 0.V = a*(v2-u2) by A7,RLVECT_1:23;
        then v2-u2=0.V by A8,A10,RLVECT_1:24;
        then v2=u2 by RLVECT_1:35;
        then u=v by A1,Th13;
        then v-u=0.V by RLVECT_1:28;
        then v-u,v1-u1 are_Ort_wrt x,y by A1,ANALMETR:9;
        hence u,v,u1,v1 are_Ort_wrt x,y by ANALMETR:def 3;
      end;
      now
        assume
A11:    b<>0;
        ((b")*a)*(v2-u2)=(b")*(b*(v1-u1)) by A7,RLVECT_1:def 9;
        then ((b")*a)*(v2-u2)=((b")*b)*(v1-u1) by RLVECT_1:def 9;
        then ((b")*a)*(v2-u2)=1*(v1-u1) by A11,XCMPLX_0:def 7;
        then v1-u1=((b")*a)*(v2-u2) by RLVECT_1:def 9;
        then v-u,v1-u1 are_Ort_wrt x,y by A5,ANALMETR:11;
        hence u,v,u1,v1 are_Ort_wrt x,y by ANALMETR:def 3;
      end;
      hence u,v,u1,v1 are_Ort_wrt x,y by A9;
    end;
    hence thesis by A6;
  end;
  hence thesis by A2,Th20;
end;

theorem
  Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,v1,u1 are_COrte_wrt x,y
  implies u=v or u1=v1
proof
  assume
A1: Gen x,y;
  assume
A2: u,v,u1,v1 are_COrte_wrt x,y & u,v,v1,u1 are_COrte_wrt x,y;
  assume
A3: u<>v & u1<>v1;
A4: Orte(x,y,u),Orte(x,y,v) // u1,v1 & Orte(x,y,u),Orte(x,y,v) // v1,u1
  by A2,Def3;
  Orte(x,y,u) <> Orte(x,y,v) by A1,A3,Th13;
  hence contradiction by A3,A4,ANALOAF:19,20;
end;

theorem
  Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,u1 are_COrtm_wrt x,y
  implies u=v or u1=v1
proof
  assume
A1: Gen x,y;
  assume
A2: u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,u1 are_COrtm_wrt x,y;
  assume
A3: u<>v & u1<>v1;
A4: Ortm(x,y,u),Ortm(x,y,v) // u1,v1 & Ortm(x,y,u),Ortm(x,y,v) // v1,u1
  by A2,Def4;
  Ortm(x,y,u) <> Ortm(x,y,v) by A1,A3,Th6;
  hence contradiction by A3,A4,ANALOAF:19,20;
end;

theorem
  Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,u1,w are_COrte_wrt x,y
  implies u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y
proof
  assume
A1: Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,u1,w are_COrte_wrt x,y;
  then
A2: Orte(x,y,u),Orte(x,y,v) // u1,v1 & Orte(x,y,u),Orte(x,y,v) // u1,w
  by Def3;
  now
    assume
A3: u<>v;
    now
      assume
A4:   u1<>v1 & u1<>w;
A5:   u1,v1 // u1,w by A1,A2,A3,Th13,ANALOAF:20;
A6:   now
        assume
A7:     u1,v1 // v1,w;
        u1,v1 // Orte(x,y,u),Orte(x,y,v) by A2,ANALOAF:21;
        then Orte(x,y,u),Orte(x,y,v) // v1,w by A4,A7,ANALOAF:20;
        hence thesis by Def3;
      end;
      now
        assume
A8:     u1,w // w,v1;
        u1,w // Orte(x,y,u),Orte(x,y,v) by A2,ANALOAF:21;
        then Orte(x,y,u),Orte(x,y,v) // w,v1 by A4,A8,ANALOAF:20;
        hence thesis by Def3;
      end;
      hence thesis by A5,A6,ANALOAF:23;
    end;
    hence thesis by A1;
  end;
  hence thesis by Th20;
end;

theorem
  Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,u1,w are_COrtm_wrt x,y
  implies u,v,v1,w are_COrtm_wrt x,y or u,v,w,v1 are_COrtm_wrt x,y
proof
  assume
A1: Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,u1,w are_COrtm_wrt x,y;
  then
A2: Ortm(x,y,u),Ortm(x,y,v) // u1,v1 & Ortm(x,y,u),Ortm(x,y,v) // u1,w
  by Def4;
A3: now
    assume
A4: u<>v & u1<>v1;
    then u1,v1 // u1,w by A1,A2,Th6,ANALOAF:20;
    then
A5: u1,v1 // v1,w or u1,w // w,v1 by ANALOAF:23;
    now
      assume
A6:   u1<>w;
      u1,v1 // Ortm(x,y,u),Ortm(x,y,v) & u1,w // Ortm(x,y,u),Ortm(x,y,v)
      by A2,ANALOAF:21;
      then Ortm(x,y,u),Ortm(x,y,v) // v1,w or
      Ortm(x,y,u),Ortm(x,y,v) // w,v1 by A4,A5,A6,ANALOAF:20;
      hence thesis by Def4;
    end;
    hence thesis by A1;
  end;
  now
    assume u=v;
    then Ortm(x,y,u),Ortm(x,y,v) // v1,w or
    Ortm(x,y,u),Ortm(x,y,v) // w,v1 by ANALOAF:18;
    hence thesis by Def4;
  end;
  hence thesis by A1,A3;
end;

theorem
  u,v,u1,v1 are_COrte_wrt x,y implies v,u,v1,u1 are_COrte_wrt x,y
proof
  assume u,v,u1,v1 are_COrte_wrt x,y;
  then Orte(x,y,u),Orte(x,y,v) // u1,v1 by Def3;
  then Orte(x,y,v),Orte(x,y,u) // v1,u1 by ANALOAF:21;
  hence thesis by Def3;
end;

theorem
  u,v,u1,v1 are_COrtm_wrt x,y implies v,u,v1,u1 are_COrtm_wrt x,y
proof
  assume u,v,u1,v1 are_COrtm_wrt x,y;
  then Ortm(x,y,u),Ortm(x,y,v) // u1,v1 by Def4;
  then Ortm(x,y,v),Ortm(x,y,u) // v1,u1 by ANALOAF:21;
  hence thesis by Def4;
end;

theorem
  Gen x,y & u,v,u1,v1 are_COrte_wrt x,y & u,v,v1,w are_COrte_wrt x,y
  implies u,v,u1,w are_COrte_wrt x,y
proof
  assume
A1: Gen x,y;
  assume
A2: u,v,u1,v1 are_COrte_wrt x,y & u,v,v1,w are_COrte_wrt x,y;
  then
A3: Orte(x,y,u),Orte(x,y,v) // u1,v1 & Orte(x,y,u),Orte(x,y,v) // v1,w
  by Def3;
  then
A4: u1,v1 // Orte(x,y,u),Orte(x,y,v) by ANALOAF:21;
A5: now
    assume u<>v;
    then u1,v1 // v1,w by A1,A3,Th13,ANALOAF:20;
    then
A6: u1,v1 // u1,w by ANALOAF:22;
    now
      assume u1<>v1;
      then Orte(x,y,u),Orte(x,y,v) // u1,w by A4,A6,ANALOAF:20;
      hence thesis by Def3;
    end;
    hence thesis by A2;
  end;
  now
    assume u=v;
    then Orte(x,y,u),Orte(x,y,v) // u1,w by ANALOAF:18;
    hence thesis by Def3;
  end;
  hence thesis by A5;
end;

theorem
  Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,w are_COrtm_wrt x,y
  implies u,v,u1,w are_COrtm_wrt x,y
proof
  assume
A1: Gen x,y;
  assume
A2: u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,w are_COrtm_wrt x,y;
  then
A3: Ortm(x,y,u),Ortm(x,y,v) // u1,v1 & Ortm(x,y,u),Ortm(x,y,v) // v1,w
  by Def4;
  then
A4: u1,v1 // Ortm(x,y,u),Ortm(x,y,v) by ANALOAF:21;
A5: now
    assume u<>v;
    then u1,v1 // v1,w by A1,A3,Th6,ANALOAF:20;
    then
A6: u1,v1 // u1,w by ANALOAF:22;
    now
      assume u1<>v1;
      then Ortm(x,y,u),Ortm(x,y,v) // u1,w by A4,A6,ANALOAF:20;
      hence thesis by Def4;
    end;
    hence thesis by A2;
  end;
  now
    assume u=v;
    then Ortm(x,y,u),Ortm(x,y,v) // u1,w by ANALOAF:18;
    hence thesis by Def4;
  end;
  hence thesis by A5;
end;

theorem
  Gen x,y implies for u,v,w ex u1 st w<>u1 & w,u1,u,v are_COrte_wrt x,y
proof
  assume
A1: Gen x,y;
  let u,v,w;
A2: now
    assume
A3: u=v;
    take u1=w+x;
    Orte(x,y,w),Orte(x,y,u1) // u,v by A3,ANALOAF:18;
    then
A4: w,u1,u,v are_COrte_wrt x,y by Def3;
    now
      assume w=u1;
      then x=0.V by RLVECT_1:22;
      hence contradiction by A1,Lm4;
    end;
    hence thesis by A4;
  end;
  now
    assume
A5: u<>v;
    consider u2 such that
A6: Orte(x,y,u2)=u by A1,Th15;
    consider v2 such that
A7: Orte(x,y,v2)=v by A1,Th15;
    take u1= (v2+w)-u2;
    u2,v2 // w,u1 by ANALOAF:25;
    then w,u1 // u2,v2 by ANALOAF:21;
    then Orte(x,y,w),Orte(x,y,u1) // Orte(x,y,u2),Orte(x,y,v2) by A1,Th16;
    then
A8: w,u1,u,v are_COrte_wrt x,y by A6,A7,Def3;
    now
      assume w=u1;
      then w= w+(v2-u2) by RLVECT_1:def 6;
      then v2-u2=0.V by RLVECT_1:22;
      hence contradiction by A5,A6,A7,RLVECT_1:35;
    end;
    hence thesis by A8;
  end;
  hence thesis by A2;
end;

theorem
  Gen x,y implies for u,v,w ex u1 st w<>u1 & w,u1,u,v are_COrtm_wrt x,y
proof
  assume
A1: Gen x,y;
  let u,v,w;
A2: now
    assume
A3: u=v;
    take u1=w+x;
    Ortm(x,y,w),Ortm(x,y,u1) // u,v by A3,ANALOAF:18;
    then
A4: w,u1,u,v are_COrtm_wrt x,y by Def4;
    now
      assume w=u1;
      then x=0.V by RLVECT_1:22;
      hence contradiction by A1,Lm4;
    end;
    hence thesis by A4;
  end;
  now
    assume
A5: u<>v;
    consider u2 such that
A6: Ortm(x,y,u2)=u by A1,Th8;
    consider v2 such that
A7: Ortm(x,y,v2)=v by A1,Th8;
    take u1= (v2+w)-u2;
    u2,v2 // w,u1 by ANALOAF:25;
    then w,u1 // u2,v2 by ANALOAF:21;
    then Ortm(x,y,w),Ortm(x,y,u1) // Ortm(x,y,u2),Ortm(x,y,v2) by A1,Th17;
    then
A8: w,u1,u,v are_COrtm_wrt x,y by A6,A7,Def4;
    now
      assume w=u1;
      then w= w+(v2-u2) by RLVECT_1:def 6;
      then v2-u2=0.V by RLVECT_1:22;
      hence contradiction by A5,A6,A7,RLVECT_1:35;
    end;
    hence thesis by A8;
  end;
  hence thesis by A2;
end;

theorem Th40:
  Gen x,y implies for u,v,w ex u1 st w<>u1 & u,v,w,u1 are_COrte_wrt x,y
proof
  assume
A1: Gen x,y;
  let u,v,w;
A2: now
    assume
A3: u=v;
    take u1=w+x;
    Orte(x,y,u),Orte(x,y,v) // w,u1 by A3,ANALOAF:18;
    then
A4: u,v,w,u1 are_COrte_wrt x,y by Def3;
    now
      assume w=u1;
      then x=0.V by RLVECT_1:22;
      hence contradiction by A1,Lm4;
    end;
    hence thesis by A4;
  end;
  now
    assume
A5: u<>v;
    consider u2 such that
A6: Orte(x,y,u2)=u by A1,Th15;
    consider v2 such that
A7: Orte(x,y,v2)=v by A1,Th15;
    take u1= (u2+w)-v2;
    v2,u2 // w,u1 by ANALOAF:25;
    then Orte(x,y,v2),Orte(x,y,u2) // Orte(x,y,w),Orte(x,y,u1) by A1,Th16;
    then Orte(x,y,w),Orte(x,y,u1) // v,u by A6,A7,ANALOAF:21;
    then Orte(x,y,u1),Orte(x,y,w) // u,v by ANALOAF:21;
    then
A8: u1,w,u,v are_COrte_wrt x,y by Def3;
    now
      assume w=u1;
      then w= w+(u2-v2) by RLVECT_1:def 6;
      then u2-v2=0.V by RLVECT_1:22;
      hence contradiction by A5,A6,A7,RLVECT_1:35;
    end;
    hence thesis by A1,A8,Th18;
  end;
  hence thesis by A2;
end;

theorem Th41:
  Gen x,y implies for u,v,w ex u1 st w<>u1 & u,v,w,u1 are_COrtm_wrt x,y
proof
  assume
A1: Gen x,y;
  let u,v,w;
A2: now
    assume
A3: u=v;
    take u1=w+x;
    Ortm(x,y,w),Ortm(x,y,u1) // u,v by A3,ANALOAF:18;
    then
A4: w,u1,u,v are_COrtm_wrt x,y by Def4;
    w<>u1
    proof
      assume w=u1;
      then x=0.V by RLVECT_1:22;
      hence contradiction by A1,Lm4;
    end;
    hence thesis by A1,A4,Th19;
  end;
  now
    assume
A5: u<>v;
    consider u2 such that
A6: Ortm(x,y,u2)=u by A1,Th8;
    consider v2 such that
A7: Ortm(x,y,v2)=v by A1,Th8;
    take u1= (v2+w)-u2;
    u2,v2 // w,u1 by ANALOAF:25;
    then w,u1 // u2,v2 by ANALOAF:21;
    then Ortm(x,y,w),Ortm(x,y,u1) // Ortm(x,y,u2),Ortm(x,y,v2) by A1,Th17;
    then
A8: w,u1,u,v are_COrtm_wrt x,y by A6,A7,Def4;
    w<>u1
    proof
      assume w=u1;
      then w= w+(v2-u2) by RLVECT_1:def 6;
      then v2-u2=0.V by RLVECT_1:22;
      hence contradiction by A5,A6,A7,RLVECT_1:35;
    end;
    hence thesis by A1,A8,Th19;
  end;
  hence thesis by A2;
end;

theorem
  Gen x,y & u,u1,v,v1 are_COrte_wrt x,y & w,w1,v,v1 are_COrte_wrt x,y &
  w,w1,u2,v2 are_COrte_wrt x,y implies
  w=w1 or v=v1 or u,u1,u2,v2 are_COrte_wrt x,y
proof
  assume
A1: Gen x,y;
  assume
A2: u,u1,v,v1 are_COrte_wrt x,y &
  w,w1,v,v1 are_COrte_wrt x,y & w,w1,u2,v2 are_COrte_wrt x,y;
  then Orte(x,y,u),Orte(x,y,u1) // v,v1 by Def3;
  then
A3: v,v1 // Orte(x,y,u),Orte(x,y,u1) by ANALOAF:21;
  Orte(x,y,w),Orte(x,y,w1) // v,v1 by A2,Def3;
  then
A4: v,v1 // Orte(x,y,w),Orte(x,y,w1) by ANALOAF:21;
A5: Orte(x,y,w),Orte(x,y,w1) // u2,v2 by A2,Def3;
  now
    assume
A6: w<>w1 & v<>v1;
    Orte(x,y,w),Orte(x,y,w1) // Orte(x,y,u),Orte(x,y,u1)
    by A3,A4,A6,ANALOAF:20;
    then Orte(x,y,u),Orte(x,y,u1) // u2,v2 by A1,A5,A6,Th13,ANALOAF:20;
    hence u,u1,u2,v2 are_COrte_wrt x,y by Def3;
  end;
  hence thesis;
end;

theorem
  Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y & w,w1,v,v1 are_COrtm_wrt x,y &
  w,w1,u2,v2 are_COrtm_wrt x,y implies
  w=w1 or v=v1 or u,u1,u2,v2 are_COrtm_wrt x,y
proof
  assume
A1: Gen x,y;
  assume
A2: u,u1,v,v1 are_COrtm_wrt x,y &
  w,w1,v,v1 are_COrtm_wrt x,y & w,w1,u2,v2 are_COrtm_wrt x,y;
  then Ortm(x,y,u),Ortm(x,y,u1) // v,v1 by Def4;
  then
A3: v,v1 // Ortm(x,y,u),Ortm(x,y,u1) by ANALOAF:21;
  Ortm(x,y,w),Ortm(x,y,w1) // v,v1 by A2,Def4;
  then
A4: v,v1 // Ortm(x,y,w),Ortm(x,y,w1) by ANALOAF:21;
A5: Ortm(x,y,w),Ortm(x,y,w1) // u2,v2 by A2,Def4;
  now
    assume
A6: w<>w1 & v<>v1;
    Ortm(x,y,w),Ortm(x,y,w1) // Ortm(x,y,u),Ortm(x,y,u1)
    by A3,A4,A6,ANALOAF:20;
    then Ortm(x,y,u),Ortm(x,y,u1) // u2,v2 by A1,A5,A6,Th6,ANALOAF:20;
    hence u,u1,u2,v2 are_COrtm_wrt x,y by Def4;
  end;
  hence thesis;
end;

canceled 2;

theorem
  Gen x,y & u,u1,v,v1 are_COrte_wrt x,y & v,v1,w,w1 are_COrte_wrt x,y
  & u2,v2,w,w1 are_COrte_wrt x,y implies
  u,u1,u2,v2 are_COrte_wrt x,y or v=v1 or w=w1
proof
  assume
A1: Gen x,y;
  assume
A2: u,u1,v,v1 are_COrte_wrt x,y &
  v,v1,w,w1 are_COrte_wrt x,y & u2,v2,w,w1 are_COrte_wrt x,y;
  then v,v1,u1,u are_COrte_wrt x,y by A1,Th18;
  then
A3: Orte(x,y,v),Orte(x,y,v1) // u1,u by Def3;
  Orte(x,y,v),Orte(x,y,v1) // w,w1 by A2,Def3;
  then
A4: w,w1 // Orte(x,y,v),Orte(x,y,v1) by ANALOAF:21;
  Orte(x,y,u2),Orte(x,y,v2) // w,w1 by A2,Def3;
  then
A5: w,w1 // Orte(x,y,u2),Orte(x,y,v2) by ANALOAF:21;
  now
    assume
A6: w<>w1 & v<>v1;
    then Orte(x,y,v),Orte(x,y,v1) // Orte(x,y,u2),Orte(x,y,v2)
    by A4,A5,ANALOAF:20;
    then Orte(x,y,u2),Orte(x,y,v2) // u1,u by A1,A3,A6,Th13,ANALOAF:20;
    then Orte(x,y,v2),Orte(x,y,u2) // u,u1 by ANALOAF:21;
    then v2,u2,u,u1 are_COrte_wrt x,y by Def3;
    hence thesis by A1,Th18;
  end;
  hence thesis;
end;

theorem
  Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y & v,v1,w,w1 are_COrtm_wrt x,y
  & u2,v2,w,w1 are_COrtm_wrt x,y implies
  u,u1,u2,v2 are_COrtm_wrt x,y or v=v1 or w=w1
proof
  assume
A1: Gen x,y;
  assume
A2: u,u1,v,v1 are_COrtm_wrt x,y &
  v,v1,w,w1 are_COrtm_wrt x,y & u2,v2,w,w1 are_COrtm_wrt x,y;
  then Ortm(x,y,u),Ortm(x,y,u1) // v,v1 by Def4;
  then
A3: v,v1 // Ortm(x,y,u),Ortm(x,y,u1) by ANALOAF:21;
  w,w1,v,v1 are_COrtm_wrt x,y by A1,A2,Th19;
  then Ortm(x,y,w),Ortm(x,y,w1) // v,v1 by Def4;
  then
A4: v,v1 // Ortm(x,y,w),Ortm(x,y,w1) by ANALOAF:21;
  w,w1,u2,v2 are_COrtm_wrt x,y by A1,A2,Th19;
  then
A5: Ortm(x,y,w),Ortm(x,y,w1) // u2,v2 by Def4;
  now
    assume
A6: w<>w1 & v<>v1;
    then Ortm(x,y,w),Ortm(x,y,w1) // Ortm(x,y,u),Ortm(x,y,u1)
    by A3,A4,ANALOAF:20;
    then Ortm(x,y,u),Ortm(x,y,u1) // u2,v2 by A1,A5,A6,Th6,ANALOAF:20;
    hence thesis by Def4;
  end;
  hence thesis;
end;

theorem
  Gen x,y & u,u1,v,v1 are_COrte_wrt x,y & v,v1,w,w1 are_COrte_wrt x,y
  & u,u1,u2,v2 are_COrte_wrt x,y implies
  u2,v2,w,w1 are_COrte_wrt x,y or v=v1 or u=u1
proof
  assume
A1: Gen x,y;
  assume
A2: u,u1,v,v1 are_COrte_wrt x,y &
  v,v1,w,w1 are_COrte_wrt x,y & u,u1,u2,v2 are_COrte_wrt x,y;
  then
A3: Orte(x,y,u),Orte(x,y,u1) // v,v1 by Def3;
A4: Orte(x,y,v),Orte(x,y,v1) // w,w1 by A2,Def3;
A5: Orte(x,y,u),Orte(x,y,u1) // u2,v2 by A2,Def3;
  now
    assume
A6: u<>u1 & v<>v1;
    then v,v1 // u2,v2 by A1,A3,A5,Th13,ANALOAF:20;
    then Orte(x,y,v),Orte(x,y,v1) // Orte(x,y,u2),Orte(x,y,v2) by A1,Th16;
    then Orte(x,y,u2),Orte(x,y,v2) // w,w1 by A1,A4,A6,Th13,ANALOAF:20;
    hence thesis by Def3;
  end;
  hence thesis;
end;

theorem
  Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y & v,v1,w,w1 are_COrtm_wrt x,y
  & u,u1,u2,v2 are_COrtm_wrt x,y implies
  u2,v2,w,w1 are_COrtm_wrt x,y or v=v1 or u=u1
proof
  assume
A1: Gen x,y;
  assume
A2: u,u1,v,v1 are_COrtm_wrt x,y &
  v,v1,w,w1 are_COrtm_wrt x,y & u,u1,u2,v2 are_COrtm_wrt x,y;
  then
A3: Ortm(x,y,u),Ortm(x,y,u1) // v,v1 by Def4;
A4: Ortm(x,y,v),Ortm(x,y,v1) // w,w1 by A2,Def4;
A5: Ortm(x,y,u),Ortm(x,y,u1) // u2,v2 by A2,Def4;
  now
    assume
A6: u<>u1 & v<>v1;
    then v,v1 // u2,v2 by A1,A3,A5,Th6,ANALOAF:20;
    then Ortm(x,y,v),Ortm(x,y,v1) // Ortm(x,y,u2),Ortm(x,y,v2) by A1,Th17;
    then Ortm(x,y,u2),Ortm(x,y,v2) // w,w1 by A1,A4,A6,Th6,ANALOAF:20;
    hence thesis by Def4;
  end;
  hence thesis;
end;

theorem
  Gen x,y implies (for v,w,u1,v1,w1 holds (not (v,v1,w,u1 are_COrte_wrt x,y) &
  not (v,v1,u1,w are_COrte_wrt x,y) & u1,w1,u1,w are_COrte_wrt x,y)
  implies ex u2 st
  ((v,v1,v,u2 are_COrte_wrt x,y or v,v1,u2,v are_COrte_wrt x,y) &
  (u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y)))
proof
  assume
A1: Gen x,y;
  let v,w,u1,v1,w1;
  consider u such that
A2: v<>u and
X: v,v1,v,u are_COrte_wrt x,y by A1,Th40;
  assume not (v,v1,w,u1 are_COrte_wrt x,y) &
  not (v,v1,u1,w are_COrte_wrt x,y) & u1,w1,u1,w are_COrte_wrt x,y;
  then
A3: not Orte(x,y,v),Orte(x,y,v1) // w,u1 & Orte(x,y,v),Orte(x,y,v1) // v,u &
  Orte(x,y,u1),Orte(x,y,w1) // u1,w &
  not Orte(x,y,v),Orte(x,y,v1) // u1,w by X,Def3;
  then
A4: v,u // Orte(x,y,v),Orte(x,y,v1) &
  u1,w // Orte(x,y,u1),Orte(x,y,w1) by ANALOAF:21;
A5: u1<>w by A3,ANALOAF:18;
A6: not (v,u // u1,w or v,u // w,u1) by A2,A3,A4,ANALOAF:20;
  Gen x,y implies (ex u,v st (for w ex a,b st a*u + b*v=w))
  proof
    assume
A7: Gen x,y;
    take x,y;thus thesis by A7,ANALMETR:def 1;
  end;
  then consider u2 such that
A8: v,u // v,u2 or v,u // u2,v and
A9: u1,w // u1,u2 or u1,w // u2,u1 by A1,A6,ANALOAF:31;
  Orte(x,y,v),Orte(x,y,v1) // v,u2 or Orte(x,y,v),Orte(x,y,v1) // u2,v
  by A2,A4,A8,ANALOAF:20;
  then
A10: v,v1,v,u2 are_COrte_wrt x,y or v,v1,u2,v are_COrte_wrt x,y by Def3;
  Orte(x,y,u1),Orte(x,y,w1) // u1,u2 or Orte(x,y,u1),Orte(x,y,w1) // u2,u1
  by A4,A5,A9,ANALOAF:20;
  then u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y by Def3;
  hence thesis by A10;
end;

theorem
  Gen x,y implies (ex u,v,w st (u,v,u,w are_COrte_wrt x,y &
  for v1,w1 st v1,w1,u,v are_COrte_wrt x,y holds
  (not v1,w1,u,w are_COrte_wrt x,y & not v1,w1,w,u are_COrte_wrt x,y
  or v1=w1)))
proof
  assume
A1: Gen x,y;
  Gen x,y implies ex u,v st u<>v
  proof
    assume
A2: Gen x,y;
    take x,0.V; thus thesis by A2,Lm4;
  end;
  then consider u,v such that
A3: u<>v by A1;
  take u,v;
  consider w such that
A4: w<>u & u,v,u,w are_COrte_wrt x,y by A1,Th40;
  take w;
  thus u,v,u,w are_COrte_wrt x,y by A4;
A5: Orte(x,y,u),Orte(x,y,v) // u,w by A4,Def3;
  let v1,w1;
  assume v1,w1,u,v are_COrte_wrt x,y;
  then
A6: Orte(x,y,v1),Orte(x,y,w1) // u,v by Def3;
  now
    assume
A7: v1<>w1;
    assume v1,w1,u,w are_COrte_wrt x,y or v1,w1,w,u are_COrte_wrt x,y;
    then Orte(x,y,v1),Orte(x,y,w1) // u,w or
    Orte(x,y,v1),Orte(x,y,w1) // w,u by Def3;
    then u,v // u,w or u,v // w,u by A1,A6,A7,Th13,ANALOAF:20;
    then Orte(x,y,u),Orte(x,y,v) // Orte(x,y,u),Orte(x,y,w) or
    Orte(x,y,u),Orte(x,y,v) // Orte(x,y,w),Orte(x,y,u) by A1,Th16;
    then u,w // Orte(x,y,u),Orte(x,y,w) or u,w // Orte(x,y,w),Orte(x,y,u)
    by A1,A3,A5,Th13,ANALOAF:20;
    then consider a,b such that
A8: a*(w-u)=b*(Orte(x,y,w)-Orte(x,y,u)) & (a<>0 or b<>0) by ANALMETR:18;
    take a,b;
    a*(w-u)=b*Orte(x,y,w-u) & (a<>0 or b<>0) by A1,A8,Th11;
    then
A9: a*(pr1(x,y,w-u)*x + pr2(x,y,w-u)*y)=b*Orte(x,y,w-u)
    & (a<>0 or b<>0) by A1,Lm5;
A10: now
      assume
A11:  a<>0;
A12:  pr2(x,y,w-u)<>0
      proof
        assume
A13:    not thesis;
        then a*(pr1(x,y,w-u)*x + pr2(x,y,w-u)*y)=
        (b*0)*x + (b*(-pr1(x,y,w-u)))*y by A9,Lm2;
        then (a*pr1(x,y,w-u))*x + (a*pr2(x,y,w-u))*y=
        (b*0)*x + (b*(-pr1(x,y,w-u)))*y by Lm2;
        then a*pr1(x,y,w-u)=0 by A1,Lm3;
        then pr1(x,y,w-u)=0 by A11,XCMPLX_1:6;
        then w-u=0*x + 0*y by A1,A13,Lm5
          .=0.V + 0*y by RLVECT_1:23
          .=0.V + 0.V by RLVECT_1:23
          .=0.V by RLVECT_1:10;
        hence thesis by A4,RLVECT_1:35;
      end;
      (a"*a)*(pr1(x,y,w-u)*x + pr2(x,y,w-u)*y)=
      a"*(b*(pr2(x,y,w-u)*x + (-pr1(x,y,w-u))*y)) by A9,RLVECT_1:def 9;
      then (a"*a)*(pr1(x,y,w-u)*x + pr2(x,y,w-u)*y)=
      (a"*b)*(pr2(x,y,w-u)*x + (-pr1(x,y,w-u))*y) by RLVECT_1:def 9;
      then 1*(pr1(x,y,w-u)*x + pr2(x,y,w-u)*y)=
      (a"*b)*(pr2(x,y,w-u)*x + (-pr1(x,y,w-u))*y) by A11,XCMPLX_0:def 7;
      then pr1(x,y,w-u)*x + pr2(x,y,w-u)*y=
      (a"*b)*(pr2(x,y,w-u)*x + (-pr1(x,y,w-u))*y) by RLVECT_1:def 9;
      then pr1(x,y,w-u)*x + pr2(x,y,w-u)*y=
      (a"*b)*pr2(x,y,w-u)*x + (a"*b)*(-pr1(x,y,w-u))*y by Lm2;
      then pr1(x,y,w-u)=(a"*b)*pr2(x,y,w-u) &
      pr2(x,y,w-u)=(a"*b)*(-pr1(x,y,w-u)) by A1,Lm3;
      then
A14:  pr2(x,y,w-u)=-((a"*b)*((a"*b)*pr2(x,y,w-u)));
      -(pr2(x,y,w-u)"*pr2(x,y,w-u)) = (pr2(x,y,w-u)"*-pr2(x,y,w-u))
        .= pr2(x,y,w-u)"*((a"*b)*((a"*b)*pr2(x,y,w-u))) by A14;
      then -1=pr2(x,y,w-u)"*pr2(x,y,w-u)*((a"*b)*(a"*b)) by A12,XCMPLX_0:def 7;
      then -1=1*((a"*b)*(a"*b)) by A12,XCMPLX_0:def 7;
      hence thesis by XREAL_1:65;
    end;
    now
      assume
A15:  b<>0;
A16:  pr2(x,y,w-u)<>0
      proof
        assume
A17:    not thesis;
        then a*(pr1(x,y,w-u)*x + 0*y)=
        (b*0)*x + (b*(-pr1(x,y,w-u)))*y by A9,Lm2;
        then (a*pr1(x,y,w-u))*x + (a*0)*y=
        (b*0)*x + (b*(-pr1(x,y,w-u)))*y by Lm2;
        then b*(-pr1(x,y,w-u))=0 by A1,Lm3;
        then -pr1(x,y,w-u)=0 by A15,XCMPLX_1:6;
        then w-u=0*x + (-0)*y by A1,A17,Lm5
          .=0.V + 0*y by RLVECT_1:23
          .=0.V + 0.V by RLVECT_1:23
          .=0.V by RLVECT_1:10;
        hence thesis by A4,RLVECT_1:35;
      end;
      b"*(a*(pr1(x,y,w-u)*x + pr2(x,y,w-u)*y))=
      (b"*b)*(pr2(x,y,w-u)*x + (-pr1(x,y,w-u))*y) by A9,RLVECT_1:def 9;
      then (b"*a)*(pr1(x,y,w-u)*x + pr2(x,y,w-u)*y)=
      (b"*b)*(pr2(x,y,w-u)*x + (-pr1(x,y,w-u))*y) by RLVECT_1:def 9;
      then (b"*a)*(pr1(x,y,w-u)*x + pr2(x,y,w-u)*y)=
      1*(pr2(x,y,w-u)*x + (-pr1(x,y,w-u))*y) by A15,XCMPLX_0:def 7;
      then (b"*a)*(pr1(x,y,w-u)*x + pr2(x,y,w-u)*y)=
      pr2(x,y,w-u)*x + (-pr1(x,y,w-u))*y by RLVECT_1:def 9;
      then (b"*a)*pr1(x,y,w-u)*x + (b"*a)*pr2(x,y,w-u)*y=
      pr2(x,y,w-u)*x + (-pr1(x,y,w-u))*y by Lm2;
      then (b"*a)*pr1(x,y,w-u)=pr2(x,y,w-u) &
      (b"*a)*pr2(x,y,w-u)=-pr1(x,y,w-u) by A1,Lm3;
      then
A18:  pr2(x,y,w-u)=(b"*a)*(-((b"*a)*pr2(x,y,w-u)));
      -(pr2(x,y,w-u)"*pr2(x,y,w-u)) = (pr2(x,y,w-u)"*-pr2(x,y,w-u))
        .= pr2(x,y,w-u)"*((b"*a)*((b"*a)*pr2(x,y,w-u))) by A18;
      then -1=pr2(x,y,w-u)"*pr2(x,y,w-u)*((b"*a)*(b"*a)) by A16,XCMPLX_0:def 7;
      then -1=1*((b"*a)*(b"*a)) by A16,XCMPLX_0:def 7;
      hence thesis by XREAL_1:65;
    end;
    hence thesis by A8,A10;
  end;
  hence thesis;
end;

theorem
  Gen x,y implies (for v,w,u1,v1,w1 holds (not v,v1,w,u1 are_COrtm_wrt x,y &
  not v,v1,u1,w are_COrtm_wrt x,y & u1,w1,u1,w are_COrtm_wrt x,y)
  implies ex u2 st
  ((v,v1,v,u2 are_COrtm_wrt x,y or v,v1,u2,v are_COrtm_wrt x,y) &
  (u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_wrt x,y)))
proof
  assume
A1: Gen x,y;
  let v,w,u1,v1,w1;
  consider u such that
A2: v<>u and
X: v,v1,v,u are_COrtm_wrt x,y by A1,Th41;
  assume not (v,v1,w,u1 are_COrtm_wrt x,y) &
  not (v,v1,u1,w are_COrtm_wrt x,y) & u1,w1,u1,w are_COrtm_wrt x,y;
  then
A3: not Ortm(x,y,v),Ortm(x,y,v1) // w,u1 & Ortm(x,y,v),Ortm(x,y,v1) // v,u &
  Ortm(x,y,u1),Ortm(x,y,w1) // u1,w &
  not Ortm(x,y,v),Ortm(x,y,v1) // u1,w by Def4,X;
  then
A4: v,u // Ortm(x,y,v),Ortm(x,y,v1) &
  u1,w // Ortm(x,y,u1),Ortm(x,y,w1) by ANALOAF:21;
A5: u1<>w by A3,ANALOAF:18;
A6: not (v,u // u1,w or v,u // w,u1) by A2,A3,A4,ANALOAF:20;
  Gen x,y implies (ex u,v st (for w ex a,b st a*u + b*v=w))
  proof
    assume
A7: Gen x,y;
    take x,y;thus thesis by A7,ANALMETR:def 1;
  end;
  then consider u2 such that
A8: v,u // v,u2 or v,u // u2,v and
A9: u1,w // u1,u2 or u1,w // u2,u1 by A1,A6,ANALOAF:31;
  Ortm(x,y,v),Ortm(x,y,v1) // v,u2 or Ortm(x,y,v),Ortm(x,y,v1) // u2,v
  by A2,A4,A8,ANALOAF:20;
  then
A10: v,v1,v,u2 are_COrtm_wrt x,y or v,v1,u2,v are_COrtm_wrt x,y by Def4;
  Ortm(x,y,u1),Ortm(x,y,w1) // u1,u2 or Ortm(x,y,u1),Ortm(x,y,w1) // u2,u1
  by A4,A5,A9,ANALOAF:20;
  then u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_wrt x,y by Def4;
  hence thesis by A10;
end;

theorem
  Gen x,y implies (ex u,v,w st (u,v,u,w are_COrtm_wrt x,y &
  for v1,w1 holds (v1,w1,u,v are_COrtm_wrt x,y implies
  (not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y
  or v1=w1))))
proof
  assume
A1: Gen x,y;
  take u=0*x+0*y,v=1*x+1*y,w=1*x+(-1)*y;
pr1(x,y,u)=0 & pr2(x,y,u)=0 & pr1(x,y,v)=1 & pr2(x,y,v)=1 by A1,Lm6;
then A2: Ortm(x,y,u),Ortm(x,y,v) // u,w by ANALOAF:17;
  for v1,w1 holds (v1,w1,u,v are_COrtm_wrt x,y implies
  (not v1,w1,u,w are_COrtm_wrt x,y & not v1,w1,w,u are_COrtm_wrt x,y
  or v1=w1))
  proof
    let v1,w1;
    assume v1,w1,u,v are_COrtm_wrt x,y;
    then
A3: Ortm(x,y,v1),Ortm(x,y,w1) // u,v by Def4;
    now
      assume
A4:   v1<>w1;
      assume v1,w1,u,w are_COrtm_wrt x,y or v1,w1,w,u are_COrtm_wrt x,y;
      then Ortm(x,y,v1),Ortm(x,y,w1) // u,w or
      Ortm(x,y,v1),Ortm(x,y,w1) // w,u by Def4;
      then u,v // u,w or u,v // w,u by A1,A3,A4,Th6,ANALOAF:20;
      then consider a,b such that
A5:   a*(v-u)=b*(w-u) & (a<>0 or b<>0) by ANALMETR:18;
      take a,b;
      u=0.V+0*y by RLVECT_1:23
        .=0.V+0.V by RLVECT_1:23
        .=0.V by RLVECT_1:10;
      then a*v=b*(w-0.V) & (a<>0 or b<>0) by A5,RLVECT_1:26;
      then
A6:   a*v=b*w & (a<>0 or b<>0) by RLVECT_1:26;
A7:   now
        assume
A8:     a<>0;
        a"*a*v=a"*(b*w) by A6,RLVECT_1:def 9;
        then a"*a*v=a"*b*w by RLVECT_1:def 9;
        then 1*v=a"*b*w by A8,XCMPLX_0:def 7;
        then 1*v=a"*b*1*x+a"*b*(-1)*y by Lm2;
        then 1*1*x+1*1*y=a"*b*1*x+a"*b*(-1)*y by Lm2;
        then a*1=a*(a"*(b*1)) & 1=a"*b*(-1) by A1,Lm3;
        then a*1=a*a"*(b*1) & 1=a"*b*(-1);
        then 1=a"*a*(-1) by A8,XCMPLX_0:def 7;
        hence thesis by A8,XCMPLX_0:def 7;
      end;
      now
        assume
A9:     b<>0;
        b"*a*v=b"*(b*w) by A6,RLVECT_1:def 9;
        then b"*a*v=b"*b*w by RLVECT_1:def 9;
        then b"*a*v=1*w by A9,XCMPLX_0:def 7;
        then b"*a*1*x+b"*a*1*y=1*w by Lm2;
        then b"*a*1*x+b"*a*1*y=1*1*x+1*(-1)*y by Lm2;
        then b*1=b*(b"*(a*1)) & -1=b"*a*1 by A1,Lm3;
        then b*1=b*b"*(a*1) & -1=b"*a*1;
        then -1=b"*b*1 by A9,XCMPLX_0:def 7;
        hence thesis by A9,XCMPLX_0:def 7;
      end;
      hence thesis by A5,A7;
    end;
    hence thesis;
  end;
  hence thesis by A2,Def4;
end;

reserve uu,vv for set;

definition
  let V;
  let x,y;
  func CORTE(V,x,y) -> Relation of [:the carrier of V,the carrier of V:] means
  :Def5:
  [uu,vv] in it iff
  ex u1,u2,v1,v2 st uu=[u1,u2] & vv=[v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y;
  existence
  proof
    set VV = [:the carrier of V,the carrier of V :];
    defpred P[set,set] means ex u1,u2,v1,v2 st $1=[u1,u2] &
    $2=[v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y;
    consider P being Relation of VV,VV such that
A1: for uu,vv holds
    ([uu,vv] in P iff uu in VV & vv in VV & P[uu,vv]) from RELSET_1:sch 1;
    take P;
    let uu,vv;
    thus [uu,vv] in P implies ex u1,u2,v1,v2 st
    uu=[u1,u2] & vv=[v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y by A1;
    assume
A2: ex u1,u2,v1,v2 st uu=[u1,u2] & vv=[v1,v2] & u1,u2,v1,v2 are_COrte_wrt x,y;
    then uu in VV & vv in VV by ZFMISC_1:def 2;
    hence [uu,vv] in P by A1,A2;
  end;
  uniqueness
  proof
    let P,Q be Relation of [:the carrier of V,the carrier of V:] such that
A3: [uu,vv] in P iff ex u1,u2,v1,v2 st uu=[u1,u2] & vv=[v1,v2] &
    u1,u2,v1,v2 are_COrte_wrt x,y and
A4: [uu,vv] in Q iff ex u1,u2,v1,v2 st uu=[u1,u2] & vv=[v1,v2] &
    u1,u2,v1,v2 are_COrte_wrt x,y;
    for uu,vv holds [uu,vv] in P iff [uu,vv] in Q
    proof
      let uu,vv;
      [uu,vv] in P iff ex u1,u2,v1,v2 st uu=[u1,u2] & vv=[v1,v2] &
      u1,u2,v1,v2 are_COrte_wrt x,y by A3;
      hence thesis by A4;
    end;
    hence thesis by RELAT_1:def 2;
  end;
end;

definition
  let V;
  let x,y;
  func CORTM(V,x,y) -> Relation of [:the carrier of V,the carrier of V:] means
  :Def6:
  [uu,vv] in it iff
  ex u1,u2,v1,v2 st uu=[u1,u2] & vv=[v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y;
  existence
  proof
    set VV = [:the carrier of V,the carrier of V :];
    defpred P[set,set] means ex u1,u2,v1,v2 st $1=[u1,u2] &
    $2=[v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y;
    consider P being Relation of VV,VV such that
A1: for uu,vv holds
    ([uu,vv] in P iff uu in VV & vv in VV & P[uu,vv]) from RELSET_1:sch 1;
    take P;
    let uu,vv;
    thus [uu,vv] in P implies ex u1,u2,v1,v2 st
    uu=[u1,u2] & vv=[v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y by A1;
    assume
A2: ex u1,u2,v1,v2 st uu=[u1,u2] & vv=[v1,v2] & u1,u2,v1,v2 are_COrtm_wrt x,y;
    then uu in VV & vv in VV by ZFMISC_1:def 2;
    hence [uu,vv] in P by A1,A2;
  end;
  uniqueness
  proof
    let P,Q be Relation of [:the carrier of V,the carrier of V:] such that
A3: [uu,vv] in P iff ex u1,u2,v1,v2 st uu=[u1,u2] & vv=[v1,v2] &
    u1,u2,v1,v2 are_COrtm_wrt x,y and
A4: [uu,vv] in Q iff ex u1,u2,v1,v2 st uu=[u1,u2] & vv=[v1,v2] &
    u1,u2,v1,v2 are_COrtm_wrt x,y;
    for uu,vv holds [uu,vv] in P iff [uu,vv] in Q
    proof
      let uu,vv;
      [uu,vv] in P iff ex u1,u2,v1,v2 st uu=[u1,u2] & vv=[v1,v2] &
      u1,u2,v1,v2 are_COrtm_wrt x,y by A3;
      hence thesis by A4;
    end;
    hence thesis by RELAT_1:def 2;
  end;
end;

definition
  let V;
  let x,y;
  func CESpace(V,x,y) -> strict AffinStruct equals
  AffinStruct (# the carrier of V,CORTE(V,x,y) #);
  correctness;
end;

registration
  let V;
  let x,y;
  cluster CESpace(V,x,y) -> non empty;
  coherence;
end;

definition
  let V;
  let x,y;
  func CMSpace(V,x,y) -> strict AffinStruct equals
  AffinStruct (# the carrier of V,CORTM(V,x,y) #);
  correctness;
end;

registration
  let V;
  let x,y;
  cluster CMSpace(V,x,y) -> non empty;
  coherence;
end;

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

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

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

theorem
  u=p & v=q & u1=r & v1=s implies (p,q // r,s iff u,v,u1,v1 are_COrte_wrt x,y
  )
proof
  assume
A1: u=p & v=q & u1=r & v1=s;
A2: p,q // r,s implies u,v,u1,v1 are_COrte_wrt x,y
  proof
    assume p,q // r,s;
    then [[p,q],[r,s]] in the CONGR of CESpace(V,x,y) by ANALOAF:def 2;
    then consider u1',u2',v1',v2' being VECTOR of V such that
A3: [u,v]=[u1',u2'] & [u1,v1]=[v1',v2'] and
A4: u1',u2',v1',v2' are_COrte_wrt x,y by A1,Def5;
    u=u1' & v=u2' & u1=v1' & v1=v2' by A3,ZFMISC_1:33;
    hence thesis by A4;
  end;
  u,v,u1,v1 are_COrte_wrt x,y implies p,q // r,s
  proof
    assume u,v,u1,v1 are_COrte_wrt x,y;
    then [[u,v],[u1,v1]] in the CONGR of
    AffinStruct (# the carrier of V,CORTE(V,x,y) #) by Def5;
    hence thesis by A1,ANALOAF:def 2;
  end;
  hence thesis by A2;
end;

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

theorem
  u=p & v=q & u1=r & v1=s implies (p,q // r,s iff u,v,u1,v1 are_COrtm_wrt x,y
  )
proof
  assume
A1: u=p & v=q & u1=r & v1=s;
A2: p,q // r,s implies u,v,u1,v1 are_COrtm_wrt x,y
  proof
    assume p,q // r,s;
    then [[p,q],[r,s]] in the CONGR of CMSpace(V,x,y) by ANALOAF:def 2;
    then consider u1',u2',v1',v2' being VECTOR of V such that
A3: [u,v]=[u1',u2'] & [u1,v1]=[v1',v2'] and
A4: u1',u2',v1',v2' are_COrtm_wrt x,y by A1,Def6;
    u=u1' & v=u2' & u1=v1' & v1=v2' by A3,ZFMISC_1:33;
    hence thesis by A4;
  end;
  u,v,u1,v1 are_COrtm_wrt x,y implies p,q // r,s
  proof
    assume u,v,u1,v1 are_COrtm_wrt x,y;
    then [[u,v],[u1,v1]] in the CONGR of
    AffinStruct (# the carrier of V,CORTM(V,x,y) #) by Def6;
    hence thesis by A1,ANALOAF:def 2;
  end;
  hence thesis by A2;
end;