:: Ordered Affine Spaces Defined in Terms of Directed Parallelity - part I
::  by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received May 4, 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, SUBSET_1, RELAT_1, ZFMISC_1, ANALOAF, STRUCT_0,
      PARSP_1, PARSP_2, DIRAF;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELSET_1, STRUCT_0,
      ANALOAF;
 constructors DOMAIN_1, ANALOAF;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, ANALOAF;
 requirements SUBSET, BOOLE;
 definitions ANALOAF, STRUCT_0;
 theorems ANALOAF, RELAT_1, ZFMISC_1, DOMAIN_1, STRUCT_0, XTUPLE_0;
 schemes RELSET_1;

begin

reserve x,y for set;
reserve X for non empty set;
reserve a,b,c,d for Element of X;

definition
  let X;
  let R be Relation of [:X,X:];
  func lambda(R) -> Relation of [:X,X:] means
  :Def1:
  for a,b,c,d being Element
of X holds [[a,b],[c,d]] in it iff ([[a,b],[c,d]] in R or [[a,b],[d,c]] in R);
  existence
  proof
    defpred P[set,set] means ex a,b,c,d being Element of X st $1=[a,b] & $2=[c
    ,d] & ([[a,b],[c,d]] in R or [[a,b],[d,c]] in R);
    set XX = [:X,X:];
    consider P being Relation of XX,XX such that
A1: for x,y holds [x,y] in P iff x in XX & y in XX & P[x,y] from
    RELSET_1:sch 1;
    take P;
    let a,b,c,d be Element of X;
    [[a,b],[c,d]] in P implies ([[a,b],[c,d]] in R or [[a,b],[d,c]] in R)
    proof
      assume [[a,b],[c,d]] in P;
      then consider a9,b9,c9,d9 being Element of X such that
A2:   [a,b]=[a9,b9] and
A3:   [c,d]=[c9,d9] and
A4:   [[a9,b9],[c9,d9]] in R or [[a9,b9],[d9,c9]] in R by A1;
      c = c9 by A3,XTUPLE_0:1;
      hence thesis by A2,A3,A4,XTUPLE_0:1;
    end;
    hence thesis by A1;
  end;
  uniqueness
  proof
    set XX = [:X,X:];
    let P,Q be Relation of [:X,X:] such that
A5: for a,b,c,d being Element of X holds [[a,b],[c,d]] in P iff ([[a,
    b],[c,d]] in R or [[a,b],[d,c]] in R) and
A6: for a,b,c,d being Element of X holds [[a,b],[c,d]] in Q iff ([[a,
    b],[c,d]] in R or [[a,b],[d,c]] in R);
    for x,y holds [x,y] in P iff [x,y] in Q
    proof
      let x,y;
A7:   now
        assume
A8:     [x,y] in Q;
        then y in XX by ZFMISC_1:87;
        then consider c,d such that
A9:     y=[c,d] by DOMAIN_1:1;
        x in XX by A8,ZFMISC_1:87;
        then
A10:    ex a,b st x=[a,b] by DOMAIN_1:1;
        then [x,y] in Q iff [x,y] in R or [x,[d,c]] in R by A6,A9;
        hence [x,y] in P by A5,A8,A10,A9;
      end;
      now
        assume
A11:    [x,y] in P;
        then y in XX by ZFMISC_1:87;
        then consider c,d such that
A12:    y=[c,d] by DOMAIN_1:1;
        x in XX by A11,ZFMISC_1:87;
        then
A13:    ex a,b st x=[a,b] by DOMAIN_1:1;
        then [x,y] in P iff [x,y] in R or [x,[d,c]] in R by A5,A12;
        hence [x,y] in Q by A6,A11,A13,A12;
      end;
      hence thesis by A7;
    end;
    hence thesis by RELAT_1:def 2;
  end;
end;

