:: Semi-Affine Space
::  by Eugeniusz Kusak and Krzysztof Radziszewski
::
:: Received November 30, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, ANALOAF, SUBSET_1, DIRAF, PARSP_2, FDIFF_1, SEMI_AF1;
 notations STRUCT_0, ANALOAF, DIRAF;
 constructors DIRAF;
 registrations ANALOAF, STRUCT_0;
 theorems PARDEPAP, DIRAF;

begin

definition
  let IT be non empty AffinStruct;
  attr IT is Semi_Affine_Space-like means
  :Def1:
  (for a,b being Element of IT holds a,b // b,a) &
  (for a,b,c being Element of IT holds a,b // c,c) &
  (for a,b,p,q,r,s being Element of IT holds
  ( a<>b & a,b // p,q & a,b // r,s implies p,q // r,s )) &
  (for a,b,c being Element of IT holds ( a,b // a,c implies b,a // b,c )) &
  (ex a,b,c being Element of IT st not a,b // a,c) &
  (for a,b,p being Element of IT
    ex q being Element of IT st ( a,b // p,q & a,p // b,q )) &
  (for o,a being Element of IT holds
   (ex p being Element of IT st
   (for b,c being Element of IT holds o,a // o,p &
   (ex d being Element of IT st
    ( o,p // o,b implies o,c // o,d & p,c // b,d ))))) &
  (for o,a,a9,b,b9,c,c9 being Element of IT holds
    ( not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c //
      o,c9 & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )) &
  (for a,a9,b,b9,c,c9 being Element of IT holds
    ( not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 &
      a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )) &
  (for a1,a2,a3,b1,b2,b3 being Element of IT holds
    ( a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2
      implies a3,b1 // a1,b3 )) &
  for a,b,c,d being Element of IT holds
    ( not a,b // a,c & a,b // c,d & a,c // b,d implies not a,d // b,c );
end;

registration
  cluster Semi_Affine_Space-like for non empty AffinStruct;
  existence
  proof
    consider SAS being AffinPlane such that
A1: ( ( for o,a,a9,b,b9,c,c9 being Element of SAS holds ( not o,a // o
,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,b9 &
a,c // a9,c9 implies b,c // b9,c9 ))& for a,a9,b,b9,c,c9 being Element of SAS
holds ( not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b
    // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 ) )&( ( for a1,a2,a3,b1,b2,b3
being Element of SAS holds ( a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 &
    a2,b3 // a3,b2 implies a3,b1 // a1,b3 ))& for a,b,c,d being Element of SAS
holds ( not a,b // a,c & a,b // c,d & a,c // b,d implies not a,d // b,c ) ) by
PARDEPAP:4;
    reconsider AS=SAS as non empty AffinStruct;
    take AS;
    thus for a,b being Element of AS holds a,b // b,a by DIRAF:40;
    thus thesis by A1,DIRAF:40,PARDEPAP:5;
  end;
end;

definition
  mode Semi_Affine_Space is Semi_Affine_Space-like non empty AffinStruct;
end;

::
::                        AXIOMS OF SEMI_AFFINE SPACE
::

reserve SAS for Semi_Affine_Space;
reserve a,a9,a1,a2,a3,a4,b,b9,c,c9,d,d9,d1,d2,o,p,p1,p2,q,r,r1,r2,s,x, y,t,z
  for Element of SAS;

theorem Th1:
  a,b // a,b
proof
  b,a // b,b by Def1;
  hence thesis by Def1;
end;

theorem Th2:
  a,b // c,d implies c,d // a,b
proof
  assume
A1: a,b // c,d;
  a,b // a,b by Th1;
  then a<>b implies c,d // a,b by A1,Def1;
  hence thesis by Def1;
end;

theorem Th3:
  a,a // b,c
proof
  b,c // a,a by Def1;
  hence thesis by Th2;
end;

theorem Th4:
  a,b // c,d implies b,a // c,d
proof
  assume
A1: a,b // c,d;
  a,b // b,a by Def1;
  then a<>b implies b,a // c,d by A1,Def1;
  hence thesis by A1;
end;

theorem Th5:
  a,b // c,d implies a,b // d,c
proof
  assume a,b // c,d;
  then c,d // a,b by Th2;
  then d,c // a,b by Th4;
  hence thesis by Th2;
end;

theorem Th6:
  a,b // c,d implies b,a // c,d & a,b // d,c & b,a // d,c & c,d //
  a,b & d,c // a,b & c,d // b,a & d,c // b,a
proof
  assume a,b // c,d;
  then c,d // a,b by Th2;
  then
A1: d,c // a,b by Th4;
  then
A2: d,c // b,a by Th5;
  then c,d // b,a by Th4;
  hence thesis by A1,A2,Th2,Th4;
end;

theorem Th7:
  a,b // a,c implies a,c // a,b & b,a // a,c & a,b // c,a & a,c //
b,a & b,a // c,a & c,a // a,b & c,a // b,a & b,a // b,c & a,b // b,c & b,a // c
,b & b,c // b,a & a,b // c,b & c,b // b,a & b,c // a,b & c,b // a,b & c,a // c,
b & a,c // c,b & c,a // b,c & a,c // b,c & c,b // c,a & b,c // c,a & c,b // a,c
  & b,c // a,c
proof
  assume
A1: a,b // a,c;
  then a,c // a,b by Th2;
  then
A2: c,a // c,b by Def1;
  b,a // b,c by A1,Def1;
  hence thesis by A1,A2,Th6;
end;

theorem Th8:
  a<>b & p,q // a,b & a,b // r,s implies p,q // r,s
proof
  assume that
A1: a<>b and
A2: p,q // a,b and
A3: a,b // r,s;
  a,b // p,q by A2,Th6;
  hence thesis by A1,A3,Def1;
end;

theorem
  not a,b // a,d implies a<>b & b<>d & d<>a by Def1,Th1,Th3;

theorem
  not a,b // p,q implies a<>b & p<>q by Def1,Th3;

theorem
  a,b // a,x & b,c // b,x & c,a // c,x implies a,b // a,c
proof
  assume that
A1: a,b // a,x and
A2: b,c // b,x and
A3: c,a // c,x;
  now
    assume
A4: a<>x;
    a,x // a,b & a,x // a,c by A1,A3,Th7;
    hence thesis by A4,Def1;
  end;
  hence thesis by A2,Th7;
end;

theorem Th12:
  not a,b // a,c & p<>q implies not p,q // p,a or not p,q // p,b
  or not p,q // p,c
proof
  assume that
A1: not a,b // a,c and
A2: p<>q;
  now
    assume that
A3: a<>p and
A4: p,q // p,a and
A5: p,q // p,b and
A6: p,q // p,c;
    p,a // p,c by A2,A4,A6,Def1;
    then
A7: a,p // a,c by Def1;
    p,a // p,b by A2,A4,A5,Def1;
    then a,p // a,b by Def1;
    hence contradiction by A1,A3,A7,Def1;
  end;
  hence thesis by A1,A2,Def1;
end;

theorem Th13:
  p<>q implies ex r st not p,q // p,r
proof
  consider a,b,c such that
A1: not a,b // a,c by Def1;
  assume p<>q;
  then not p,q // p,a or not p,q // p,b or not p,q // p,c by A1,Th12;
  hence thesis;
end;

theorem Th14:
  not a,b // a,c implies not a,b // c,a & not b,a // a,c & not b,a
  // c,a & not a,c // a,b & not a,c // b,a & not c,a // a,b & not c,a // b,a &
not b,a // b,c & not b,a // c,b & not a,b // b,c & not a,b // c,b & not b,c //
b,a & not b,c // a,b & not c,b // a,b & not c,b // b,a & not c,b // c,a & not c
,b // a,c & not b,c // c,a & not b,c // a,c & not c,a // c,b & not c,a // b,c &
  not a,c // b,c & not a,c // c,b
proof
  assume
A1: not a,b // a,c;
A2: now
    assume a,c // c,b;
    then c,a // c,b by Th6;
    hence contradiction by A1,Th7;
  end;
  assume
A3: not thesis;
  not b,a // b,c by A1,Th7;
  hence thesis by A1,A3,A2,Th6;
end;

theorem Th15:
  not a,b // c,d & a,b // p,q & c,d // r,s & p<>q & r<>s implies not p,q // r,s
proof
  assume that
A1: not a,b // c,d and
A2: a,b // p,q and
A3: c,d // r,s and
A4: p<>q and
A5: r<>s;
  assume p,q // r,s;
  then a,b // r,s by A2,A4,Th8;
  then
A6: r,s // a,b by Th6;
  r,s // c,d by A3,Th6;
  hence contradiction by A1,A5,A6,Def1;
end;

theorem Th16:
  not a,b // a,c & a,b // p,q & a,c // p,r & b,c // q,r & p<>q
  implies not p,q // p,r
proof
  assume that
A1: not a,b // a,c and
A2: a,b // p,q and
A3: a,c // p,r and
A4: b,c // q,r and
A5: p<>q;
  now
    assume p=r;
    then
A6: p,q // b,c by A4,Th6;
    p,q // a,b by A2,Th6;
    then a,b // b,c by A5,A6,Def1;
    then b,a // b,c by Th4;
    hence contradiction by A1,Th7;
  end;
  hence thesis by A1,A2,A3,A5,Th15;
end;

theorem Th17:
  not a,b // a,c & a,c // p,r & b,c // p,r implies p=r
proof
  assume that
A1: ( not a,b // a,c)& a,c // p,r and
A2: b,c // p,r;
A3: p,r // b,c by A2,Th6;
  ( not a,c // b,c)& p,r // a,c by A1,Th6,Th14;
  hence thesis by A3,Def1;
end;

theorem Th18:
  not p,q // p,r1 & p,r1 // p,r2 & q,r1 // q,r2 implies r1=r2
proof
  assume that
A1: ( not p,q // p,r1)& p,r1 // p,r2 and
A2: q,r1 // q,r2;
A3: r1,r2 // r1,q by A2,Th14;
  ( not r1,p // r1,q)& r1,r2 // r1,p by A1,Th14;
  hence thesis by A3,Def1;
end;

theorem Th19:
  not a,b // a,c & a,b // p,q & a,c // p,r1 & a,c // p,r2 & b,c //
  q,r1 & b,c // q,r2 implies r1=r2
proof
  assume that
A1: not a,b // a,c and
A2: a,b // p,q and
A3: a,c // p,r1 and
A4: a,c // p,r2 and
A5: b,c // q,r1 and
A6: b,c // q,r2;
A7: now
    b<>c by A1,Th1;
    then
A8: q,r1 // q,r2 by A5,A6,Def1;
    a<>c by A1,Def1;
    then
A9: p,r1 // p,r2 by A3,A4,Def1;
    assume p<>q;
    then not p,q // p,r1 by A1,A2,A3,A5,Th16;
    hence thesis by A9,A8,Th18;
  end;
  now
    assume
A10: p=q;
    then p=r1 by A1,A3,A5,Th17;
    hence thesis by A1,A4,A6,A10,Th17;
  end;
  hence thesis by A7;
end;

theorem
  a=b or c =d or a=c & b=d or a=d & b=c implies a,b // c,d by Def1,Th1,Th3;

theorem
  a=b or a=c or b=c implies a,b // a,c by Def1,Th1,Th3;

::
::          BASIC FACTS ABOUT COLLINEARITY RELATION
::

definition
  let SAS,a,b,c;
  pred a,b,c is_collinear means
  :Def2:
  a,b // a,c;
end;

theorem Th22:
  a1,a2,a3 is_collinear implies a1,a3,a2 is_collinear & a2,a1,a3
  is_collinear & a2,a3,a1 is_collinear & a3,a1,a2 is_collinear & a3,a2,a1
  is_collinear
proof
  assume a1,a2,a3 is_collinear;
  then
A1: a1,a2 // a1,a3 by Def2;
  then
A2: a2,a3 // a2,a1 & a3,a2 // a3,a1 by Th7;
A3: a3,a1 // a3,a2 by A1,Th7;
  a1,a3 // a1,a2 & a2,a1 // a2,a3 by A1,Th7;
  hence thesis by A2,A3,Def2;
end;

theorem Th23:
  not a,b,c is_collinear & a,b // p,q & a,c // p,r & p<>q & p<>r
  implies not p,q,r is_collinear
proof
  assume that
A1: not a,b,c is_collinear and
A2: a,b // p,q & a,c // p,r & p<>q & p<>r;
  not a,b // a,c by A1,Def2;
  then not p,q // p,r by A2,Th15;
  hence thesis by Def2;
end;

theorem Th24:
  a=b or b=c or c =a implies a,b,c is_collinear
proof
  assume a=b or b=c or c =a;
  then a,b // a,c by Def1,Th1,Th3;
  hence thesis by Def2;
end;

theorem Th25:
  p<>q implies ex r st not p,q,r is_collinear
proof
  assume p<>q;
  then consider r such that
A1: not p,q // p,r by Th13;
  take r;
  thus thesis by A1,Def2;
end;

theorem Th26:
  a,b,c is_collinear & a,b,d is_collinear implies a,b // c,d
proof
  assume that
A1: a,b,c is_collinear and
A2: a,b,d is_collinear;
  now
    assume that
A3: a<>b and
A4: a<>c;
A5: a,b // a,c by A1,Def2;
    a,b // a,d by A2,Def2;
    then a,c // a,d by A3,A5,Def1;
    then a,c // c,d by Th7;
    hence thesis by A4,A5,Th8;
  end;
  hence thesis by A2,Def2,Th3;
end;

theorem Th27:
  not a,b,c is_collinear & a,b // c,d implies not a,b,d is_collinear
proof
  assume that
A1: not a,b,c is_collinear and
A2: a,b // c,d;
  now
    assume that
A3: c <>d and
A4: a,b,d is_collinear;
    a,b // a,d by A4,Def2;
    then
A5: a,b // d,a by Th6;
A6: a,b // d,c by A2,Th6;
A7: a,c // c,a by Def1;
A8: not a,b // a,c by A1,Def2;
    then a<>b by Th3;
    then
A9: d,c // d,a by A6,A5,Def1;
    c <>a by A8,Def1;
    then not c,d // c,a by A2,A3,A8,A7,Th15;
    hence contradiction by A9,Th7;
  end;
  hence thesis by A1;
end;

theorem Th28:
  not a,b,c is_collinear & a,b // c,d & c <>d & c,d,x is_collinear
  implies not a,b,x is_collinear
proof
  assume that
A1: ( not a,b,c is_collinear)& a,b // c,d & c <>d and
A2: c,d,x is_collinear;
  c,d // c,x by A2,Def2;
  hence thesis by A1,Th8,Th27;
end;

theorem
  not o,a,b is_collinear & o,a,x is_collinear & o,b,x is_collinear implies o=x
proof
  assume that
A1: not o,a,b is_collinear and
A2: o,a,x is_collinear and
A3: o,b,x is_collinear;
  b,o,x is_collinear by A3,Th22;
  then
A4: b,o // b,x by Def2;
  o,a // o,x by A2,Def2;
  then
A5: a,o // a,x by Th14;
  not a,b,o is_collinear by A1,Th22;
  then not a,b // a,o by Def2;
  hence thesis by A5,A4,Th18;
end;

theorem
  o<>a & o<>b & o,a,b is_collinear & o,a,a9 is_collinear & o,b,b9
  is_collinear implies a,b // a9,b9
proof
  assume that
A1: o<>a and
A2: o<>b and
A3: o,a,b is_collinear and
A4: o,a,a9 is_collinear and
A5: o,b, b9 is_collinear;
A6: now
A7: o,a // o,b by A3,Def2;
    o,a // o,a9 by A4,Def2;
    then
A8: o,b // o,a9 by A1,A7,Def1;
    o,b // o,b9 by A5,Def2;
    then o,a9 // o,b9 by A2,A8,Def1;
    then
A9: o,a9 // a9,b9 by Th7;
    o,b // a,b by A7,Th7;
    then
A10: a,b // o,a9 by A2,A8,Def1;
    assume o<>a9;
    hence thesis by A10,A9,Th8;
  end;
  now
    assume
A11: o=a9;
    then a9,a // a9,b by A3,Def2;
    then
A12: a,b // a9,b by Th7;
    a9,b // a9,b9 by A5,A11,Def2;
    hence thesis by A2,A11,A12,Th8;
  end;
  hence thesis by A6;
end;

theorem
  not a,b // c,d & a,b,p1 is_collinear & a,b,p2 is_collinear & c,d,p1
  is_collinear & c,d,p2 is_collinear implies p1=p2
proof
  assume that
A1: not a,b // c,d and
A2: a,b,p1 is_collinear & a,b,p2 is_collinear and
A3: c,d,p1 is_collinear & c,d,p2 is_collinear;
  c,d // p1,p2 by A3,Th26;
  then
A4: p1,p2 // c,d by Th6;
  a,b // p1,p2 by A2,Th26;
  then p1,p2 // a,b by Th6;
  hence thesis by A1,A4,Def1;
end;

theorem Th32:
  a<>b & a,b,c is_collinear & a,b // c,d implies a,c // b,d
proof
  assume that
A1: a<>b and
A2: a,b,c is_collinear and
A3: a,b // c,d;
  now
A4: a,b // a,c by A2,Def2;
    then a,b // c,b by Th7;
    then c,b // c,d by A1,A3,Def1;
    then
A5: b,c // b,d by Th7;
    assume
A6: b<>c;
    b,c // a,c by A4,Th7;
    hence thesis by A6,A5,Def1;
  end;
  hence thesis by A3;
end;

theorem Th33:
  a<>b & a,b,c is_collinear & a,b // c,d implies c,b // c,d
proof
  assume that
A1: a<>b and
A2: a,b,c is_collinear and
A3: a,b // c,d;
  now
    a,b // a,c by A2,Def2;
    then
A4: a,c // c,b & a,c // c,d by A1,A3,Def1,Th7;
    assume a<>c;
    hence thesis by A4,Def1;
  end;
  hence thesis by A3;
end;

theorem Th34:
  not o,a,c is_collinear & o,a,b is_collinear & o,c,d1
  is_collinear & o,c,d2 is_collinear & a,c // b,d1 & a,c // b,d2 implies d1=d2
proof
  assume that
A1: ( not o,a,c is_collinear)& o,a,b is_collinear and
A2: o,c,d1 is_collinear & o,c,d2 is_collinear and
A3: a,c // b,d1 & a,c // b,d2;
A4: o,c // o,d1 & o,c // o,d2 by A2,Def2;
  ( not o,a // o,c)& o,a // o,b by A1,Def2;
  hence thesis by A3,A4,Th19;
end;

theorem
  a<>b & a,b,c is_collinear & a,b,d is_collinear implies a,c,d is_collinear
proof
  assume that
A1: a<>b and
A2: a,b,c is_collinear & a,b,d is_collinear;
  a,b // a,c & a,b // a,d by A2,Def2;
  then a,c // a,d by A1,Def1;
  hence thesis by Def2;
end;

::
::                              PARALLELOGRAM
::

definition
  let SAS,a,b,c,d;
  pred parallelogram a,b,c,d means
  :Def3:
  not a,b,c is_collinear & a,b // c,d & a,c // b,d;
end;

theorem Th36:
  parallelogram a,b,c,d implies a<>b & a<>c & c <>b & a<>d & b<>d & c <>d
proof
  assume
A1: parallelogram a,b,c,d;
  then not a,b,c is_collinear by Def3;
  hence a<>b & a<>c & c <>b by Th24;
A2: now
    assume a=d;
    then a,b // c,a by A1,Def3;
    then
A3: a,b // a,c by Th6;
    not a,b,c is_collinear by A1,Def3;
    hence contradiction by A3,Def2;
  end;
A4: now
    assume c =d;
    then a,c // b,c by A1,Def3;
    then c,a // c,b by Th6;
    then
A5: c,a,b is_collinear by Def2;
    not a,b,c is_collinear by A1,Def3;
    hence contradiction by A5,Th22;
  end;
A6: now
    assume b=d;
    then a,b // c,b by A1,Def3;
    then b,a // b,c by Th6;
    then
A7: b,a,c is_collinear by Def2;
    not a,b,c is_collinear by A1,Def3;
    hence contradiction by A7,Th22;
  end;
  assume not thesis;
  hence contradiction by A2,A6,A4;
end;

theorem Th37:
  parallelogram a,b,c,d implies not a,b,c is_collinear & not b,a,d
  is_collinear & not c,d,a is_collinear & not d,c,b is_collinear
proof
A1: a,b // b,a by Def1;
  assume
A2: parallelogram a,b,c,d;
  hence not a,b,c is_collinear by Def3;
A3: b<>a & b<>d by A2,Th36;
  a,c // b,d by A2,Def3;
  then
A4: a,c // d,b by Th6;
  a,b // c,d by A2,Def3;
  then
A5: a,b // d,c by Th6;
  ( not a,b,c is_collinear)& a,c // b,d by A2,Def3;
  hence not b,a,d is_collinear by A1,A3,Th23;
A6: a,c // c,a by Def1;
A7: c <>d & c <>a by A2,Th36;
  ( not a,b,c is_collinear)& a,b // c,d by A2,Def3;
  hence not c,d,a is_collinear by A6,A7,Th23;
A8: d<>b by A2,Th36;
  ( not a,b,c is_collinear)& c <>d by A2,Def3,Th36;
  hence thesis by A5,A4,A8,Th23;
end;

theorem Th38:
  parallelogram a1,a2,a3,a4 implies not a1,a2,a3 is_collinear &
  not a1,a3,a2 is_collinear & not a1,a2,a4 is_collinear & not a1,a4,a2
is_collinear & not a1,a3,a4 is_collinear & not a1,a4,a3 is_collinear & not a2,
  a1,a3 is_collinear & not a2,a3,a1 is_collinear & not a2,a1,a4 is_collinear &
  not a2,a4,a1 is_collinear & not a2,a3,a4 is_collinear & not a2,a4,a3
is_collinear & not a3,a1,a2 is_collinear & not a3,a2,a1 is_collinear & not a3,
  a1,a4 is_collinear & not a3,a4,a1 is_collinear & not a3,a2,a4 is_collinear &
  not a3,a4,a2 is_collinear & not a4,a1,a2 is_collinear & not a4,a2,a1
is_collinear & not a4,a1,a3 is_collinear & not a4,a3,a1 is_collinear & not a4,
  a2,a3 is_collinear & not a4,a3,a2 is_collinear
proof
  assume
A1: parallelogram a1,a2,a3,a4;
  then
A2: ( not a3,a4,a1 is_collinear)& not a4,a3,a2 is_collinear by Th37;
  ( not a1,a2,a3 is_collinear)& not a2,a1,a4 is_collinear by A1,Th37;
  hence thesis by A2,Th22;
end;

theorem Th39:
  parallelogram a,b,c,d implies not a,b,x is_collinear or not c,d,
  x is_collinear
proof
  assume
A1: parallelogram a,b,c,d;
  then
A2: c <>d by Th36;
  ( not a,b,c is_collinear)& a,b // c,d by A1,Def3;
  hence thesis by A2,Th28;
end;

theorem
  parallelogram a,b,c,d implies parallelogram a,c,b,d
proof
  assume
A1: parallelogram a,b,c,d;
  then
A2: a,c // b,d by Def3;
  ( not a,c,b is_collinear)& a,b // c,d by A1,Def3,Th38;
  hence thesis by A2,Def3;
end;

theorem
  parallelogram a,b,c,d implies parallelogram c,d,a,b
proof
  assume
A1: parallelogram a,b,c,d;
  then a,b // c,d by Def3;
  then
A2: c,d // a,b by Th6;
  a,c // b,d by A1,Def3;
  then
A3: c,a // d,b by Th6;
  not c,d,a is_collinear by A1,Th38;
  hence thesis by A2,A3,Def3;
end;

theorem
  parallelogram a,b,c,d implies parallelogram b,a,d,c
proof
  assume
A1: parallelogram a,b,c,d;
  then a,b // c,d by Def3;
  then
A2: b,a // d,c by Th6;
  a,c // b,d by A1,Def3;
  then
A3: b,d // a,c by Th6;
  not b,a,d is_collinear by A1,Th38;
  hence thesis by A2,A3,Def3;
end;

theorem Th43:
  parallelogram a,b,c,d implies parallelogram a,c,b,d &
  parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b &
  parallelogram d,b,c,a & parallelogram b,d,a,c
proof
  assume
A1: parallelogram a,b,c,d;
  then
A2: ( not c,d,a is_collinear)& not b,a,d is_collinear by Th38;
A3: ( not a,c,b is_collinear)& a,c // b,d by A1,Def3,Th38;
A4: ( not c,a,d is_collinear)& not d,b,c is_collinear by A1,Th38;
A5: a,b // c,d by A1,Def3;
  then
A6: d,c // b,a by Th6;
A7: a,c // b,d by A1,Def3;
  then
A8: c,a // d,b & b,d // a,c by Th6;
A9: not b,d,a is_collinear by A1,Th38;
A10: d,b // c,a by A7,Th6;
  c,d // a,b & b,a // d,c by A5,Th6;
  hence thesis by A5,A3,A2,A8,A4,A10,A6,A9,Def3;
end;

theorem Th44:
  not a,b,c is_collinear implies ex d st parallelogram a,b,c,d
proof
  assume
A1: not a,b,c is_collinear;
  consider d such that
A2: a,b // c,d & a,c // b,d by Def1;
  take d;
  thus thesis by A1,A2,Def3;
end;

theorem Th45:
  parallelogram a,b,c,d1 & parallelogram a,b,c,d2 implies d1=d2
proof
  assume that
A1: parallelogram a,b,c,d1 and
A2: parallelogram a,b,c,d2;
  not b,c,a is_collinear by A1,Th38;
  then
A3: not b,c // b,a by Def2;
  a,c // b,d2 by A2,Def3;
  then
A4: c,a // b,d2 by Th6;
  a,b // c,d2 by A2,Def3;
  then
A5: b,a // c,d2 by Th6;
  a,c // b,d1 by A1,Def3;
  then
A6: c,a // b,d1 by Th6;
  a,b // c,d1 by A1,Def3;
  then
A7: b,a // c,d1 by Th6;
  b,c // c,b by Def1;
  hence thesis by A3,A7,A5,A6,A4,Th19;
end;

theorem Th46:
  parallelogram a,b,c,d implies not a,d // b,c
proof
  assume
A1: parallelogram a,b,c,d;
  then not a,b,c is_collinear by Def3;
  then
A2: not a,b // a,c by Def2;
  a,b // c,d & a,c // b,d by A1,Def3;
  hence thesis by A2,Def1;
end;

theorem Th47:
  parallelogram a,b,c,d implies not parallelogram a,b,d,c
proof
  assume
A1: parallelogram a,b,c,d;
  then not a,b,c is_collinear by Def3;
  then
A2: not a,b // a,c by Def2;
  assume not thesis;
  then
A3: a,d // b,c by Def3;
  a,b // c,d & a,c // b,d by A1,Def3;
  hence contradiction by A3,A2,Def1;
end;

theorem Th48:
  a<>b implies ex c st a,b,c is_collinear & c <>a & c <>b
proof
  assume a<>b;
  then consider p such that
A1: not a,b,p is_collinear by Th25;
  consider q such that
A2: parallelogram a,b,p,q by A1,Th44;
  not p,q,b is_collinear by A2,Th38;
  then consider c such that
A3: parallelogram p,q,b,c by Th44;
  take c;
A4: p,q // b,c by A3,Def3;
  p<>q & a,b // p,q by A2,Def3,Th36;
  then a,b // b,c by A4,Th8;
  then b,a // b,c by Th6;
  then
A5: b,a,c is_collinear by Def2;
A6: not a,q // b,p by A2,Th46;
  p,b // q,c & not b,c,p is_collinear by A3,Def3,Th37;
  hence thesis by A6,A5,Th6,Th22,Th24;
end;

theorem Th49:
  parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 implies b,c // b9,c9
proof
  assume that
A1: parallelogram a,a9,b,b9 and
A2: parallelogram a,a9,c,c9;
A3: a,a9 // c,c9 & a,c // a9,c9 by A2,Def3;
  not a,a9,c is_collinear by A2,Def3;
  then
A4: not a,a9 // a,c by Def2;
  not a,a9,b is_collinear by A1,Def3;
  then
A5: not a,a9 // a,b by Def2;
  a,a9 // b,b9 & a,b // a9,b9 by A1,Def3;
  hence thesis by A5,A4,A3,Def1;
end;

theorem Th50:
  not b,b9,c is_collinear & parallelogram a,a9,b,b9 &
  parallelogram a,a9,c,c9 implies parallelogram b,b9,c,c9
proof
  assume that
A1: not b,b9,c is_collinear and
A2: parallelogram a,a9,b,b9 and
A3: parallelogram a,a9,c,c9;
A4: a,a9 // c,c9 by A3,Def3;
  a<>a9 & a,a9 // b,b9 by A2,Def3,Th36;
  then
A5: b,b9 // c,c9 by A4,Def1;
  b,c // b9,c9 by A2,A3,Th49;
  hence thesis by A1,A5,Def3;
end;

theorem Th51:
  a,b,c is_collinear & b<>c & parallelogram a,a9,b,b9 &
  parallelogram a,a9,c,c9 implies parallelogram b,b9,c,c9
proof
  assume that
A1: a,b,c is_collinear and
A2: b<>c and
A3: parallelogram a,a9,b,b9 and
A4: parallelogram a,a9,c,c9;
A5: b<>b9 by A3,Th36;
  a,b // a,c by A1,Def2;
  then
A6: a,b // b,c by Th7;
  ( not a,a9,b is_collinear)& a,a9 // b,b9 by A3,Def3;
  hence thesis by A2,A3,A4,A6,A5,Th23,Th50;
end;

theorem Th52:
  parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 &
  parallelogram b,b9,d,d9 implies c,d // c9,d9
proof
  assume that
A1: parallelogram a,a9,b,b9 and
A2: parallelogram a,a9,c,c9 and
A3: parallelogram b,b9,d,d9;
A4: now
    assume
A5: not a,a9,d is_collinear;
    parallelogram b,b9,a,a9 by A1,Th43;
    then parallelogram a,a9,d,d9 by A3,A5,Th50;
    hence thesis by A2,Th49;
  end;
A6: now
A7: ( not a,a9,b is_collinear)& a,a9 // a,a9 by A1,Th1,Th38;
A8: a<>a9 by A1,Th36;
    assume that
A9: b,b9,c is_collinear and
A10: a,a9,d is_collinear;
    a<>b by A1,Th36;
    then consider x such that
A11: a,b,x is_collinear and
A12: x<>a and
A13: x<>b by Th48;
    a,b // a,x by A11,Def2;
    then consider y such that
A14: parallelogram a,a9,x,y by A12,A7,A8,Th23,Th44;
A15: not x,y,d is_collinear by A10,A14,Th39;
    parallelogram b,b9,x,y by A1,A11,A13,A14,Th51;
    then
A16: parallelogram x,y,d,d9 by A3,A15,Th50;
    not x,y,c is_collinear by A1,A9,A11,A13,A14,Th39,Th51;
    then parallelogram x,y,c,c9 by A2,A14,Th50;
    hence thesis by A16,Th49;
  end;
  now
    assume not b,b9,c is_collinear;
    then parallelogram b,b9,c,c9 by A1,A2,Th50;
    hence thesis by A3,Th49;
  end;
  hence thesis by A4,A6;
end;

Lm1: a<>b implies ex c,d st parallelogram a,b,c,d
proof
  assume a<>b;
  then consider c such that
A1: not a,b,c is_collinear by Th25;
  ex d st parallelogram a,b,c,d by A1,Th44;
  hence thesis;
end;

theorem
  a<>d implies ex b,c st parallelogram a,b,c,d
proof
  assume a<>d;
  then consider b such that
A1: not a,d,b is_collinear by Th25;
  not b,a,d is_collinear by A1,Th22;
  then consider c such that
A2: parallelogram b,a,d,c by Th44;
  parallelogram a,b,c,d by A2,Th43;
  hence thesis;
end;

::
::                                 CONGRUENCE
::

definition
  let SAS,a,b,r,s;
  pred congr a,b,r,s means
  :Def4:
  a=b & r =s or ex p,q st parallelogram p,q,a, b & parallelogram p,q,r,s;
end;

theorem Th54:
  congr a,a,b,c implies b=c
proof
  assume congr a,a,b,c;
  then
  a=a & b=c or ex p,q st parallelogram p,q,a,a & parallelogram p,q,b,c by Def4;
  hence thesis by Th36;
end;

theorem Th55:
  congr a,b,c,c implies a=b
proof
  assume congr a,b,c,c;
  then
  a=b & c =c or ex p,q st parallelogram p,q,a,b & parallelogram p,q,c,c by Def4
;
  hence thesis by Th36;
end;

theorem Th56:
  congr a,b,b,a implies a=b
proof
  assume
A1: congr a,b,b,a;
  now
    assume a<>b;
    then ex p,q st parallelogram p,q,a,b & parallelogram p,q,b,a by A1,Def4;
    hence contradiction by Th47;
  end;
  hence thesis;
end;

theorem Th57:
  congr a,b,c,d implies a,b // c,d
proof
  assume
A1: congr a,b,c,d;
  now
    assume a<>b;
    then consider p,q such that
A2: parallelogram p,q,a,b and
A3: parallelogram p, q,c,d by A1,Def4;
A4: p,q // c,d by A3,Def3;
    p<>q & p,q // a,b by A2,Def3,Th36;
    hence thesis by A4,Def1;
  end;
  hence thesis by Th3;
end;

theorem Th58:
  congr a,b,c,d implies a,c // b,d
proof
  assume
A1: congr a,b,c,d;
A2: now
    assume a<>b;
    then ex p,q st parallelogram p,q,a,b & parallelogram p,q,c,d by A1,Def4;
    hence thesis by Th49;
  end;
  now
    assume
A3: a=b;
    then c =d by A1,Th54;
    hence thesis by A3,Th1;
  end;
  hence thesis by A2;
end;

theorem Th59:
  congr a,b,c,d & not a,b,c is_collinear implies parallelogram a,b ,c,d
proof
  assume that
A1: congr a,b,c,d and
A2: not a,b,c is_collinear;
  a,b // c,d & a,c // b,d by A1,Th57,Th58;
  hence thesis by A2,Def3;
end;

theorem Th60:
  parallelogram a,b,c,d implies congr a,b,c,d
proof
A1: a,b // a,b by Th1;
  assume
A2: parallelogram a,b,c,d;
  then
A3: ( not a,c,b is_collinear)& a<>b by Th36,Th38;
  a<>c by A2,Th36;
  then consider p such that
A4: a,c,p is_collinear and
A5: a<>p and
A6: c <>p by Th48;
  a,c // a,p by A4,Def2;
  then consider q such that
A7: parallelogram a,p,b,q by A5,A1,A3,Th23,Th44;
  parallelogram a,b,p,q by A7,Th43;
  then parallelogram c,d,p,q by A2,A4,A6,Th51;
  then
A8: parallelogram p,q,c,d by Th43;
  parallelogram p,q,a,b by A7,Th43;
  hence thesis by A8,Def4;
end;

theorem Th61:
  congr a,b,c,d & a,b,c is_collinear & parallelogram r,s,a,b
  implies parallelogram r,s,c,d
proof
  assume that
A1: congr a,b,c,d and
A2: a,b,c is_collinear and
A3: parallelogram r,s,a,b;
  now
A4: parallelogram a,b,r,s by A3,Th43;
    assume
A5: a<>b;
    then consider p,q such that
A6: parallelogram p,q,a,b and
A7: parallelogram p, q,c,d by A1,Def4;
    parallelogram a,b,p,q by A6,Th43;
    then
A8: r,c // s,d by A7,A4,Th52;
    r,s // a,b & a,b // c,d by A1,A3,Def3,Th57;
    then
A9: r,s // c,d by A5,Th8;
    not r,s,c is_collinear by A2,A3,Th39;
    hence thesis by A9,A8,Def3;
  end;
  hence thesis by A3,Th36;
end;

theorem Th62:
  congr a,b,c,x & congr a,b,c,y implies x=y
proof
  assume that
A1: congr a,b,c,x and
A2: congr a,b,c,y;
A3: now
    assume that
    a<>b and
A4: not a,b,c is_collinear;
    parallelogram a,b,c,x & parallelogram a,b,c,y by A1,A2,A4,Th59;
    hence thesis by Th45;
  end;
A5: now
    assume that
A6: a<>b and
A7: a,b,c is_collinear;
    consider p,q such that
A8: parallelogram a,b,p,q by A6,Lm1;
    parallelogram p,q,a,b by A8,Th43;
    then parallelogram p,q,c,x & parallelogram p,q,c,y by A1,A2,A7,Th61;
    hence thesis by Th45;
  end;
  now
    assume
A9: a=b;
    then c =x by A1,Th54;
    hence thesis by A2,A9,Th54;
  end;
  hence thesis by A5,A3;
end;

theorem Th63:
  ex d st congr a,b,c,d
proof
A1: now
    assume a=b;
    then congr a,b,c,c by Def4;
    hence thesis;
  end;
A2: now
    assume that
A3: a<>b and
A4: a,b,c is_collinear;
    consider p,q such that
A5: parallelogram a,b,p,q by A3,Lm1;
    not p,q,c is_collinear by A4,A5,Th39;
    then consider d such that
A6: parallelogram p,q,c,d by Th44;
    parallelogram p,q,a,b by A5,Th43;
    then congr a,b,c,d by A6,Def4;
    hence thesis;
  end;
  now
    assume that
    a<>b and
A7: not a,b,c is_collinear;
    ex d st parallelogram a,b,c,d by A7,Th44;
    hence thesis by Th60;
  end;
  hence thesis by A1,A2;
end;

theorem Th64:
  congr a,b,a,b
proof
  now
    assume a<>b;
    then consider p,q such that
A1: parallelogram a,b,p,q by Lm1;
    parallelogram p,q,a,b by A1,Th43;
    hence thesis by Def4;
  end;
  hence thesis by Def4;
end;

theorem Th65:
  congr r,s,a,b & congr r,s,c,d implies congr a,b,c,d
proof
  assume that
A1: congr r,s,a,b and
A2: congr r,s,c,d;
A3: now
    assume that
    r<>s and
A4: ( not r,s,a is_collinear)& not r,s,c is_collinear;
    parallelogram r,s,a,b & parallelogram r,s,c,d by A1,A2,A4,Th59;
    hence thesis by Def4;
  end;
A5: now
    assume that
A6: r<>s and
A7: r,s,c is_collinear;
    consider p,q such that
A8: parallelogram p,q,r,s and
A9: parallelogram p, q,a,b by A1,A6,Def4;
    parallelogram p,q,c,d by A2,A7,A8,Th61;
    hence thesis by A9,Def4;
  end;
A10: now
    assume that
A11: r<>s and
A12: r,s,a is_collinear;
    consider p,q such that
A13: parallelogram p,q,r,s and
A14: parallelogram p,q,c,d by A2,A11,Def4;
    parallelogram p,q,a,b by A1,A12,A13,Th61;
    hence thesis by A14,Def4;
  end;
  now
    assume r=s;
    then a=b & c =d by A1,A2,Th54;
    hence thesis by Def4;
  end;
  hence thesis by A10,A5,A3;
end;

theorem Th66:
  congr a,b,c,d implies congr c,d,a,b
proof
  assume
A1: congr a,b,c,d;
  congr a,b,a,b by Th64;
  hence thesis by A1,Th65;
end;

theorem Th67:
  congr a,b,c,d implies congr b,a,d,c
proof
  assume
A1: congr a,b,c,d;
A2: now
    assume a<>b;
    then consider p,q such that
A3: parallelogram p,q,a,b & parallelogram p, q,c,d by A1,Def4;
    parallelogram q,p,b,a & parallelogram q,p,d,c by A3,Th43;
    hence thesis by Def4;
  end;
  now
    assume
A4: a=b;
    then c =d by A1,Th54;
    hence thesis by A4,Def4;
  end;
  hence thesis by A2;
end;

theorem Th68:
  congr a,b,c,d implies congr a,c,b,d
proof
  assume
A1: congr a,b,c,d;
A2: now
    assume
A3: a=c;
    congr a,b,a,b by Th64;
    then b=d by A1,A3,Th62;
    hence thesis by A3,Def4;
  end;
A4: now
    assume that
A5: a<>b and
A6: a<>c and
A7: a,b,c is_collinear;
A8: a,b // a,c by A7,Def2;
    consider p,q such that
A9: parallelogram p,q,a,b and
A10: parallelogram p, q,c,d by A1,A5,Def4;
A11: a,p // a,p by Th1;
    ( not a,b,p is_collinear)& a<>p by A9,Th36,Th38;
    then consider r such that
A12: parallelogram a,c,p,r by A6,A8,A11,Th23,Th44;
A13: a,c // p,r by A12,Def3;
A14: p,q // c,d by A10,Def3;
    p<>q & p,q // a,b by A9,Def3,Th36;
    then
A15: a,b // c,d by A14,Def1;
    then a,c // b,d by A5,A7,Th32;
    then
A16: p,r // b,d by A6,A13,Def1;
    parallelogram p,r,a,c by A12,Th43;
    then
A17: p,a // r,c by Def3;
    p,a // q,b & p<>a by A9,Def3,Th36;
    then
A18: r,c // q,b by A17,Def1;
    p,c // q,d by A10,Def3;
    then
A19: q,d // p,c by Th6;
    p,q // a,b by A9,Def3;
    then
A20: a,b // p,q by Th6;
A21: a,c // p,r by A12,Def3;
    a,b // a,c by A7,Def2;
    then a,c // p,q by A5,A20,Def1;
    then p,q // p,r by A6,A21,Def1;
    then
A22: r,q // r,p by Th7;
    a,c,b is_collinear by A7,Th22;
    then
A23: not p,r,b is_collinear by A12,Th39;
A24: parallelogram p,r,a,c by A12,Th43;
    c,b // c,d by A5,A7,A15,Th33;
    then b,c // b,d by Th7;
    then p,b // r,d by A22,A18,A19,Def1;
    then parallelogram p,r,b,d by A23,A16,Def3;
    hence thesis by A24,Def4;
  end;
A25: now
    assume that
    a<>b and
    a<>c and
A26: not a,b,c is_collinear;
    parallelogram a,b,c,d by A1,A26,Th59;
    then parallelogram a,c,b,d by Th43;
    hence thesis by Th60;
  end;
  now
    assume
A27: a=b;
    then c =d by A1,Th54;
    hence thesis by A27,Th64;
  end;
  hence thesis by A2,A4,A25;
end;

theorem Th69:
  congr a,b,c,d implies congr c,d,a,b & congr b,a,d,c & congr a,c,
  b,d & congr d,c,b,a & congr b,d,a,c & congr c,a,d,b & congr d,b,c,a
proof
  assume
A1: congr a,b,c,d;
  then congr c,d,a,b by Th66;
  then
A2: congr d,c,b,a by Th67;
  congr b,a,d,c & congr a,c,b,d by A1,Th67,Th68;
  hence thesis by A2,Th67,Th68;
end;

theorem Th70:
  congr a,b,p,q & congr b,c,q,s implies congr a,c,p,s
proof
  assume congr a,b,p,q & congr b,c,q,s;
  then congr b,q,a,p & congr b,q,c,s by Th69;
  then congr a,p,c,s by Th65;
  hence thesis by Th68;
end;

theorem Th71:
  congr b,a,p,q & congr c,a,p,r implies congr b,c,r,q
proof
  assume that
A1: congr b,a,p,q and
A2: congr c,a,p,r;
A3: congr r,p,a,c by A2,Th69;
  consider s such that
A4: congr p,q,r,s by Th63;
  congr r,p,s,q by A4,Th69;
  then
A5: congr a,c,s,q by A3,Th65;
  congr p,q,b,a by A1,Th69;
  then congr b,a,r,s by A4,Th65;
  hence thesis by A5,Th70;
end;

theorem
  congr a,o,o,p & congr b,o,o,q implies congr a,b,q,p by Th71;

theorem Th73:
  congr b,a,p,q & congr c,a,p,r implies b,c // q,r
proof
  assume congr b,a,p,q & congr c,a,p,r;
  then b,c // r,q by Th57,Th71;
  hence thesis by Th6;
end;

theorem
  congr a,o,o,p & congr b,o,o,q implies a,b // p,q by Th73;

::
::                          A VECTOR' GROUP
::

definition
  let SAS,a,b,o;
  func sum(a,b,o) -> Element of SAS means
  :Def5:
  congr o,a,b,it;
  correctness by Th62,Th63;
end;

definition
  let SAS,a,o;
  func opposite(a,o) -> Element of SAS means
  :Def6:
  sum(a,it,o) = o;
  existence
  proof
    consider b being Element of SAS such that
A1: congr a,o,o,b by Th63;
    take b;
    congr o,a,b,o by A1,Th67;
    hence thesis by Def5;
  end;
  uniqueness
  proof
    let b1,b2 be Element of SAS such that
A2: sum(a,b1,o) = o and
A3: sum(a,b2,o) = o;
    congr o,a,b2,o by A3,Def5;
    then
A4: congr a,o,o,b2 by Th67;
    congr o,a,b1,o by A2,Def5;
    then congr a,o,o,b1 by Th67;
    hence thesis by A4,Th62;
  end;
end;

definition
  let SAS,a,b,o;
  func diff(a,b,o) -> Element of SAS equals
  sum(a,opposite(b,o),o);
  correctness;
end;

theorem Th75:
  sum(a,o,o)=a
proof
  congr o,a,o,a by Th64;
  hence thesis by Def5;
end;

theorem
  ex x st sum(a,x,o)=o
proof
  consider x such that
A1: congr a,o,o,x by Th63;
A2: congr o,a,x,sum(a,x,o) by Def5;
  congr o,a,x,o by A1,Th69;
  hence thesis by A2,Th62;
end;

theorem
  sum(sum(a,b,o),c,o)=sum(a,sum(b,c,o),o)
proof
  congr o,a,b,sum(a,b,o) & congr o,a,sum(b,c,o),sum(a,sum(b,c,o),o) by Def5;
  then
A1: congr b,sum(a,b,o),sum(b,c,o),sum(a,sum(b,c,o),o) by Th65;
  congr o,b,c,sum(b,c,o) by Def5;
  then
A2: congr b,o,sum(b,c,o) ,c by Th69;
  congr o,sum(a,b,o),c,sum(sum(a,b,o),c,o) by Def5;
  then congr b,sum(a,b,o),sum(b,c,o),sum(sum(a,b,o),c,o) by A2,Th70;
  hence thesis by A1,Th62;
end;

theorem Th78:
  sum(a,b,o)=sum(b,a,o)
proof
  congr o,b,a,sum(b,a,o) by Def5;
  then congr o,a,b,sum(b,a,o) by Th69;
  hence thesis by Def5;
end;

theorem
  sum(a,a,o)=o implies a=o
proof
  assume sum(a,a,o)=o;
  then congr o,a,a,o by Def5;
  hence thesis by Th56;
end;

theorem
  sum(a,x,o)=sum(a,y,o) implies x=y
proof
  assume
A1: sum(a,x,o)=sum(a,y,o);
  congr o,a,x,sum(a,x,o) by Def5;
  then
A2: congr a,o,sum(a,x,o),x by Th69;
  congr o,a,y,sum(a,y,o) by Def5;
  then congr a,o,sum(a,x,o),y by A1,Th69;
  hence thesis by A2,Th62;
end;

theorem Th81:
  congr a,o,o,opposite(a,o)
proof
  sum(a,opposite(a,o),o)=o & congr o,a,opposite(a,o),sum(a,opposite(a,o),o
  ) by Def5,Def6;
  hence thesis by Th69;
end;

theorem Th82:
  opposite(a,o)=opposite(b,o) implies a=b
proof
  assume
A1: opposite(a,o)=opposite(b,o);
  congr a,o,o,opposite(a,o) by Th81;
  then
A2: congr opposite(a,o),o,o,a by Th69;
  congr b,o,o,opposite(b,o) by Th81;
  then congr opposite(a,o),o,o,b by A1,Th69;
  hence thesis by A2,Th62;
end;

theorem
  a,b // opposite(a,o),opposite(b,o)
proof
  sum(b,opposite(b,o),o)=o by Def6;
  then congr o,b,opposite(b,o),o by Def5;
  then
A1: congr b,o,o,opposite(b,o) by Th69;
  sum(a,opposite(a,o),o)=o by Def6;
  then congr o,a,opposite(a,o),o by Def5;
  then congr a,o,o,opposite(a,o) by Th69;
  hence thesis by A1,Th73;
end;

theorem
  opposite(o,o)=o
proof
  sum(o,opposite(o,o),o)=o by Def6;
  then sum(opposite(o,o),o,o)=o by Th78;
  hence thesis by Th75;
end;

theorem Th85:
  p,q // sum(p,r,o),sum(q,r,o)
proof
  congr o,p,r,sum(p,r,o) by Def5;
  then
A1: congr p,o,sum(p,r,o),r by Th69;
  congr o,q,r,sum(q,r,o) by Def5;
  hence thesis by A1,Th57,Th70;
end;

theorem
  p,q // r,s implies p,q // sum(p,r,o),sum(q,s,o)
proof
  assume
A1: p,q // r,s;
  now
    consider t such that
A2: congr o,q,r,t by Th63;
    assume that
A3: p<>q and
A4: r<>s;
    congr o,q,s,sum(q,s,o) by Def5;
    then congr r,t,s,sum(q,s,o) by A2,Th65;
    then
A5: congr r,s,t,sum(q,s,o) by Th69;
    then
A6: t<>sum(q,s,o) by A4,Th55;
    r,s // t,sum(q,s,o) by A5,Th57;
    then
A7: p,q // t,sum(q,s,o) by A1,A4,Th8;
    congr o,p,r,sum(p,r,o) by Def5;
    then congr p,o,sum(p,r,o),r by Th69;
    then p,q // sum(p,r,o),t by A2,Th57,Th70;
    then p,q // t,sum(p,r,o) by Th6;
    then t,sum(q,s,o) // t,sum(p,r,o) by A3,A7,Def1;
    then t,sum(q,s,o) // sum(p,r,o),sum(q,s,o) by Th7;
    hence thesis by A6,A7,Th8;
  end;
  hence thesis by Th3,Th85;
end;

theorem Th87:
  diff(a,b,o)=o iff a=b
proof
  diff(a,b,o)=o implies a=b
  proof
    assume diff(a,b,o)=o;
    then opposite(a,o)= opposite(b,o) by Def6;
    hence thesis by Th82;
  end;
  hence thesis by Def6;
end;

theorem Th88:
  o,diff(b,a,o) // a,b
proof
  congr a,o,o,opposite(a,o) by Th81;
  then
A1: congr o,opposite(a,o),a,o by Th69;
  congr o,b,opposite(a,o),sum(b,opposite(a,o),o) by Def5;
  then congr o,opposite(a,o),b,diff(b,a,o) by Th69;
  then congr a,o,b,diff(b,a,o) by A1,Th65;
  then congr o,diff(b,a,o),a,b by Th69;
  hence thesis by Th57;
end;

theorem
  o,diff(b,a,o),diff(d,c,o) is_collinear iff a,b // c,d
proof
A1: a,b // c,d implies o,diff(b,a,o),diff(d,c,o) is_collinear
  proof
    assume
A2: a,b // c,d;
A3: now
      o,diff(d,c,o) // c,d by Th88;
      then
A4:   c,d // o,diff(d,c,o) by Th6;
      assume that
A5:   a<>b and
A6:   c <>d;
      o,diff(b,a,o) // a,b by Th88;
      then a,b // o,diff(b,a,o) by Th6;
      then o,diff(b,a,o) // c,d by A2,A5,Def1;
      then o,diff(b,a,o) // o,diff(d,c,o) by A6,A4,Th8;
      hence thesis by Def2;
    end;
    now
      assume a=b or c =d;
      then o=diff(b,a,o) or o=diff(d,c,o) by Th87;
      then o,diff(b,a,o) // o,diff(d,c,o) by Def1,Th3;
      hence thesis by Def2;
    end;
    hence thesis by A3;
  end;
  o,diff(b,a,o),diff(d,c,o) is_collinear implies a,b // c,d
  proof
    assume
A7: o,diff(b,a,o),diff(d,c,o) is_collinear;
A8: now
A9:   o,diff(d,c,o) // c,d by Th88;
      assume that
A10:  o<>diff(b,a,o) and
A11:  o<>diff(d,c,o);
      o,diff(b,a,o) // o,diff(d,c,o) & o,diff(b,a,o) // a,b by A7,Def2,Th88;
      then o,diff(d,c,o) // a,b by A10,Def1;
      hence thesis by A11,A9,Def1;
    end;
    now
      assume o=diff(b,a,o) or o=diff(d,c,o);
      then a=b or c =d by Th87;
      hence thesis by Def1,Th3;
    end;
    hence thesis by A8;
  end;
  hence thesis by A1;
end;

::
::                       A TRAPEZIUM RELATION
::

definition
  let SAS,a,b,c,d,o;
  pred trap a,b,c,d,o means
  :Def8:
  not o,a,c is_collinear & o,a,b is_collinear
  & o,c,d is_collinear & a,c // b,d;
end;

definition
  let SAS,o,p;
  pred qtrap o,p means
  :Def9:
  for b,c holds ex d st ( o,p,b is_collinear
  implies o,c,d is_collinear & p,c // b,d);
end;

theorem Th90:
  trap a,b,c,d,o implies o<>a & a<>c & c <>o
proof
  assume trap a,b,c,d,o;
  then not o,a,c is_collinear by Def8;
  hence thesis by Th24;
end;

theorem
  trap a,b,c,x,o & trap a,b,c,y,o implies x=y
proof
  assume that
A1: trap a,b,c,x,o and
A2: trap a,b,c,y,o;
A3: a,c // b,x & a,c // b,y by A1,A2,Def8;
A4: ( not o,a,c is_collinear)& o,a,b is_collinear by A1,Def8;
  o,c,x is_collinear & o,c,y is_collinear by A1,A2,Def8;
  hence thesis by A4,A3,Th34;
end;

theorem
  not o,a,b is_collinear implies trap a,o,b,o,o
proof
  assume
A1: not o,a,b is_collinear;
A2: a,b // o,o by Def1;
  o,a,o is_collinear & o,b,o is_collinear by Th24;
  hence thesis by A1,A2,Def8;
end;

theorem Th93:
  trap a,b,c,d,o implies trap c,d,a,b,o
proof
  assume
A1: trap a,b,c,d,o;
  then not o,a,c is_collinear by Def8;
  then
A2: not o,c,a is_collinear by Th22;
  a,c // b,d by A1,Def8;
  then
A3: c,a // d,b by Th6;
  o,a,b is_collinear & o,c,d is_collinear by A1,Def8;
  hence thesis by A2,A3,Def8;
end;

theorem Th94:
  trap a,b,c,d,d implies d=b
proof
  assume
A1: trap a,b,c,d,d;
  then a,c // b,d by Def8;
  then
A2: d,b // a,c by Th6;
  d,a,b is_collinear by A1,Def8;
  then d,a // d,b by Def2;
  then
A3: d,b // a,d by Th6;
  assume not thesis;
  then a,d // a,c by A3,A2,Def1;
  then
A4: d,a // d,c by Th7;
  not d,a,c is_collinear by A1,Def8;
  hence contradiction by A4,Def2;
end;

theorem Th95:
  o<>b & trap a,b,c,d,o implies not o,b,d is_collinear
proof
  assume that
A1: o<>b and
A2: trap a,b,c,d,o;
  o,a,b is_collinear by A2,Def8;
  then
A3: o,a // o,b by Def2;
  o,c,d is_collinear by A2,Def8;
  then
A4: o,c // o,d by Def2;
  o<>d & not o,a,c is_collinear by A1,A2,Def8,Th94;
  hence thesis by A1,A3,A4,Th23;
end;

theorem
  o<>b & trap a,b,c,d,o implies trap b,a,d,c,o
proof
  assume that
A1: o<>b and
A2: trap a,b,c,d,o;
  o,a,b is_collinear by A2,Def8;
  then
A3: o,b,a is_collinear by Th22;
  a,c // b,d by A2,Def8;
  then
A4: b,d // a,c by Th6;
  o,c,d is_collinear by A2,Def8;
  then
A5: o,d,c is_collinear by Th22;
  not o,b,d is_collinear by A1,A2,Th95;
  hence thesis by A3,A5,A4,Def8;
end;

theorem
  trap a,b,c,d,b implies b=d by Th93,Th94;

theorem Th98:
  trap a,p,b,q,o & trap a,p,c,r,o implies b,c // q,r
proof
  assume that
A1: trap a,p,b,q,o and
A2: trap a,p,c,r,o;
  not o,a,b is_collinear by A1,Def8;
  then
A3: not o,a // o,b by Def2;
  o,c,r is_collinear by A2,Def8;
  then
A4: o,c //o,r by Def2;
  not o,a,c is_collinear by A2,Def8;
  then
A5: not o,a //o,c by Def2;
  o,b,q is_collinear by A1,Def8;
  then
A6: o,b //o,q by Def2;
  o,a,p is_collinear by A1,Def8;
  then
A7: o,a //o,p by Def2;
  a,b // p,q & a,c // p,r by A1,A2,Def8;
  hence thesis by A3,A7,A6,A5,A4,Def1;
end;

theorem Th99:
  trap a,p,b,q,o & trap a,p,c,r,o & not o,b,c is_collinear
  implies trap b,q,c,r,o
proof
  assume that
A1: trap a,p,b,q,o & trap a,p,c,r,o and
A2: not o,b,c is_collinear;
A3: b,c // q,r by A1,Th98;
  o,b,q is_collinear & o,c,r is_collinear by A1,Def8;
  hence thesis by A2,A3,Def8;
end;

theorem
  trap a,p,b,q,o & trap a,p,c,r,o & trap b,q,d,s,o implies c,d // r,s
proof
  assume that
A1: trap a,p,b,q,o and
A2: trap a,p,c,r,o and
A3: trap b,q,d,s,o;
A4: now
    assume
A5: not o,a,d is_collinear;
    trap b,q,a,p,o by A1,Th93;
    then trap a,p,d,s,o by A3,A5,Th99;
    hence thesis by A2,Th98;
  end;
A6: now
    not o,a,b is_collinear by A1,Def8;
    then not b,a,o is_collinear by Th22;
    then consider x such that
A7: parallelogram b,a,o,x by Th44;
    o,b,q is_collinear by A1,Def8;
    then o,b // o,q by Def2;
    then
A8: b,o // q,o by Th6;
A9: o,x // o,x by Th1;
    b,o // a,x & b<>o by A7,Def3,Th36;
    then
A10: q,o // a,x by A8,Def1;
A11: not o,x,b is_collinear by A7,Th38;
A12: o<>d by A3,Th90;
    assume that
A13: o<>p and
A14: o,b,c is_collinear and
A15: o,a,d is_collinear;
    not o,p,q is_collinear by A1,A13,Th95;
    then not q,p,o is_collinear by Th22;
    then consider y such that
A16: parallelogram q,p,o,y by Th44;
A17: not o,x,a is_collinear by A7,Th38;
A18: o<>c by A2,Th90;
    a,b // p,q by A1,Def8;
    then
A19: b,a // q,p by Th6;
A20: o,a,p is_collinear by A1,Def8;
    b,a // o,x & b<>a by A7,Def3,Th36;
    then
A21: q,p // o,x by A19,Def1;
A22: o<>x by A7,Th36;
    q<>p & q,p // o,y by A16,Def3,Th36;
    then o,x // o,y by A21,Def1;
    then
A23: o,x,y is_collinear by Def2;
    q,o // p,y & q<>o by A16,Def3,Th36;
    then
A24: a,x // p,y by A10,Def1;
    not o,a,x is_collinear by A7,Th38;
    then
A25: trap a,p,x,y,o by A23,A24,A20,Def8;
    not o,b,x is_collinear by A7,Th38;
    then
A26: trap b,q,x,y,o by A1,A25,Th99;
    o,a // o,d by A15,Def2;
    then
A27: trap x,y,d,s,o by A3,A26,A22,A12,A17,A9,Th23,Th99;
    o,b // o,c by A14,Def2;
    then trap x,y,c,r,o by A2,A25,A11,A22,A18,A9,Th23,Th99;
    hence thesis by A27,Th98;
  end;
A28: now
    assume
A29: o=p;
    then o=q by A1,Th93,Th94;
    then
A30: o=s by A3,Th93,Th94;
    o=r by A2,A29,Th93,Th94;
    hence thesis by A30,Def1;
  end;
  now
    assume not o,b,c is_collinear;
    then trap b,q,c,r,o by A1,A2,Th99;
    hence thesis by A3,Th98;
  end;
  hence thesis by A4,A28,A6;
end;

theorem Th101:
  for o,a holds ex p st o,a,p is_collinear & qtrap o,p
proof
  let o,a;
  consider p such that
A1: for b,c holds o,a // o,p & ex d st o,p // o,b implies o,c // o,d & p
  ,c // b,d by Def1;
  take p;
  now
    thus o,a,p is_collinear by A1,Def2;
    let b,c;
    consider d such that
A2: o,p // o,b implies o,c // o,d & p,c // b,d by A1;
    take d;
    assume o,p,b is_collinear;
    hence o,c,d is_collinear & p,c // b,d by A2,Def2;
  end;
  hence thesis by Def9;
end;

theorem Th102:
  ex x,y,z st x<>y & y<>z & z<>x
proof
  consider x,y,z such that
A1: not x,y // x,z by Def1;
  take x,y,z;
  thus thesis by A1,Def1,Th1,Th3;
end;

theorem Th103:
  qtrap o,p implies o<>p
proof
  ex b st o<>b
  proof
    consider x,y,z such that
A1: x<>y and
    y<>z and
    z<>x by Th102;
    o<>x or o<>y or o<>z by A1;
    hence thesis;
  end;
  then consider b such that
A2: o<>b;
  consider c such that
A3: not o,b // o,c by A2,Th13;
  assume qtrap o,p;
  then consider d such that
A4: o,p,b is_collinear implies o,c,d is_collinear & p,c // b,d by Def9;
A5: now
    assume that
A6: b<>d & not o,b // o,c and
A7: o,d // b,d and
A8: o,c // b,d;
    d,o // d,b by A7,Th6;
    hence b<>d & not o,b // o,c & b,d // o,b & b,d // o,c by A6,A8,Th6,Th7;
  end;
  assume not thesis;
  then o,o // o,b implies o,c // o,d & o,c // b,d by A4,Def2;
  then
  b=d & not o,b // o,c & o,c // o,d or b<>d & o<>c & not o,b // o,c & o,c
  // o,d & o,c // b,d by A3,Def1,Th3;
  hence contradiction by A5,Def1,Th6;
end;

theorem
  qtrap o,p implies ex q st not o,p,q is_collinear & qtrap o,q
proof
A1: o,p // o,p by Th1;
  assume
A2: qtrap o,p;
  then
A3: o<>p by Th103;
  consider r such that
A4: not o,p,r is_collinear by A2,Th25,Th103;
  consider q such that
A5: o,r,q is_collinear and
A6: qtrap o,q by Th101;
  take q;
  o<>q & o,r // o,q by A5,A6,Def2,Th103;
  hence thesis by A3,A4,A6,A1,Th23;
end;

theorem
  not o,p,c is_collinear & o,p,b is_collinear & qtrap o,p implies ex d
  st trap p,b,c,d,o
proof
  assume that
A1: ( not o,p,c is_collinear)& o,p,b is_collinear and
A2: qtrap o,p;
  consider d such that
A3: o,p,b is_collinear implies o,c,d is_collinear & p,c // b,d by A2,Def9;
  take d;
  thus thesis by A1,A3,Def8;
end;