definition
  let S be non empty AffinStruct;
  func Lambda(S) -> strict AffinStruct equals
  AffinStruct (# the carrier of S,
    lambda(the CONGR of S) #);
  correctness;
end;

registration
  let S be non empty AffinStruct;
  cluster Lambda S -> non empty;
  coherence;
end;

reserve S for OAffinSpace;
reserve a,b,c,d,p,q,r,x,y,z,t,u,w for Element of S;

theorem Th1:
  x,y // x,y
proof
  x,y // y,y by ANALOAF:def 5;
  hence thesis by ANALOAF:def 5;
end;

Lm1: x,y // z,t implies z,t // x,y
proof
  assume
A1: x,y // z,t;
  now
    assume
A2: x<>y;
    x,y // x,y by Th1;
    hence thesis by A1,A2,ANALOAF:def 5;
  end;
  hence thesis by ANALOAF:def 5;
end;

theorem Th2:
  x,y // z,t implies y,x // t,z & z,t // x,y & t,z // y,x
proof
  assume x,y // z,t;
  hence y,x // t,z & z,t // x,y by Lm1,ANALOAF:def 5;
  hence thesis by ANALOAF:def 5;
end;

theorem Th3:
  z<>t & x,y // z,t & z,t // u,w implies x,y // u,w
proof
  assume
A1: z<>t;
  assume that
A2: x,y // z,t and
A3: z,t // u,w;
  z,t // x,y by A2,Th2;
  hence thesis by A1,A3,ANALOAF:def 5;
end;

theorem Th4:
  x,x // y,z & y,z // x,x
proof
  y,z // x,x by ANALOAF:def 5;
  hence thesis by Th2;
end;

theorem Th5:
  x,y // z,t & x,y // t,z implies x=y or z=t
proof
  assume that
A1: x,y // z,t & x,y // t,z & x<>y and
A2: z<>t;
  z,t // t,z by A1,ANALOAF:def 5;
  hence contradiction by A2,ANALOAF:def 5;
end;

theorem Th6:
  x,y // x,z iff x,y // y,z or x,z // z,y
proof
  now
    assume x,y // y,z or x,z // z,y;
    then x,y // x,z or x,z // x,y by ANALOAF:def 5;
    hence x,y // x,z by Th2;
  end;
  hence thesis by ANALOAF:def 5;
end;

definition
  let S be non empty AffinStruct;
  let a,b,c be Element of S;
  pred Mid a,b,c means
  :Def3:
  a,b // b,c;
end;

theorem Th7:
  x,y // x,z iff Mid x,y,z or Mid x,z,y
proof
  x,y // x,z iff x,y // y,z or x,z // z,y by Th6;
  hence thesis by Def3;
end;

theorem Th8:
  Mid a,b,a implies a=b
proof
  assume Mid a,b,a;
  then a,b // b,a by Def3;
  hence thesis by ANALOAF:def 5;
end;

theorem
  Mid a,b,c implies Mid c,b,a
proof
  assume Mid a,b,c;
  then a,b // b,c by Def3;
  then c,b // b,a by Th2;
  hence thesis by Def3;
end;

theorem
  Mid x,x,y & Mid x,y,y
proof
  x,x // x,y & x,y // y,y by Th4;
  hence thesis by Def3;
end;

theorem
  Mid a,b,c & Mid a,c,d implies Mid b,c,d
proof
  assume that
A1: Mid a,b,c and
A2: Mid a,c,d;
  now
A3: a,b // b,c by A1,Def3;
    then a,b // a,c by ANALOAF:def 5;
    then
A4: b,c // a,c or a=b by A3,ANALOAF:def 5;
    assume
A5: a<>c;
    a,c // c,d by A2,Def3;
    then b,c // c,d by A5,A4,Th3;
    hence thesis by Def3;
  end;
  hence thesis by A1,A2,Th8;
end;

theorem
  b<>c & Mid a,b,c & Mid b,c,d implies Mid a,c,d
proof
  assume that
A1: b<>c and
A2: Mid a,b,c and
A3: Mid b,c,d;
  now
    assume
A4: a<>b;
A5: a,b // b,c by A2,Def3;
    b,c // c,d by A3,Def3;
    then
A6: a,b // c,d by A1,A5,Th3;
    a,b // a,c by A5,ANALOAF:def 5;
    then a,c // c,d by A4,A6,ANALOAF:def 5;
    hence thesis by Def3;
  end;
  hence thesis by A3;
end;

theorem Th13:
  ex z st Mid x,y,z & y<>z
proof
  consider z such that
A1: x,y // y,z and
  x,y // y,z and
A2: y<>z by ANALOAF:def 5;
  Mid x,y,z by A1,Def3;
  hence thesis by A2;
end;

theorem
  Mid x,y,z & Mid y,x,z implies x=y
proof
  assume that
A1: Mid x,y,z and
A2: Mid y,x,z;
  x,y // y,z by A1,Def3;
  then
A3: x,y // x,z by ANALOAF:def 5;
  y,x // x,z by A2,Def3;
  then
A4: x,y // z,x by ANALOAF:def 5;
  x=z implies x=y by A1,Th8;
  hence thesis by A3,A4,Th5;
end;

theorem
  x<>y & Mid x,y,z & Mid x,y,t implies Mid y,z,t or Mid y,t,z
proof
  assume
A1: x<>y;
  assume Mid x,y,z & Mid x,y,t;
  then x,y // y,z & x,y // y,t by Def3;
  then y,z // y,t by A1,ANALOAF:def 5;
  hence thesis by Th7;
end;

theorem
  x<>y & Mid x,y,z & Mid x,y,t implies Mid x,z,t or Mid x,t,z
proof
  assume
A1: x<>y;
  assume that
A2: Mid x,y,z and
A3: Mid x,y,t;
  x,y // y,t by A3,Def3;
  then
A4: x,y // x,t by ANALOAF:def 5;
  x,y // y,z by A2,Def3;
  then x,y // x,z by ANALOAF:def 5;
  then x,z // x,t by A1,A4,ANALOAF:def 5;
  hence thesis by Th7;
end;

theorem
  Mid x,y,t & Mid x,z,t implies Mid x,y,z or Mid x,z,y
proof
  assume that
A1: Mid x,y,t and
A2: Mid x,z,t;
A3: x,z // z,t by A2,Def3;
A4: x,y // y,t by A1,Def3;
  now
    x,z // x,t by A3,ANALOAF:def 5;
    then
A5: x,t // x,z by Th2;
    assume
A6: x<>t;
    x,y // x,t by A4,ANALOAF:def 5;
    then x,y // x,z by A6,A5,Th3;
    hence thesis by Th7;
  end;
  hence thesis by A1,A2,Th8;
end;

definition
  let S be non empty AffinStruct;
  let a,b,c,d be Element of S;
  pred a,b '||' c,d means
  :Def4:
  a,b // c,d or a,b // d,c;
end;

theorem
  a,b '||' c,d iff [[a,b],[c,d]] in lambda(the CONGR of S)
proof
  thus a,b '||' c,d implies [[a,b],[c,d]] in lambda(the CONGR of S)
  proof
    assume a,b // c,d or a,b // d,c;
    then
    [[a,b],[c,d]] in the CONGR of S or [[a,b],[d,c]] in the CONGR of S by
ANALOAF:def 2;
    hence thesis by Def1;
  end;
  assume [[a,b],[c,d]] in lambda(the CONGR of S);
  then
  [[a,b],[c,d]] in the CONGR of S or [[a,b],[d,c]] in the CONGR of S by Def1;
  hence a,b // c,d or a,b // d,c by ANALOAF:def 2;
end;

theorem Th19:
  x,y '||' y,x & x,y '||' x,y
proof
  x,y // x,y by Th1;
  hence thesis by Def4;
end;

theorem Th20:
  x,y '||' z,z & z,z '||' x,y
proof
  x,y // z,z & z,z // x,y by Th4;
  hence thesis by Def4;
end;

Lm2: x<>y & x,y '||' z,t & x,y '||' u,w implies z,t '||' u,w
proof
  assume that
A1: x<>y and
A2: x,y '||' z,t and
A3: x,y '||' u,w;
A4: x,y // u,w or x,y // w,u by A3,Def4;
A5: now
    assume x,y // t,z;
    then t,z // u,w or t,z // w,u by A1,A4,ANALOAF:def 5;
    then z,t // w,u or z,t // u,w by ANALOAF:def 5;
    hence thesis by Def4;
  end;
  now
    assume x,y // z,t;
    then z,t // u,w or z,t // w,u by A1,A4,ANALOAF:def 5;
    hence thesis by Def4;
  end;
  hence thesis by A2,A5,Def4;
end;

theorem Th21:
  x,y '||' x,z implies y,x '||' y,z
proof
A1: now
    assume x,y // z,x;
    then y,x // x,z by ANALOAF:def 5;
    then y,x // y,z by ANALOAF:def 5;
    hence thesis by Def4;
  end;
A2: now
A3: now
      assume x,z // z,y;
      then y,z // z,x by Th2;
      then y,z // y,x by ANALOAF:def 5;
      then y,x // y,z by Th2;
      hence thesis by Def4;
    end;
A4: now
      assume x,y // y,z;
      then y,x // z,y by ANALOAF:def 5;
      hence thesis by Def4;
    end;
    assume x,y // x,z;
    hence thesis by A4,A3,ANALOAF:def 5;
  end;
  assume x,y '||' x,z;
  hence thesis by A2,A1,Def4;
end;

theorem Th22:
  x,y '||' z,t implies x,y '||' t,z & y,x '||' z,t & y,x '||' t,z
  & z,t '||' x,y & z,t '||' y,x & t,z '||' x,y & t,z '||' y,x
proof
  assume x,y '||' z,t;
  then
A1: x,y // z,t or x,y // t,z by Def4;
  hence x,y '||' t,z by Def4;
  y,x // t,z or y,x // z,t by A1,ANALOAF:def 5;
  hence y,x '||' z,t & y,x '||' t,z by Def4;
  z,t // x,y or z,t // y,x by A1,Th2;
  hence z,t '||' x,y & z,t '||' y,x by Def4;
  t,z // y,x or t,z // x,y by A1,Th2;
  hence thesis by Def4;
end;

theorem Th23:
  a<>b & ( a,b '||' x,y & a,b '||' z,t or a,b '||' x,y & z,t '||'
a,b or x,y '||' a,b & z,t '||' a,b or x,y '||' a,b & a,b '||' z,t ) implies x,y
  '||' z,t
proof
  assume that
A1: a<>b and
A2: a,b '||' x,y & a,b '||' z,t or a,b '||' x,y & z,t '||' a,b or x,y
  '||' a,b & z,t '||' a,b or x,y '||' a,b & a,b '||' z,t;
  a,b '||' x,y & a,b '||' z,t by A2,Th22;
  hence thesis by A1,Lm2;
end;

theorem Th24:
  ex x,y,z st not x,y '||' x,z
proof
  consider x,y,z,t such that
A1: not x,y // z,t and
A2: not x,y // t,z by ANALOAF:def 5;
A3: x<>y by A1,Th4;
  now
    assume
A4: x,y '||' x,z;
    thus not x,y '||' x,t
    proof
      assume
A5:   x,y '||' x,t;
      then x,z '||' x,t by A3,A4,Th23;
      then z,x '||' z,t by Th21;
      then x,z '||' z,t by Th22;
      then x,y '||' z,t or x=z by A4,Th23;
      hence contradiction by A1,A2,A5,Def4;
    end;
  end;
  hence thesis;
end;

theorem Th25:
  ex t st x,z '||' y,t & y<>t
proof
  consider t such that
  x,y // z,t and
A1: x,z // y,t and
A2: y<>t by ANALOAF:def 5;
  x,z '||' y,t by A1,Def4;
  hence thesis by A2;
end;

theorem Th26:
  ex t st x,y '||' z,t & x,z '||' y,t
proof
  consider t such that
A1: x,y // z,t & x,z // y,t and
  y<>t by ANALOAF:def 5;
  x,y '||' z,t & x,z '||' y,t by A1,Def4;
  hence thesis;
end;

theorem Th27:
  z,x '||' x,t & x<>z implies ex u st y,x '||' x,u & y,z '||' t,u
proof
  assume that
A1: z,x '||' x,t and
A2: x<>z;
A3: now
    consider p such that
A4: Mid z,x,p and
A5: x<>p by Th13;
A6: z,x // x,p by A4,Def3;
    then consider q such that
A7: y,x // x,q and
A8: y,z // p,q by A2,ANALOAF:def 5;
    assume
A9: z,x // t,x;
    then x,p // t,x by A2,A6,ANALOAF:def 5;
    then p,x // x,t by Th2;
    then consider r such that
A10: q,x // x,r and
A11: q,p // t,r by A5,ANALOAF:def 5;
A12: now
      assume q=p;
      then
A13:  x,p // y,x by A7,Th2;
      x,p // z,x by A6,Th2;
      then z,x // y,x by A5,A13,ANALOAF:def 5;
      then y,x // t,x by A2,A9,ANALOAF:def 5;
      then
A14:  y,x '||' x,t by Def4;
      y,z // t,t by ANALOAF:def 5;
      then y,z '||' t,t by Def4;
      hence thesis by A14;
    end;
A15: now
A16:  x,z // x,t by A9,Th2;
      assume
A17:  q=x;
      p,x // x,z by A6,Th2;
      then y,z // x,z by A5,A8,A17,Th3;
      then y,z // x,t by A2,A16,Th3;
      then
A18:  y,z '||' t,x by Def4;
      y,x // x,x by Th4;
      then y,x '||' x,x by Def4;
      hence thesis by A18;
    end;
    now
      assume that
A19:  q<>p and
A20:  q<>x;
      x,q // r,x by A10,Th2;
      then y,x // r,x by A7,A20,Th3;
      then
A21:  y,x '||' x,r by Def4;
      p,q // r,t by A11,Th2;
      then y,z // r,t by A8,A19,Th3;
      then y,z '||' t,r by Def4;
      hence thesis by A21;
    end;
    hence thesis by A12,A15;
  end;
  now
    assume z,x // x,t;
    then consider u such that
A22: y,x // x,u & y,z // t,u by A2,ANALOAF:def 5;
    y,x '||' x,u & y,z '||' t,u by A22,Def4;
    hence thesis;
  end;
  hence thesis by A1,A3,Def4;
end;

definition
  let S be non empty AffinStruct;
  let a,b,c be Element of S;
  pred LIN a,b,c means
  :Def5:
  a,b '||' a,c;
end;

notation
  let S be non empty AffinStruct;
  let a,b,c be Element of S;
  synonym a,b,c is_collinear for LIN a,b,c;
end;

theorem
  Mid a,b,c implies a,b,c is_collinear
proof
  assume Mid a,b,c;
  then a,b // b,c by Def3;
  then a,b // a,c by ANALOAF:def 5;
  then a,b '||' a,c by Def4;
  hence thesis by Def5;
end;

theorem
  a,b,c is_collinear implies Mid a,b,c or Mid b,a,c or Mid a,c,b
proof
A1: now
    assume a,b // c,a;
    then b,a // a,c by ANALOAF:def 5;
    hence Mid b,a,c by Def3;
  end;
  assume a,b,c is_collinear;
  then
A2: a,b '||' a,c by Def5;
  a,b // a,c implies ( Mid a,b,c or Mid a,c,b) by Th7;
  hence thesis by A2,A1,Def4;
end;

Lm3: x,y,z is_collinear implies x,z,y is_collinear & y,x,z is_collinear
proof
  assume x,y,z is_collinear;
  then x,y '||' x,z by Def5;
  then x,z '||' x,y & y,x '||' y,z by Th21,Th22;
  hence thesis by Def5;
end;

theorem Th30:
  x,y,z is_collinear implies x,z,y is_collinear & y,x,z
  is_collinear & y,z,x is_collinear & z,x,y is_collinear & z,y,x is_collinear
proof
  assume x,y,z is_collinear;
  hence x,z,y is_collinear & y,x,z is_collinear by Lm3;
  hence y,z,x is_collinear & z,x,y is_collinear by Lm3;
  hence thesis by Lm3;
end;

theorem Th31:
  x,x,y is_collinear & x,y,y is_collinear & x,y,x is_collinear
proof
A1: x,y '||' x,x by Th20;
  x,x '||' x,y & x,y '||' x,y by Th19,Th20;
  hence thesis by A1,Def5;
end;

theorem Th32:
  x<>y & x,y,z is_collinear & x,y,t is_collinear & x,y,u
  is_collinear implies z,t,u is_collinear
proof
  assume that
A1: x<>y and
A2: x,y,z is_collinear and
A3: x,y,t is_collinear and
A4: x,y,u is_collinear;
A5: now
A6: x,y '||' x,z by A2,Def5;
    x,y '||' x,u by A4,Def5;
    then x,z '||' x,u by A1,A6,Th23;
    then
A7: z,x '||' z,u by Th21;
    x,y '||' x,t by A3,Def5;
    then x,z '||' x,t by A1,A6,Th23;
    then
A8: z,x '||' z,t by Th21;
    assume x<>z;
    then z,t '||' z,u by A8,A7,Th23;
    hence thesis by Def5;
  end;
  now
    assume
A9: x=z;
    then z,y '||' z,t & z,y '||' z,u by A3,A4,Def5;
    then z,t '||' z,u by A1,A9,Th23;
    hence thesis by Def5;
  end;
  hence thesis by A5;
end;

theorem
  x<>y & x,y,z is_collinear & x,y '||' z,t implies x,y,t is_collinear
proof
  assume that
A1: x<>y and
A2: x,y,z is_collinear and
A3: x,y '||' z,t;
  now
    x,y '||' x,z by A2,Def5;
    then x,z '||' z,t by A1,A3,Th23;
    then z,x '||' z,t by Th22;
    then z,x,t is_collinear by Def5;
    then
A4: x,z,t is_collinear by Th30;
    assume
A5: z<>x;
    x,z,y is_collinear & x,z,x is_collinear by A2,Th30,Th31;
    hence thesis by A5,A4,Th32;
  end;
  hence thesis by A3,Def5;
end;

theorem
  x,y,z is_collinear & x,y,t is_collinear implies x,y '||' z,t
proof
  assume
A1: x,y,z is_collinear & x,y,t is_collinear;
  now
A2: x,y '||' x,z & x,y '||' x,t by A1,Def5;
    assume x<>y;
    then x,z '||' x,t by A2,Th23;
    then z,x '||' z,t by Th21;
    then x,z '||' z,t by Th22;
    hence thesis by A2,Th23;
  end;
  hence thesis by Th20;
end;

theorem
  u<>z & x,y,u is_collinear & x,y,z is_collinear & u,z,w is_collinear
  implies x,y,w is_collinear
proof
  assume that
A1: u<>z and
A2: x,y,u is_collinear & x,y,z is_collinear and
A3: u,z,w is_collinear;
  now
    assume
A4: x<>y;
    x,y,x is_collinear by Th31;
    then
A5: z,u,x is_collinear by A2,A4,Th32;
    x,y,y is_collinear by Th31;
    then
A6: z,u,y is_collinear by A2,A4,Th32;
    z,u,w is_collinear by A3,Th30;
    hence thesis by A1,A6,A5,Th32;
  end;
  hence thesis by Th31;
end;

theorem Th36:
  ex x,y,z st not x,y,z is_collinear
proof
  consider x,y,z such that
A1: not x,y '||' x,z by Th24;
  not x,y,z is_collinear by A1,Def5;
  hence thesis;
end;

theorem
  x<>y implies ex z st not x,y,z is_collinear
proof
  assume
A1: x<>y;
  consider a,b,c such that
A2: not a,b,c is_collinear by Th36;
  assume
A3: not thesis;
  then
A4: x,y,c is_collinear;
  x,y,a is_collinear & x,y,b is_collinear by A3;
  hence contradiction by A1,A2,A4,Th32;
end;

reserve AS for non empty AffinStruct;

theorem Th38:
  AS=Lambda(S) implies for a,b,c,d being Element of S, a9,b9,c9,d9
being Element of AS st a=a9 & b=b9 & c =c9 & d=d9 holds a9,b9 // c9,d9 iff a,b
  '||' c,d
proof
  assume
A1: AS=Lambda(S);
  let a,b,c,d be Element of S;
  let a9,b9,c9,d9 be Element of AS;
  assume
A2: a=a9 & b=b9 & c =c9 & d=d9;
  thus a9,b9 // c9,d9 implies a,b '||' c,d
  proof
    assume
A3: [[a9,b9],[c9,d9]] in the CONGR of AS;
    assume not [[a,b],[c,d]] in the CONGR of S;
    hence [[a,b],[d,c]] in the CONGR of S by A1,A2,A3,Def1;
  end;
  assume a,b '||' c,d;
  then a,b // c,d or a,b // d,c by Def4;
  then [[a,b],[c,d]] in the CONGR of S or [[a,b],[d,c]] in the CONGR of S by
ANALOAF:def 2;
  hence [[a9,b9],[c9,d9]] in the CONGR of AS by A1,A2,Def1;
end;

theorem Th39:
  AS = Lambda(S) implies (ex x,y being Element of AS st x<>y) & (
for x,y,z,t,u,w being Element of AS holds x,y // y,x & x,y // z,z & (x<>y & x,y
// z,t & x,y // u,w implies z,t // u,w) & (x,y // x,z implies y,x // y,z)) & (
  ex x,y,z being Element of AS st not x,y // x,z) & (for x,y,z being Element of
AS ex t being Element of AS st x,z // y,t & y<>t) & (for x,y,z being Element of
  AS ex t being Element of AS st x,y // z,t & x,z // y,t) & for x,y,z,t being
Element of AS st z,x // x,t & x<>z ex u being Element of AS st y,x // x,u & y,z
  // t,u
proof
  assume
A1: AS = Lambda(S);
  hence ex x,y being Element of AS st x<>y by STRUCT_0:def 10;
  thus for x,y,z,t,u,w being Element of AS holds x,y // y,x & x,y // z,z & (x
<>y & x,y // z,t & x,y // u,w implies z,t // u,w) & (x,y // x,z implies y,x //
  y,z)
  proof
    let x,y,z,t,u,w be Element of AS;
    reconsider x9=x, y9=y, z9=z, t9=t, u9=u, w9=w as Element of S by A1;
    x9,y9 '||' y9,x9 & x9,y9 '||' z9,z9 by Th19,Th20;
    hence x,y // y,x & x,y // z,z by A1,Th38;
    x9<>y9 & x9,y9 '||' z9,t9 & x9,y9 '||' u9,w9 implies z9,t9 '||' u9,w9
    by Lm2;
    hence x<>y & x,y // z,t & x,y // u,w implies z,t // u,w by A1,Th38;
    x9,y9 '||' x9,z9 implies y9,x9 '||' y9,z9 by Th21;
    hence thesis by A1,Th38;
  end;
  thus ex x,y,z being Element of AS st not x,y // x,z
  proof
    consider x9,y9,z9 being Element of S such that
A2: not x9,y9 '||' x9,z9 by Th24;
    reconsider x=x9, y=y9, z=z9 as Element of AS by A1;
    not x,y // x,z by A1,A2,Th38;
    hence thesis;
  end;
  thus for x,y,z being Element of AS ex t being Element of AS st x,z // y,t &
  y<>t
  proof
    let x,y,z be Element of AS;
    reconsider x9=x, y9=y, z9=z as Element of S by A1;
    consider t9 being Element of S such that
A3: x9,z9 '||' y9,t9 and
A4: y9<>t9 by Th25;
    reconsider t=t9 as Element of AS by A1;
    x,z // y,t by A1,A3,Th38;
    hence thesis by A4;
  end;
  thus for x,y,z being Element of AS ex t being Element of AS st x,y // z,t &
  x,z // y,t
  proof
    let x,y,z be Element of AS;
    reconsider x9=x, y9=y, z9=z as Element of S by A1;
    consider t9 being Element of S such that
A5: x9,y9 '||' z9,t9 & x9,z9 '||' y9,t9 by Th26;
    reconsider t=t9 as Element of AS by A1;
    x,y // z,t & x,z // y,t by A1,A5,Th38;
    hence thesis;
  end;
  thus for x,y,z,t being Element of AS st z,x // x,t & x<>z ex u being Element
  of AS st y,x // x,u & y,z // t,u
  proof
    let x,y,z,t be Element of AS such that
A6: z,x // x,t and
A7: x<>z;
    reconsider x9=x, y9=y, z9=z, t9=t as Element of S by A1;
    z9,x9 '||' x9,t9 by A1,A6,Th38;
    then consider u9 being Element of S such that
A8: y9,x9 '||' x9,u9 & y9,z9 '||' t9,u9 by A7,Th27;
    reconsider u=u9 as Element of AS by A1;
    y,x // x,u & y,z // t,u by A1,A8,Th38;
    hence thesis;
  end;
end;

definition
  let IT be non empty AffinStruct;

  attr IT is AffinSpace-like means
  :Def6:
  (for x,y,z,t,u,w being Element of IT
holds x,y // y,x & x,y // z,z & (x<>y & x,y // z,t & x,y // u,w implies z,t //
u,w) & (x,y // x,z implies y,x // y,z)) & (ex x,y,z being Element of IT st not
x,y // x,z) & (for x,y,z being Element of IT ex t being Element of IT st x,z //
y,t & y<>t) & (for x,y,z being Element of IT ex t being Element of IT st x,y //
  z,t & x,z // y,t) & for x,y,z,t being Element of IT st z,x // x,t & x<>z ex u
  being Element of IT st y,x // x,u & y,z // t,u;
end;

registration
  cluster strict AffinSpace-like for non trivial AffinStruct;
  existence
  proof
    set S = the OAffinSpace;
A1: ( for x,y,z being Element of Lambda(S) ex t being Element of Lambda(S)
st x,z // y,t & y<>t)& for x,y,z being Element of Lambda(S) ex t being Element
    of Lambda(S) st x,y // z,t & x,z // y,t by Th39;
A2: for x,y,z,t being Element of Lambda(S) st z,x // x,t & x<>z ex u being
    Element of Lambda(S) st y,x // x,u & y,z // t,u by Th39;
    ( for x,y,z,t,u,w being Element of Lambda(S) holds x,y // y,x & x,y //
    z, z & ( x<>y & x,y // z,t & x,y // u,w implies z,t // u,w) & (x,y // x,z
implies y,x // y,z))& ex x,y,z being Element of Lambda(S) st not x,y // x,z by
Th39;
    then Lambda(S) is non trivial AffinSpace-like by A1,A2,Def6;
    hence thesis;
  end;
end;

definition
  mode AffinSpace is AffinSpace-like non trivial AffinStruct;
end;

theorem
  for AS being AffinSpace holds (ex x,y being Element of AS st x<>y) & (
for x,y,z,t,u,w being Element of AS holds (x,y // y,x & x,y // z,z) & (x<>y & x
,y // z,t & x,y // u,w implies z,t // u,w) & (x,y // x,z implies y,x // y,z)) &
(ex x,y,z being Element of AS st not x,y // x,z) & (for x,y,z being Element of
AS ex t being Element of AS st x,z // y,t & y<>t) & (for x,y,z being Element of
  AS ex t being Element of AS st x,y // z,t & x,z // y,t) & for x,y,z,t being
Element of AS st z,x // x,t & x<>z ex u being Element of AS st y,x // x,u & y,z
  // t,u by Def6,STRUCT_0:def 10;

theorem Th41:
  Lambda(S) is AffinSpace
proof
  set AS=Lambda(S);
A1: ( for x,y,z being Element of AS ex t being Element of AS st x,z // y,t &
y<>t)& for x,y,z being Element of AS ex t being Element of AS st x,y // z,t & x
  ,z // y,t by Th39;
A2: for x,y,z,t being Element of AS st z,x // x,t & x<>z ex u being Element
  of AS st y,x // x,u & y,z // t,u by Th39;
  ( for x,y,z,t,u,w being Element of AS holds x,y // y,x & x,y // z,z & (x
<>y & x,y // z,t & x,y // u,w implies z,t // u,w) & (x,y // x,z implies y,x //
  y,z))& ex x,y,z being Element of AS st not x,y // x,z by Th39;
  hence thesis by A1,A2,Def6;
end;

theorem
  (ex x,y being Element of AS st x<>y) & (for x,y,z,t,u,w being Element
of AS holds x,y // y,x & x,y // z,z & (x<>y & x,y // z,t & x,y // u,w implies z
  ,t // u,w) & (x,y // x,z implies y,x // y,z)) & (ex x,y,z being Element of AS
st not x,y // x,z) & (for x,y,z being Element of AS ex t being Element of AS st
x,z // y,t & y<>t) & (for x,y,z being Element of AS ex t being Element of AS st
x,y // z,t & x,z // y,t) & (for x,y,z,t being Element of AS st z,x // x,t & x<>
z ex u being Element of AS st y,x // x,u & y,z // t,u) iff AS is AffinSpace by
Def6,STRUCT_0:def 10;

reserve S for OAffinPlane;
reserve x,y,z,t,u for Element of S;

theorem Th43:
  not x,y '||' z,t implies ex u st x,y '||' x,u & z,t '||' z,u
proof
  assume not x,y '||' z,t;
  then ( not x,y // z,t)& not x,y // t,z by Def4;
  then consider u such that
A1: ( x,y // x,u or x,y // u,x)&( z,t // z,u or z,t // u,z) by ANALOAF:def 6;
  x,y '||' x,u & z,t '||' z,u by A1,Def4;
  hence thesis;
end;

theorem Th44:
  AS = Lambda(S) implies for x,y,z,t being Element of AS st not x,
  y // z,t ex u being Element of AS st x,y // x,u & z,t // z,u
proof
  assume
A1: AS = Lambda(S);
  let x,y,z,t be Element of AS;
  reconsider x9=x, y9=y, z9=z, t9=t as Element of S by A1;
  assume not x,y // z,t;
  then not x9,y9 '||' z9,t9 by A1,Th38;
  then consider u9 being Element of S such that
A2: x9,y9 '||' x9,u9 & z9,t9 '||' z9,u9 by Th43;
  reconsider u=u9 as Element of AS by A1;
  x,y // x,u & z,t // z,u by A1,A2,Th38;
  hence thesis;
end;

definition
  let IT be non empty AffinStruct;
  attr IT is 2-dimensional means
  :Def7:
  for x,y,z,t being Element of IT st not
  x,y // z,t ex u being Element of IT st x,y // x,u & z,t // z,u;
end;

registration
  cluster strict 2-dimensional for AffinSpace;
  existence
  proof
    set S = the OAffinPlane;
    reconsider AS = Lambda(S) as AffinSpace by Th41;
    for x,y,z,t being Element of AS st not x,y // z,t ex u being Element
    of AS st x,y // x,u & z,t // z,u by Th44;
    then AS is 2-dimensional by Def7;
    hence thesis;
  end;
end;

definition
  mode AffinPlane is 2-dimensional AffinSpace;
end;

theorem
  Lambda(S) is AffinPlane
proof
  set AS = Lambda(S);
  for x,y,z,t being Element of AS st not x,y // z,t ex u being Element of
  AS st x,y // x,u & z,t // z,u by Th44;
  hence thesis by Def7,Th41;
end;

theorem
  AS is AffinPlane iff (ex x,y being Element of AS st x<>y) & (for x,y,z
,t,u,w being Element of AS holds x,y // y,x & x,y // z,z & (x<>y & x,y // z,t &
  x,y // u,w implies z,t // u,w) & (x,y // x,z implies y,x // y,z)) & (ex x,y,z
  being Element of AS st not x,y // x,z) & (for x,y,z being Element of AS ex t
being Element of AS st x,z // y,t & y<>t) & (for x,y,z being Element of AS ex t
being Element of AS st x,y // z,t & x,z // y,t) & (for x,y,z,t being Element of
AS st z,x // x,t & x<>z ex u being Element of AS st y,x // x,u & y,z // t,u) &
for x,y,z,t being Element of AS st not x,y // z,t ex u being Element of AS st x
  ,y // x,u & z,t // z,u by Def6,Def7,STRUCT_0:def 10;