:: Fano-Desargues Parallelity Spaces
::  by Eugeniusz Kusak and Wojciech Leo\'nczuk
::
:: Received March 23, 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 RLVECT_1, ALGSTR_0, XBOOLE_0, SUBSET_1, ARYTM_1, SUPINF_2,
      ARYTM_3, VECTSP_1, PARSP_1, ZFMISC_1, STRUCT_0, MCART_1, RELAT_1,
      GROUP_1, MESFUNC1, PARSP_2, RECDEF_2;
 notations ZFMISC_1,
      XTUPLE_0, SUBSET_1, MCART_1, DOMAIN_1, STRUCT_0, ALGSTR_0, RLVECT_1,
      GROUP_1, VECTSP_1, PARSP_1;
 constructors DOMAIN_1, PARSP_1, XTUPLE_0;
 registrations XBOOLE_0, STRUCT_0, VECTSP_1, PARSP_1, XTUPLE_0;
 definitions XTUPLE_0;
 theorems MCART_1, VECTSP_1, PARSP_1, RLVECT_1, GROUP_1, XTUPLE_0;

begin

:: 1. A CONSTRUCTION OF A MODEL OF A FANO-DESARGUES SPACE

Lm1: for F being add-associative right_zeroed right_complementable non empty
addLoopStr, a,b being Element of F holds a - b = 0.F implies a = b
proof
  let F be add-associative right_zeroed right_complementable non empty
  addLoopStr, a,b be Element of F;
  assume a - b = 0.F;
  then a + -b = 0.F by RLVECT_1:def 11;
  then a = - -b by RLVECT_1:6;
  hence thesis by RLVECT_1:17;
end;

Lm2: for F being add-associative right_zeroed right_complementable non empty
addLoopStr, x,y being Element of F holds (x+(-y)=0.F iff x=y) & (x-y=0.F iff x
=y)
proof
  let F be add-associative right_zeroed right_complementable non empty
  addLoopStr, x,y be Element of F;
A1: x+(-y)=0.F implies x=y
  proof
    assume x+(-y)=0.F;
    then x+((-y)+y)=0.F+y by RLVECT_1:def 3;
    then x+0.F=0.F+y by RLVECT_1:5;
    then x=0.F+y by RLVECT_1:4;
    hence thesis by RLVECT_1:4;
  end;
A2: x-y=0.F implies x=y
  proof
    assume x-y=0.F;
    then x+(-y)+y=0.F+y by RLVECT_1:def 11;
    then x+((-y)+y)=0.F+y by RLVECT_1:def 3;
    then x+0.F=0.F+y by RLVECT_1:5;
    then x=0.F+y by RLVECT_1:4;
    hence thesis by RLVECT_1:4;
  end;
  x=y implies x-y=0.F
  proof
    assume x=y;
    then x-y=y+(-y) by RLVECT_1:def 11;
    hence thesis by RLVECT_1:5;
  end;
  hence thesis by A1,A2,RLVECT_1:5;
end;

reserve F for Field;

theorem Th1:
  MPS(F) is ParSp
proof
  for a,b,c,d,p,q,r,s being Element of MPS(F) holds a,b '||' b,a & a,b
  '||' c,c & (a,b '||' p,q & a,b '||' r,s implies p,q '||' r,s or a=b) & (a,b
'||' a,c implies b,a '||' b,c) & ex x being Element of MPS(F) st a,b '||' c,x &
  a,c '||' b,x by PARSP_1:13,14,15,16,17;
  hence thesis by PARSP_1:def 12;
end;

reserve a,b,c,d,p,q,r for Element of MPS(F);
reserve e,f,g,h,i,j,k,l,m,n,o,w for Element of [:the carrier of F,the carrier
  of F,the carrier of F:];
reserve K,L,M,N,R,S for Element of F;

Lm3: (e`1_3-f`1_3)*(g`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3) = 0.F &
   (e`1_3-f`1_3)*(g`3_3-h`3_3) - (
g`1_3-h`1_3)*(e`3_3-f`3_3) = 0.F &
  (e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3) = 0.F iff
(ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 & K*(e`2_3-f`2_3) = g`2_3-h`2_3 &
    K*(e`3_3-f`3_3) = g`3_3-h`3_3)
or e`1_3-f`1_3 = 0.F & e`2_3-f`2_3 = 0.F & e`3_3-f`3_3 = 0.F
proof
A1: (e`1_3-f`1_3)*(g`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3) = 0.F &
   (e`1_3-f`1_3)*(g`3_3-h`3_3) -
  (g`1_3-h`1_3)*(e`3_3-f`3_3) = 0.F &
(e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3) = 0.F
implies (ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 &
  K*(e`2_3-f`2_3) = g`2_3-h`2_3 & K*(e`3_3-f`3_3) =
  g`3_3-h`3_3) or e`1_3-f`1_3 = 0.F & e`2_3-f`2_3 = 0.F & e`3_3-f`3_3 = 0.F
  proof
    assume that
A2: (e`1_3-f`1_3)*(g`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3) = 0.F and
A3: (e`1_3-f`1_3)*(g`3_3-h`3_3) - (g`1_3-h`1_3)*(e`3_3-f`3_3) = 0.F and
A4: (e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3) = 0.F;
    now
A5:   now
        assume
A6:     e`3_3-f`3_3 <> 0.F;
A7:     ((g`3_3-h`3_3)*(e`3_3-f`3_3)")*(e`3_3-f`3_3)
  = (g`3_3-h`3_3)*((e`3_3-f`3_3)"*(e`3_3-f`3_3
        )) by GROUP_1:def 3
          .= (g`3_3-h`3_3)*1_F by A6,VECTSP_1:def 10
          .= g`3_3-h`3_3 by VECTSP_1:def 8;
A8:     ((g`3_3-h`3_3)*(e`3_3-f`3_3)")*(e`2_3-f`2_3)
  = ((e`2_3-f`2_3)*(g`3_3-h`3_3))*(e`3_3-f`3_3
        )" by GROUP_1:def 3
          .= ((g`2_3-h`2_3)*(e`3_3-f`3_3))*(e`3_3-f`3_3)" by A4,Lm1
          .= (g`2_3-h`2_3)*((e`3_3-f`3_3)*(e`3_3-f`3_3)") by GROUP_1:def 3
          .= (g`2_3-h`2_3)*1_F by A6,VECTSP_1:def 10
          .= g`2_3-h`2_3 by VECTSP_1:def 8;
        ((g`3_3-h`3_3)*(e`3_3-f`3_3)")*(e`1_3-f`1_3)
   = ((e`1_3-f`1_3)*(g`3_3-h`3_3))*(e`3_3-f`3_3
        )" by GROUP_1:def 3
          .= ((g`1_3-h`1_3)*(e`3_3-f`3_3))*(e`3_3-f`3_3)" by A3,Lm1
          .= (g`1_3-h`1_3)*((e`3_3-f`3_3)*(e`3_3-f`3_3)") by GROUP_1:def 3
          .= (g`1_3-h`1_3)*1_F by A6,VECTSP_1:def 10
          .= g`1_3-h`1_3 by VECTSP_1:def 8;
        hence thesis by A8,A7;
      end;
A9:   now
        assume
A10:    e`2_3-f`2_3 <> 0.F;
A11:    ((g`2_3-h`2_3)*(e`2_3-f`2_3)")*(e`2_3-f`2_3)
  = (g`2_3-h`2_3)*((e`2_3-f`2_3)"*(e`2_3-f`2_3
        )) by GROUP_1:def 3
          .= (g`2_3-h`2_3)*1_F by A10,VECTSP_1:def 10
          .= g`2_3-h`2_3 by VECTSP_1:def 8;
A12:    ((g`2_3-h`2_3)*(e`2_3-f`2_3)")*(e`3_3-f`3_3)
          = (e`2_3-f`2_3)"*((g`2_3-h`2_3)*(e`3_3-f`3_3
        )) by GROUP_1:def 3
          .= (e`2_3-f`2_3)"*((e`2_3-f`2_3)*(g`3_3-h`3_3)) by A4,Lm1
          .= ((e`2_3-f`2_3)"*(e`2_3-f`2_3))*(g`3_3-h`3_3) by GROUP_1:def 3
          .= (g`3_3-h`3_3)*1_F by A10,VECTSP_1:def 10
          .= g`3_3-h`3_3 by VECTSP_1:def 8;
        ((g`2_3-h`2_3)*(e`2_3-f`2_3)")*(e`1_3-f`1_3)
   = ((e`1_3-f`1_3)*(g`2_3-h`2_3))*(e`2_3-f`2_3
        )" by GROUP_1:def 3
          .= ((g`1_3-h`1_3)*(e`2_3-f`2_3))*(e`2_3-f`2_3)" by A2,Lm1
          .= (g`1_3-h`1_3)*((e`2_3-f`2_3)*(e`2_3-f`2_3)") by GROUP_1:def 3
          .= (g`1_3-h`1_3)*1_F by A10,VECTSP_1:def 10
          .= g`1_3-h`1_3 by VECTSP_1:def 8;
        hence thesis by A11,A12;
      end;
      now
        assume
A13:    e`1_3-f`1_3 <> 0.F;
A14:    ((g`1_3-h`1_3)*(e`1_3-f`1_3)")*(e`1_3-f`1_3)
      = (g`1_3-h`1_3)*((e`1_3-f`1_3)"*(e`1_3-f`1_3)
        ) by GROUP_1:def 3
          .= (g`1_3-h`1_3)*1_F by A13,VECTSP_1:def 10
          .= g`1_3-h`1_3 by VECTSP_1:def 8;
A15:    ((g`1_3-h`1_3)*(e`1_3-f`1_3)")*(e`3_3-f`3_3)
   = (e`1_3-f`1_3)"*((g`1_3-h`1_3)*(e`3_3-f`3_3
        )) by GROUP_1:def 3
          .= (e`1_3-f`1_3)"*((e`1_3-f`1_3)*(g`3_3-h`3_3)) by A3,Lm1
          .= ((e`1_3-f`1_3)"*(e`1_3-f`1_3))*(g`3_3-h`3_3) by GROUP_1:def 3
          .= (g`3_3-h`3_3)*1_F by A13,VECTSP_1:def 10
          .= g`3_3-h`3_3 by VECTSP_1:def 8;
        ((g`1_3-h`1_3)*(e`1_3-f`1_3)")*(e`2_3-f`2_3)
   = (e`1_3-f`1_3)"*((g`1_3-h`1_3)*(e`2_3-f`2_3)
        ) by GROUP_1:def 3
          .= (e`1_3-f`1_3)"*((e`1_3-f`1_3)*(g`2_3-h`2_3)) by A2,Lm1
          .= ((e`1_3-f`1_3)"*(e`1_3-f`1_3))*(g`2_3-h`2_3) by GROUP_1:def 3
          .= (g`2_3-h`2_3)*1_F by A13,VECTSP_1:def 10
          .= g`2_3-h`2_3 by VECTSP_1:def 8;
        hence thesis by A14,A15;
      end;
      hence thesis by A9,A5;
    end;
    hence thesis;
  end;
  (ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 & K*(e`2_3-f`2_3) = g`2_3-h`2_3 &
    K*(e`3_3-f`3_3) =
g`3_3-h`3_3) or e`1_3-f`1_3 = 0.F & e`2_3-f`2_3 = 0.F &
 e`3_3-f`3_3 = 0.F implies (e`1_3-f`1_3)*(g
`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3) = 0.F &
  (e`1_3-f`1_3)*(g`3_3-h`3_3) - (g`1_3-h`1_3)*(e`3_3-f`3_3)
  = 0.F & (e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3) = 0.F
  proof
A16: now
      given K such that
A17:  K*(e`1_3-f`1_3) = g`1_3-h`1_3 and
A18:  K*(e`2_3-f`2_3) = g`2_3-h`2_3 & K*(e`3_3-f`3_3) = g`3_3-h`3_3;
A19:  (e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3)
   = (K*(e`2_3-f`2_3))*(e`3_3-f`3_3)
      - (K*(e`2_3-f`2_3))*(e`3_3-f`3_3) by A18,GROUP_1:def 3;
      (e`1_3-f`1_3)*(g`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3)
  = (K*(e`1_3-f`1_3))*(e`2_3-f`2_3)
- (K*(e`1_3 -f`1_3))*(e`2_3-f`2_3) &
  (e`1_3-f`1_3)*(g`3_3-h`3_3) - (g`1_3-h`1_3)*(e`3_3-f`3_3) = (K*(e
      `1_3-f`1_3))*( e`3_3-f`3_3) - (K*(e`1_3-f`1_3))*(e`3_3-f`3_3)
   by A17,A18,GROUP_1:def 3;
      hence thesis by A19,RLVECT_1:15;
    end;
A20: now
      assume that
A21:  e`1_3-f`1_3 = 0.F and
A22:  e`2_3-f`2_3 = 0.F and
A23:  e`3_3-f`3_3 = 0.F;
A24:  (g`1_3-h`1_3)*(e`3_3-f`3_3) = 0.F by A23,VECTSP_1:7;
      (e`1_3-f`1_3)*(g`2_3-h`2_3) = 0.F & (e`1_3-f`1_3)*(g`3_3-h`3_3) = 0.F
  by A21,VECTSP_1:7;
      hence thesis by A21,A22,A24,RLVECT_1:15;
    end;
    assume (ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 &
  K*(e`2_3-f`2_3) = g`2_3-h`2_3 & K*(e`3_3-f
    `3_3) = g`3_3-h`3_3) or e`1_3-f`1_3 = 0.F &
  e`2_3-f`2_3 = 0.F & e`3_3-f`3_3 = 0.F;
    hence thesis by A20,A16;
  end;
  hence thesis by A1;
end;

theorem Th2:
  a,b '||' c,d iff ex e,f,g,h st [a,b,c,d] = [e,f,g,h] & ((ex K st
K*(e`1_3-f`1_3) = g`1_3-h`1_3 & K*(e`2_3-f`2_3) = g`2_3-h`2_3 &
  K*(e`3_3-f`3_3) = g`3_3-h`3_3) or e`1_3-f
  `1_3 = 0.F & e`2_3-f`2_3 = 0.F & e`3_3-f`3_3 = 0.F )
proof
A1: a,b '||' c,d implies ex e,f,g,h st [a,b,c,d] = [e,f,g,h] & ((ex K st K*(
e`1_3-f`1_3) = g`1_3-h`1_3 & K*(e`2_3-f`2_3) = g`2_3-h`2_3 &
  K*(e`3_3-f`3_3) = g`3_3-h`3_3) or e`1_3-f`1_3
  = 0.F & e`2_3-f`2_3 = 0.F & e`3_3-f`3_3 = 0.F )
  proof
    assume a,b '||' c,d;
    then consider e,f,g,h such that
A2: [a,b,c,d] = [e,f,g,h] and
A3: (e`1_3-f`1_3)*(g`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3)
 = 0.F & (e`1_3-f`1_3)*(g`3_3-h
`3_3) - (g `1_3 -h`1_3)*(e`3_3-f`3_3) = 0.F &
  (e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3) =
    0.F by PARSP_1:12;
    (ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 &
  K*(e`2_3-f`2_3) = g`2_3-h`2_3 & K*(e`3_3-f`3_3) =
    g`3_3-h`3_3) or e`1_3-f`1_3 = 0.F & e`2_3-f`2_3 = 0.F & e`3_3-f`3_3 = 0.F
  by A3,Lm3;
    hence thesis by A2;
  end;
  (ex e,f,g,h st [a,b,c,d] = [e,f,g,h] &
   ((ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 &
K*(e`2_3-f`2_3) = g`2_3-h`2_3 &
   K*(e`3_3-f`3_3) = g`3_3-h`3_3) or (e`1_3-f`1_3 = 0.F & e`2_3-f`2_3 = 0.
  F & e`3_3-f`3_3 = 0.F))) implies a,b '||' c,d
  proof
    given e,f,g,h such that
A4: [a,b,c,d] = [e,f,g,h] and
A5: (ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 &
      K*(e`2_3-f`2_3) = g`2_3-h`2_3 & K*(e`3_3-f
    `3_3 ) = g`3_3-h`3_3) or e`1_3-f`1_3 = 0.F &
         e`2_3-f`2_3 = 0.F & e`3_3-f`3_3 = 0.F;
A6: (e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3) = 0.F by A5,Lm3;
    (e`1_3-f`1_3)*(g`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3) = 0.F &
   (e`1_3-f`1_3)*(g`3_3-h`3_3)
    - (g`1_3 -h`1_3)*(e`3_3-f`3_3) = 0.F by A5,Lm3;
    hence thesis by A4,A6,PARSP_1:12;
  end;
  hence thesis by A1;
end;

theorem Th3:
  not a,b '||' a,c & [a,b,a,c]=[e,f,e,g] implies e<>f & e<>g & f<>g
proof
  assume
A1: ( not a,b '||' a,c)& [a,b,a,c]=[e,f,e,g];
  then
  0.F*(e`1_3-f`1_3) <> e`1_3-g`1_3 or 0.F*(e`2_3-f`2_3) <> e`2_3-g`2_3 or
  0.F*(e`3_3-f`3_3) <>
  e`3_3-g`3_3 by Th2;
  then
A2: 0.F <> e`1_3-g`1_3 or 0.F <> e`2_3-g`2_3 or 0.F <> e`3_3-g`3_3
 by VECTSP_1:12;
A3: f<>g
  proof
    assume
A4: not thesis;
    (e`1_3-f`1_3)*1_F <> e`1_3-g`1_3 or (e`2_3-f`2_3)*1_F <> e`2_3-g`2_3 or
(e`3_3-f`3_3)*1_F
    <> e`3_3-g`3_3 by A1,Th2;
    hence contradiction by A4,VECTSP_1:def 8;
  end;
  e`1_3-f`1_3 <> 0.F or e`2_3-f`2_3 <> 0.F or e`3_3-f`3_3 <> 0.F by A1,Th2;
  hence thesis by A2,A3,RLVECT_1:15;
end;

theorem Th4:
  not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] & K*(e`1_3-f`1_3)=L*(e`1_3-g`1_3
  ) & K*(e`2_3-f`2_3)=L*(e`2_3-g`2_3) & K*(e`3_3-f`3_3)=L*(e`3_3-g`3_3)
  implies K=0.F & L=0.F
proof
  assume that
A1: ( not a,b '||' a,c)& [a,b,a,c] = [e,f,e,g] and
A2: K*(e`1_3-f`1_3)=L*(e`1_3-g`1_3) and
A3: K*(e`2_3-f`2_3)=L*(e`2_3-g`2_3) and
A4: K*(e`3_3-f`3_3)=L*(e`3_3-g`3_3);
  e=[e`1_3,e`2_3,e`3_3] & g=[g`1_3,g`2_3,g`3_3] by MCART_1:44;
  then e`1_3 <> g`1_3 or e`2_3 <> g`2_3 or e`3_3 <> g`3_3 by A1,Th3;
  then
A5: e`1_3-g`1_3 <> 0.F or e`2_3-g`2_3 <> 0.F or e`3_3-g`3_3 <> 0.F by Lm2;
  K*(e`1_3-f`1_3)*(e`2_3-g`2_3)=L*((e`1_3-g`1_3)*(e`2_3-g`2_3)) &
 K*(e`2_3-f`2_3)*(e`1_3-g`1_3)=L*
  ((e `2_3-g`2_3)*(e`1_3-g`1_3)) by A2,A3,GROUP_1:def 3;
  then K*(e`1_3-f`1_3)*(e`2_3-g`2_3)-K*(e`2_3-f`2_3)*(e`1_3-g`1_3) = 0.F
by RLVECT_1:15;
  then K*((e`1_3-f`1_3)*(e`2_3-g`2_3))-K*(e`2_3-f`2_3)*(e`1_3-g`1_3) = 0.F
by GROUP_1:def 3;
  then K*((e`1_3-f`1_3)*(e`2_3-g`2_3))-K*((e`2_3-f`2_3)*(e`1_3-g`1_3)) = 0.F
by GROUP_1:def 3;
  then
A6: K*((e`1_3-f`1_3)*(e`2_3-g`2_3)-(e`1_3-g`1_3)*(e`2_3-f`2_3)) = 0.F
by VECTSP_1:11;
  K*(e`1_3-f`1_3)*(e`3_3-g`3_3)=L*((e`1_3-g`1_3)*(e`3_3-g`3_3)) &
K*(e`3_3-f`3_3)*(e`1_3-g`1_3)=L
  *((e `3_3-g`3_3)*(e`1_3-g`1_3)) by A2,A4,GROUP_1:def 3;
  then K*(e`1_3-f`1_3)*(e`3_3-g`3_3)-K*(e`3_3-f`3_3)*(e`1_3-g`1_3) = 0.F
by RLVECT_1:15;
  then K*((e`1_3-f`1_3)*(e`3_3-g`3_3))-K*(e`3_3-f`3_3)*(e`1_3-g`1_3) = 0.F
by GROUP_1:def 3;
  then K*((e`1_3-f`1_3)*(e`3_3-g`3_3))-K*((e`3_3-f`3_3)*(e`1_3-g`1_3)) = 0.F
by GROUP_1:def 3;
  then
A7: K*((e`1_3-f`1_3)*(e`3_3-g`3_3)-(e`1_3-g`1_3)*(e`3_3-f`3_3)) = 0.F
by VECTSP_1:11;
  K*(e`2_3-f`2_3)*(e`3_3-g`3_3)=L*((e`2_3-g`2_3)*(e`3_3-g`3_3)) &
  K*(e`3_3-f`3_3)*(e`2_3-g`2_3)=L*
  ((e `3_3-g`3_3)*(e`2_3-g`2_3)) by A3,A4,GROUP_1:def 3;
  then K*(e`2_3-f`2_3)*(e`3_3-g`3_3)-K*(e`3_3-f`3_3)*(e`2_3-g`2_3) = 0.F
 by RLVECT_1:15;
  then K*((e`2_3-f`2_3)*(e`3_3-g`3_3))-K*(e`3_3-f`3_3)*(e`2_3-g`2_3) = 0.F
 by GROUP_1:def 3;
  then K*((e`2_3-f`2_3)*(e`3_3-g`3_3))-K*((e`3_3-f`3_3)*(e`2_3-g`2_3)) = 0.F
 by GROUP_1:def 3;
  then
A8: K*((e`2_3-f`2_3)*(e`3_3-g`3_3)-(e`2_3-g`2_3)*(e`3_3-f`3_3)) = 0.F
 by VECTSP_1:11;
A9: (e`1_3-f`1_3)*(e`2_3-g`2_3)-(e`1_3-g`1_3)*(e`2_3-f`2_3) <> 0.F or
 (e`2_3-f`2_3)*(e`3_3-g`3_3)-(
e`2_3-g`2_3)*(e`3_3-f`3_3) <> 0.F or
(e`1_3-f`1_3)*(e`3_3-g`3_3)-(e`1_3-g`1_3)*(e`3_3-f`3_3) <> 0.F by A1,PARSP_1:12
;
  then
A10: K=0.F by A6,A8,A7,VECTSP_1:12;
  then
A11: 0.F=L*(e`3_3-g`3_3) by A4,VECTSP_1:7;
  0.F=L*(e`1_3-g`1_3) & 0.F=L*(e`2_3-g`2_3) by A2,A3,A10,VECTSP_1:7;
  hence thesis by A6,A8,A7,A9,A11,A5,VECTSP_1:12;
end;

Lm4: for F being add-associative right_zeroed right_complementable non empty
addLoopStr, a, b, c being Element of F holds (b+a)-(c+a) = b-c
proof
  let F be add-associative right_zeroed right_complementable non empty
  addLoopStr, a,b,c be Element of F;
  thus (b+a)-(c+a) = (b+a)+-(c+a) by RLVECT_1:def 11
    .= (b+a)+(-a+-c) by RLVECT_1:31
    .= ((b+a)+-a)+-c by RLVECT_1:def 3
    .= (b+(a+-a))+-c by RLVECT_1:def 3
    .= (b+0.F)+-c by RLVECT_1:def 10
    .= b+-c by RLVECT_1:4
    .= b-c by RLVECT_1:def 11;
end;

Lm5: (K-L)-(R-L)=K-R
proof
  thus (K-L)-(R-L)=(K+(-L))-(R-L) by RLVECT_1:def 11
    .= ((-L)+K)-(R+(-L)) by RLVECT_1:def 11
    .= K-R by Lm4;
end;

Lm6: K*(N-M)-L*(N-S)=S-M implies (K+(-1_F))*(N-M)=(L+(-1_F))*(N-S)
proof
  assume K*(N-M)-L*(N-S) = S-M;
  then K*(N-M)-L*(N-S) = S+(-M) by RLVECT_1:def 11
    .= S+(-M)+0.F by RLVECT_1:4
    .= (-M)+S+(-(N)+N) by RLVECT_1:5
    .= S+((-(N)+N)+(-M)) by RLVECT_1:def 3
    .= S+(-(N)+(N+(-M))) by RLVECT_1:def 3
    .= S+(-(N)+(N-M)) by RLVECT_1:def 11
    .= (S+(-(N)))+(N-M) by RLVECT_1:def 3
    .= (S-N)+(N-M) by RLVECT_1:def 11;
  then K*(N-M)+(-L*(N-S))+L*(N-S) = (S-N)+(N-M)+L*(N-S) by RLVECT_1:def 11;
  then K*(N-M)+((-L*(N-S))+L*(N-S)) = (S-N)+(N-M)+L*(N-S) by RLVECT_1:def 3;
  then K*(N-M)+0.F = (S-N)+(N-M)+L*(N-S) by RLVECT_1:5;
  then K*(N-M) = (S-N)+(N-M)+L*(N-S) by RLVECT_1:4
    .= ((S-N)+L*(N-S))+(N-M) by RLVECT_1:def 3;
  then K*(N-M)+(-(N-M)) = ((S-N)+L*(N-S))+((N-M)+(-(N-M))) by RLVECT_1:def 3
    .= ((S-N)+L*(N-S))+0.F by RLVECT_1:5
    .= (S-N)+L*(N-S) by RLVECT_1:4
    .= (S+-N)+L*(N-S) by RLVECT_1:def 11
    .= L*(N-S)+(-(N-S)) by RLVECT_1:33;
  then K*(N-M)+(-(1_F*(N-M))) = L*(N-S)+(-(N-S)) by VECTSP_1:def 8;
  then K*(N-M)+((-1_F)*(N-M)) = L*(N-S)+(-(N-S)) by VECTSP_1:9;
  then (K+(-1_F))*(N-M) = L*(N-S)+(-(N-S)) by VECTSP_1:def 7
    .= L*(N-S)+(-(1_F*(N-S))) by VECTSP_1:def 8
    .= L*(N-S)+((-1_F)*(N-S)) by VECTSP_1:9;
  hence thesis by VECTSP_1:def 7;
end;

Lm7: K-L=N-M implies M=L+N-K
proof
  assume K-L=N-M;
  then M+(K+(-L))=M+(N-M) by RLVECT_1:def 11;
  then M+(K+(-L))=M+(N+(-M)) by RLVECT_1:def 11;
  then (M+K)+(-L)=M+(N+(-M)) by RLVECT_1:def 3;
  then (M+K)+(-L)=(M+N)+(-M) by RLVECT_1:def 3;
  then M+K-L=N+M+(-M) by RLVECT_1:def 11;
  then M+K-L=N+(M+(-M)) by RLVECT_1:def 3;
  then M+K-L=N+0.F by RLVECT_1:5;
  then M+K-L+L=N+L by RLVECT_1:4;
  then M+K+(-L)+L=N+L by RLVECT_1:def 11;
  then M+K+((-L)+L)=N+L by RLVECT_1:def 3;
  then M+K+0.F=L+N by RLVECT_1:5;
  then M+K+(-K)=L+N+(-K) by RLVECT_1:4;
  then M+K+(-K)=L+N-K by RLVECT_1:def 11;
  then M+(K+(-K))=L+N-K by RLVECT_1:def 3;
  then M+0.F=L+N-K by RLVECT_1:5;
  hence thesis by RLVECT_1:4;
end;

theorem Th5:
  not a,b '||' a,c & a,b '||' c,d & a,c '||' b,d & [a,b,c,d] = [e,f
  ,g,h] implies h`1_3=f`1_3+g`1_3-e`1_3 & h`2_3=f`2_3+g`2_3-e`2_3 &
 h`3_3=f`3_3+g`3_3-e`3_3
proof
  assume that
A1: not a,b '||' a,c and
A2: a,b '||' c,d and
A3: a,c '||' b,d and
A4: [a,b,c,d]=[e,f,g,h];
A5: e=[e`1_3,e`2_3,e`3_3] by MCART_1:44;
  consider m,n,o,w such that
A6: [a,c,b,d]=[m,n,o,w] and
A7: ( ex L st L*(m`1_3-n`1_3) = o`1_3-w`1_3 & L*(m`2_3-n`2_3) = o`2_3-w`2_3 &
 L*(m`3_3-n
  `3_3) = o`3_3-w`3_3) or m`1_3-n`1_3=0.F & m`2_3-n`2_3=0.F &
 m`3_3-n`3_3=0.F by A3,Th2;
A8: b=f by A4,XTUPLE_0:5;
  then
A9: o=f by A6,XTUPLE_0:5;
  d=h by A4,XTUPLE_0:5;
  then
A10: w=h by A6,XTUPLE_0:5;
  c =g by A4,XTUPLE_0:5;
  then
A11: n=g by A6,XTUPLE_0:5;
A12: a=e by A4,XTUPLE_0:5;
  then
A13: [a,b,a,c]=[e,f,e,g] by A4,A8,XTUPLE_0:5;
  consider i,j,k,l such that
A14: [a,b,c,d]=[i,j,k,l] and
A15: ( ex K st K*(i`1_3-j`1_3) = k`1_3-l`1_3 & K*(i`2_3-j`2_3) = k`2_3-l`2_3 &
  K*(i`3_3-j
  `3_3) = k`3_3-l`3_3) or i`1_3-j`1_3=0.F & i`2_3-j`2_3=0.F &
  i`3_3-j`3_3=0.F by A2,Th2;
A16: e=i & f=j by A4,A14,XTUPLE_0:5;
A17: g=k & h=l by A4,A14,XTUPLE_0:5;
A18: e=m by A12,A6,XTUPLE_0:5;
  f=[f`1_3,f`2_3,f`3_3] by MCART_1:44;
  then e`1_3<>f`1_3 or e`2_3<>f`2_3 or e`3_3<>f`3_3 by A1,A13,A5,Th3;
  then consider K such that
A19: K*(e`1_3-f`1_3) = g`1_3-h`1_3 and
A20: K*(e`2_3-f`2_3) = g`2_3-h`2_3 and
A21: K*(e`3_3-f`3_3) = g`3_3-h`3_3 by A15,A16,A17,Lm2;
  g=[g`1_3,g`2_3,g`3_3] by MCART_1:44;
  then e`1_3<>g`1_3 or e`2_3<>g`2_3 or e`3_3<>g`3_3 by A1,A13,A5,Th3;
  then consider L such that
A22: L*(e`1_3-g`1_3) = f`1_3-h`1_3 and
A23: L*(e`2_3-g`2_3) = f`2_3-h`2_3 and
A24: L*(e`3_3-g`3_3) = f`3_3-h`3_3 by A7,A18,A11,A9,A10,Lm2;
  K*(e`2_3-f`2_3)-L*(e`2_3-g`2_3) = g`2_3-f`2_3 by A20,A23,Lm5;
  then
A25: (K+(-1_F))*(e`2_3-f`2_3) = (L+(-1_F))*(e`2_3-g`2_3) by Lm6;
  K*(e`3_3-f`3_3)-L*(e`3_3-g`3_3) = g`3_3-f`3_3 by A21,A24,Lm5;
  then
A26: (K+(-1_F))*(e`3_3-f`3_3) = (L+(-1_F))*(e`3_3-g`3_3) by Lm6;
  K*(e`1_3-f`1_3)-L*(e`1_3-g`1_3) = g`1_3-f`1_3 by A19,A22,Lm5;
  then (K+(-1_F))*(e`1_3-f`1_3) = (L+(-1_F))*(e`1_3-g`1_3) by Lm6;
  then
A27: K+(-1_F)=0.F by A1,A13,A25,A26,Th4;
  then (e`2_3-f`2_3)*1_F = g`2_3-h`2_3 by A20,Lm2;
  then
A28: e`2_3-f`2_3 = g`2_3-h`2_3 by VECTSP_1:def 8;
  (e`3_3-f`3_3)*1_F = g`3_3-h`3_3 by A21,A27,Lm2;
  then
A29: e`3_3-f`3_3 = g`3_3-h`3_3 by VECTSP_1:def 8;
  (e`1_3-f`1_3)*1_F = g`1_3- h`1_3 by A19,A27,Lm2;
  then e`1_3-f`1_3 = g`1_3-h`1_3 by VECTSP_1:def 8;
  hence thesis by A28,A29,Lm7;
end;

Lm8: L*K-L*R=R+K implies (L-1_F)*K=(L+1_F)*R
proof
  assume L*K-L*R=R+K;
  then L*K+(-L*R)+(-K)=R+K+(-K) by RLVECT_1:def 11
    .=R+(K+(-K)) by RLVECT_1:def 3
    .=R+0.F by RLVECT_1:5
    .=R by RLVECT_1:4;
  then (L*K+(-K))+(-L*R)=R by RLVECT_1:def 3;
  then (L*K+(-(1_F*K)))+(-L*R)=R by VECTSP_1:def 8;
  then (L*K+(-1_F)*K)+(-L*R)=R by VECTSP_1:9;
  then (L+(-1_F))*K+(-L*R)=R by VECTSP_1:def 7;
  then (L-1_F)*K+(-L*R)+L*R=R+L*R by RLVECT_1:def 11;
  then (L-1_F)*K+((-L*R)+L*R)=R+L*R by RLVECT_1:def 3;
  then (L-1_F)*K+0.F=R+L*R by RLVECT_1:5;
  then (L-1_F)*K=L*R+R by RLVECT_1:4
    .=L*R+1_F*R by VECTSP_1:def 8;
  hence thesis by VECTSP_1:def 7;
end;

Lm9: L*(K-N)=R-S & S=K+N-R implies (L-1_F)*(R-N)=(L+1_F)*(R-K)
proof
  assume L*(K-N)=R-S & S=K+N-R;
  then
A1: L*(K-N)=R+(-(K+N-R)) by RLVECT_1:def 11
    .=R+(R+(-(K+N))) by RLVECT_1:33
    .=R+(R+(-K+(-N))) by RLVECT_1:31
    .=R+(-N+(R+(-K))) by RLVECT_1:def 3
    .=(R+(-N))+(R+(-K)) by RLVECT_1:def 3
    .=(R-N)+(R+(-K)) by RLVECT_1:def 11
    .=(R-K)+(R-N) by RLVECT_1:def 11;
  L*(R-N)-L*(R-K)=L*(R+(-N))-L*(R-K) by RLVECT_1:def 11
    .=L*(R+(-N))-L*(R+(-K)) by RLVECT_1:def 11
    .=L*(R+(-N))+(-L*(R+(-K))) by RLVECT_1:def 11
    .=L*R+L*(-N)+(-L*(R+(-K))) by VECTSP_1:def 7
    .=L*R+L*(-N)+((-L)*(R+(-K))) by VECTSP_1:9
    .=L*R+L*(-N)+((-L)*R+(-L)*(-K)) by VECTSP_1:def 7
    .=L*R+L*(-N)+((-L)*R+L*K) by VECTSP_1:10
    .=L*(-N)+L*R+(-L*R+L*K) by VECTSP_1:9
    .=L*(-N)+L*R+(-L*R)+L*K by RLVECT_1:def 3
    .=L*(-N)+(L*R+(-L*R))+L*K by RLVECT_1:def 3
    .=L*(-N)+0.F+L*K by RLVECT_1:5
    .=L*K+L*(-N) by RLVECT_1:4
    .=L*(K+(-N)) by VECTSP_1:def 7
    .=L*(K-N) by RLVECT_1:def 11;
  hence thesis by A1,Lm8;
end;

Lm10: K=L+M-N & R=L+S-N implies 1_F*(M-S)=K-R
proof
  assume that
A1: K=L+M-N and
A2: R=L+S-N;
  -R=-(L+S+(-N)) by A2,RLVECT_1:def 11
    .=-(L+S)+(-(-N)) by RLVECT_1:31
    .=-(L+S)+N by RLVECT_1:17
    .=-L+(-S)+N by RLVECT_1:31;
  then K-R=(L+M-N)+(-L+(-S)+N) by A1,RLVECT_1:def 11
    .=(M+L+(-N))+(-L+(-S)+N) by RLVECT_1:def 11
    .=(M+L+(-N))+(-S+(-L+N)) by RLVECT_1:def 3
    .=(M+(L+(-N)))+(-S+(-L+N)) by RLVECT_1:def 3
    .=(M+(L-N))+(-S+(-L+N)) by RLVECT_1:def 11
    .=(M+(L-N))+(-S+(-L+(-(-N)))) by RLVECT_1:17
    .=(M+(L-N))+(-S+(-(L+(-N)))) by RLVECT_1:31
    .=(M+(L-N))+(-(L-N)+(-S)) by RLVECT_1:def 11
    .=((M+(L-N))+(-(L-N)))+(-S) by RLVECT_1:def 3
    .=(M+((L-N)+(-(L-N))))+(-S) by RLVECT_1:def 3
    .=(M+0.F)+(-S) by RLVECT_1:5
    .=M+(-S) by RLVECT_1:4
    .=M*1_F+(-S) by VECTSP_1:def 8
    .=M*1_F+(-S)*1_F by VECTSP_1:def 8
    .=(M+(-S))*1_F by VECTSP_1:def 7
    .=(M-S)*1_F by RLVECT_1:def 11;
  hence thesis;
end;

theorem Th6:
  ex a,b,c st not a,b '||' a,c
proof
  consider e,f,g being Element of [:the carrier of F,the carrier of F,the
  carrier of F:] such that
A1: e=[1_F,1_F,0.F] and
A2: f=[-0.F,1_F,0.F] and
A3: g=[1_F,-0.F,0.F];
A4: f`1_3=-0.F & f`2_3=1_F by A2,MCART_1:def 5,def 6;
A5: g`1_3=1_F & g`2_3=-0.F by A3,MCART_1:def 5,def 6;
  the carrier of MPS(F) = [:the carrier of F,the carrier of F,the carrier
  of F:] by PARSP_1:10;
  then consider a,b,c being Element of MPS(F) such that
A6: [a,b,a,c]=[e,f,e,g];
  take a,b,c;
  e`1_3=1_F & e`2_3=1_F by A1,MCART_1:def 5,def 6;
  then
A7: (e`1_3-f`1_3)*(e`2_3-g`2_3)-(e`1_3-g`1_3)*(e`2_3-f`2_3)
    = (1.F+(-(-0.F)))*(1.F-(-0.F))-
  (1.F-1.F)*(1.F-1.F) by A4,A5,RLVECT_1:def 11
    .= (1.F+(-(-0.F)))*(1.F+(-(-0.F)))-(1.F-1.F)*(1.F-1.F) by RLVECT_1:def 11
    .= (1.F+0.F)*(1.F+(-(-0.F)))-(1.F-1.F)*(1.F-1.F) by RLVECT_1:17
    .= (1.F+0.F)*(1.F+0.F)-(1.F-1.F)*(1.F-1.F) by RLVECT_1:17
    .= 1.F*(1.F+0.F)-(1.F-1.F)*(1.F-1.F) by RLVECT_1:4
    .= 1.F*1.F-(1.F-1.F)*(1.F-1.F) by RLVECT_1:4
    .= 1.F*1.F-0.F*(1.F-1.F) by RLVECT_1:15
    .= 1.F*1.F-0.F by VECTSP_1:12
    .= 1.F-0.F by VECTSP_1:def 8;
  now
    let e9,f9,g9,h9 be Element of [:the carrier of F,the carrier of F,the
    carrier of F:];
    assume
A8: [e9,f9,g9,h9]=[a,b,a,c];
    then
A9: g9=e & h9=g by A6,XTUPLE_0:5;
    e9=e & f9=f by A6,A8,XTUPLE_0:5;
    hence (e9`1_3-f9`1_3)*(g9`2_3-h9`2_3) - (g9`1_3-h9`1_3)*(e9`2_3-f9`2_3)
    <> 0.F or (e9`1_3-f9
`1_3)*(g9`3_3-h9`3_3) - (g9`1_3-h9`1_3)*(e9`3_3-f9`3_3) <> 0.F or
  (e9`2_3-f9`2_3)*(g9`3_3-h9`3_3) - (
    g9`2_3-h9`2_3)*(e9`3_3-f9`3_3) <> 0.F by A7,A9,Lm2;
  end;
  hence thesis by PARSP_1:12;
end;

theorem Th7:
  1_F+1_F<>0.F & b,c '||' a,d & a,b '||' c,d & a,c '||' b,d implies
  a,b '||' a,c
proof
  assume that
A1: 1_F+1_F<>0.F and
A2: b,c '||' a,d and
A3: a,b '||' c,d and
A4: a,c '||' b,d;
  assume
A5: not thesis;
  consider i,j,k,l such that
A6: [b,c,a,d]=[i,j,k,l] and
A7: (ex L st L*(i`1_3-j`1_3) = k`1_3-l`1_3 & L*(i`2_3-j`2_3) = k`2_3-l`2_3 &
  L*(i`3_3-j
  `3_3) = k`3_3-l`3_3) or i`1_3-j`1_3 = 0.F & i`2_3-j`2_3 = 0.F &
  i`3_3-j`3_3 = 0.F by A2,Th2;
A8: b=i & c =j by A6,XTUPLE_0:5;
A9: a=k & d=l by A6,XTUPLE_0:5;
  consider e,f,g,h such that
A10: [a,b,c,d]=[e,f,g,h] and
  (ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 & K*(e`2_3-f`2_3) = g`2_3-h`2_3 &
  K*(e`3_3-f`3_3 ) =
  g`3_3-h`3_3) or e`1_3-f`1_3 = 0.F & e`2_3-f`2_3 = 0.F & e`3_3-f`3_3 = 0.F
  by A3,Th2;
A11: b=f by A10,XTUPLE_0:5;
A12: d=h by A10,XTUPLE_0:5;
A13: c =g by A10,XTUPLE_0:5;
A14: a=e by A10,XTUPLE_0:5;
  then
A15: [a,b,a,c]=[e,f,e,g] by A10,A11,XTUPLE_0:5;
  f=[f`1_3,f`2_3,f`3_3] & g=[g`1_3,g`2_3,g`3_3] by MCART_1:44;
  then i`1_3<>j`1_3 or i`2_3<>j`2_3 or i`3_3<>j`3_3 by A5,A11,A13,A15,A8,Th3;
  then consider L such that
A16: L*(f`1_3-g`1_3) = e`1_3-h`1_3 and
A17: L*(f`2_3-g`2_3) = e`2_3-h`2_3 and
A18: L*(f`3_3-g`3_3) = e`3_3-h`3_3 by A14,A11,A13,A12,A7,A8,A9,Lm2;
  h`2_3=f`2_3+g`2_3-e`2_3 by A3,A4,A5,A10,Th5;
  then
A19: (L-1_F)*(e`2_3-g`2_3)=(L+1_F)*(e`2_3-f`2_3) by A17,Lm9;
  h`3_3=f`3_3+g`3_3-e`3_3 by A3,A4,A5,A10,Th5;
  then
A20: (L-1_F)*(e`3_3-g`3_3)=(L+1_F)*(e`3_3-f`3_3) by A18,Lm9;
  h`1_3=f`1_3+g`1_3-e`1_3 by A3,A4,A5,A10,Th5;
  then (L-1_F)*(e`1_3-g`1_3)=(L+1_F)*(e`1_3-f`1_3) by A16,Lm9;
  then L+1_F=0.F & L-1_F=0.F by A5,A15,A19,A20,Th4;
  then L+1_F-(L-1_F)=0.F+(-0.F) by RLVECT_1:def 11;
  then L+1_F-(L-1_F)=0.F by RLVECT_1:5;
  then L+1_F+(-(L-1_F))=0.F by RLVECT_1:def 11;
  then L+1_F+(1_F+-L)=0.F by RLVECT_1:33;
  then (L+1_F+1_F)+(-L)=0.F by RLVECT_1:def 3;
  then (1_F+1_F+L)+(-L)=0.F by RLVECT_1:def 3;
  then 1_F+1_F+(L+(-L))=0.F by RLVECT_1:def 3;
  then 1_F+1_F+0.F=0.F by RLVECT_1:5;
  hence contradiction by A1,RLVECT_1:4;
end;

theorem Th8:
  not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q & a,p '||' c,r
  & a,b '||' p,q & a,c '||' p,r implies b,c '||' q,r
proof
  assume that
A1: not a,p '||' a,b and
A2: not a,p '||' a,c and
A3: a,p '||' b,q and
A4: a,p '||' c,r and
A5: a,b '||' p,q and
A6: a,c '||' p,r;
  consider i,j,k,l such that
A7: [a,p,c,r]=[i,j,k,l] and
  (ex L st L*(i`1_3-j`1_3) = k`1_3-l`1_3 & L*(i`2_3-j`2_3) = k`2_3-l`2_3 &
  L*(i`3_3-j`3_3 ) =
  k`3_3-l`3_3) or i`1_3-j`1_3 = 0.F & i`2_3-j`2_3 = 0.F & i`3_3-j`3_3 = 0.F
  by A4,Th2;
  consider e,f,g,h such that
A8: [a,b,p,q]=[e,f,g,h] and
  (ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 & K*(e`2_3-f`2_3) = g`2_3-h`2_3 &
 K*(e`3_3-f`3_3 ) =
  g`3_3-h`3_3) or e`1_3-f`1_3 = 0.F & e`2_3-f`2_3 = 0.F & e`3_3-f`3_3 = 0.F
  by A5,Th2;
A9: a=e & p=g by A8,XTUPLE_0:5;
A10: c =k by A7,XTUPLE_0:5;
  then
A11: [a,p,c,r]=[e,g,k,l] by A9,A7,XTUPLE_0:5;
  then
A12: l`1_3=g`1_3+k`1_3-e`1_3 by A2,A4,A6,Th5;
A13: b=f by A8,XTUPLE_0:5;
  then
A14: [a,p,b,q]=[e,g,f,h] by A8,A9,XTUPLE_0:5;
  then h`1_3=g`1_3+f`1_3-e`1_3 by A1,A3,A5,Th5;
  then
A15: 1_F*(f`1_3-k`1_3)=h`1_3-l`1_3 by A12,Lm10;
A16: l`3_3=g`3_3+k`3_3-e`3_3 by A2,A4,A6,A11,Th5;
A17: l`2_3=g`2_3+k`2_3-e`2_3 by A2,A4,A6,A11,Th5;
  h`3_3=g`3_3+f`3_3-e`3_3 by A1,A3,A5,A14,Th5;
  then
A18: 1_F*(f`3_3-k`3_3)=h`3_3-l`3_3 by A16,Lm10;
  h`2_3=g`2_3+f`2_3-e`2_3 by A1,A3,A5,A14,Th5;
  then
A19: 1_F*(f`2_3-k`2_3)=h`2_3-l`2_3 by A17,Lm10;
  q=h by A8,XTUPLE_0:5;
  then [b,c,q,r]=[f,k,h,l] by A13,A7,A10,XTUPLE_0:5;
  hence thesis by A15,A19,A18,Th2;
end;

::              2. DEFINITION OF A FANO-DESARGUES SPACE

definition
  let IT be ParSp;
  attr IT is FanodesSp-like means
  :Def1:
  (ex a,b,c being Element of IT st not
a,b '||' a,c) & (for a,b,c,d being Element of IT holds b,c '||' a,d & a,b '||'
c,d & a,c '||' b,d implies a,b '||' a,c) & for a,b,c,p,q,r being Element of IT
  holds not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q & a,p '||' c,r & a,b
  '||' p,q & a,c '||' p,r implies b,c '||' q,r;
end;

registration
  cluster strict FanodesSp-like for ParSp;
  existence
  proof
    set FF = the Fanoian Field;
    reconsider FdSp=MPS(FF) as ParSp by Th1;
    1_FF+1_FF<>0.FF by VECTSP_1:def 19;
    then
A1: for a,b,c,d being Element of FdSp holds b,c '||' a,d & a,b '||' c,d &
    a,c '||' b,d implies a,b '||' a,c by Th7;
    ( ex a,b,c being Element of FdSp st not a,b '||' a,c)& for a,b,c,p,q,r
being Element of FdSp holds not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q
& a,p '||' c,r & a,b '||' p,q & a,c '||' p,r implies b, c '||' q,r by Th6,Th8;
    then FdSp is FanodesSp-like by A1,Def1;
    hence thesis;
  end;
end;

definition
  mode FanodesSp is FanodesSp-like ParSp;
end;

reserve FdSp for FanodesSp;
reserve a,b,c,d,p,q,r,s,o,x,y for Element of FdSp;

::           3. AXIOMS OF A FANO-DESARGUES PARALLELITY SPACE

theorem Th9:
  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,
PARSP_1:38;
  hence thesis;
end;

definition
  let FdSp,a,b,c;
  pred a,b,c is_collinear means
  :Def2:
  a,b '||' a,c;
end;

theorem Th10:
  a,b,c is_collinear implies a,c,b is_collinear & c,b,a
  is_collinear & b,a,c is_collinear & b,c,a is_collinear & c,a,b is_collinear
proof
  assume a,b,c is_collinear;
  then
A1: a,b '||' a,c by Def2;
  then
A2: b,a '||' b,c & b,c '||' b,a by PARSP_1:24;
A3: c,a '||' c,b by A1,PARSP_1:24;
  a,c '||' a,b & c,b '||' c,a by A1,PARSP_1:24;
  hence thesis by A2,A3,Def2;
end;

theorem Th11:
  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,PARSP_1:30;
  hence thesis by Def2;
end;

theorem Th12:
  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 PARSP_1:25;
  hence thesis by Def2;
end;

theorem Th13:
  a<>b & a,b,p is_collinear & a,b,q is_collinear & a,b,r
  is_collinear implies p,q,r is_collinear
proof
  assume that
A1: a<>b and
A2: a,b,p is_collinear and
A3: a,b,q is_collinear and
A4: a,b,r is_collinear;
A5: a,b '||' a,p by A2,Def2;
  a,b '||' a,r by A4,Def2;
  then
A6: a,b '||' p,r by A5,PARSP_1:35;
  a,b '||' a,q by A3,Def2;
  then a,b '||' p,q by A5,PARSP_1:35;
  then p,q '||' p,r by A1,A6,PARSP_1:def 12;
  hence thesis by Def2;
end;

theorem Th14:
  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 Th9;
  not p,q,r is_collinear by A1,Def2;
  hence thesis;
end;

theorem Th15:
  a,b,c is_collinear & a,b,d is_collinear implies a,b '||' c,d
proof
  assume a,b,c is_collinear & a,b,d is_collinear;
  then a,b '||' a,c & a,b '||' a,d by Def2;
  hence thesis by PARSP_1:35;
end;

theorem Th16:
  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;
A3: now
    assume that
A4: c <>d and
A5: a<>d;
    a,c '||' c,a & c <>a by A1,Th12,PARSP_1:25;
    then not c,d,a is_collinear by A1,A2,A4,Th11;
    then
A6: not d,c,a is_collinear by Th10;
A7: d,a '||' a,d by PARSP_1:25;
    a<>b & d,c '||' a,b by A1,A2,Th12,PARSP_1:23;
    hence thesis by A5,A6,A7,Th11;
  end;
  now
    assume a=d;
    then a,b '||' a,c by A2,PARSP_1:23;
    hence contradiction by A1,Def2;
  end;
  hence thesis by A1,A3;
end;

theorem Th17:
  not a,b,c is_collinear & a,b '||' c,d & c <>d implies not a,b,x
  is_collinear or not c,d,x is_collinear
proof
  assume
A1: ( not a,b,c is_collinear)& a,b '||' c,d & c <>d;
  now
    assume c,d,x is_collinear;
    then c,d '||' c,x by Def2;
    hence thesis by A1,Th16,PARSP_1:26;
  end;
  hence thesis;
end;

theorem
  not o,a,b is_collinear implies not o,a,x is_collinear or not o,b,x
  is_collinear or o=x
proof
  assume
A1: not o,a,b is_collinear;
  now
    assume that
A2: o,a,x is_collinear and
A3: o,b,x is_collinear;
    a,o,x is_collinear by A2,Th10;
    then
A4: a,o '||' a,x by Def2;
    b,o,x is_collinear by A3,Th10;
    then
A5: b,o '||' b,x by Def2;
    not a,b,o is_collinear by A1,Th10;
    then not a,b '||' a,o by Def2;
    hence thesis by A4,A5,PARSP_1:33;
  end;
  hence thesis;
end;

theorem
  o<>a & o<>b & o,a,b is_collinear & o,a,p is_collinear & o,b,q
  is_collinear implies a,b '||' p,q
proof
  assume that
A1: o<>a and
A2: o<>b and
A3: o,a,b is_collinear and
A4: o,a,p is_collinear and
A5: o,b,q is_collinear;
A6: now
A7: o,a '||' o,b by A3,Def2;
    o,a '||' o,p by A4,Def2;
    then
A8: o,b '||' o,p by A1,A7,PARSP_1:def 12;
    o,b '||' o,q by A5,Def2;
    then o,p '||' o,q by A2,A8,PARSP_1:def 12;
    then
A9: o,p '||' p,q by PARSP_1:24;
    o,b '||' a,b by A7,PARSP_1:24;
    then
A10: a,b '||' o,p by A2,A8,PARSP_1:def 12;
    assume o<>p;
    hence thesis by A10,A9,PARSP_1:26;
  end;
  now
    assume
A11: o=p;
    then p,a '||' p,b by A3,Def2;
    then
A12: a,b '||' p,b by PARSP_1:24;
    p,b '||' p,q by A5,A11,Def2;
    hence thesis by A2,A11,A12,PARSP_1:26;
  end;
  hence thesis by A6;
end;

theorem
  not a,b '||' c,d & a,b,p is_collinear & a,b,q is_collinear & c,d,p
  is_collinear & c,d,q is_collinear implies p=q
proof
  assume that
A1: not a,b '||' c,d and
A2: a,b,p is_collinear & a,b,q is_collinear and
A3: c,d,p is_collinear & c,d,q is_collinear;
  c,d '||' p,q by A3,Th15;
  then
A4: p,q '||' c,d by PARSP_1:23;
  a,b '||' p,q by A2,Th15;
  then p,q '||' a,b by PARSP_1:23;
  hence thesis by A1,A4,PARSP_1:def 12;
end;

theorem
  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 PARSP_1:24;
    then c,b '||' c,d by A1,A3,PARSP_1:def 12;
    then
A5: b,c '||' b,d by PARSP_1:24;
    assume
A6: b<>c;
    b,c '||' a,c by A4,PARSP_1:24;
    hence thesis by A6,A5,PARSP_1:def 12;
  end;
  hence thesis by A3;
end;

theorem
  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,PARSP_1:24,def 12;
    assume a<>c;
    hence thesis by A4,PARSP_1:def 12;
  end;
  hence thesis by A3;
end;

theorem
  not o,a,c is_collinear & o,a,b is_collinear & o,c,p is_collinear & o,c
  ,q is_collinear & a,c '||' b,p & a,c '||' b,q implies p=q
proof
  assume that
A1: ( not o,a,c is_collinear)& o,a,b is_collinear and
A2: o,c,p is_collinear & o,c,q is_collinear and
A3: a,c '||' b,p & a,c '||' b,q;
A4: o,c '||' o,p & o,c '||' o,q by A2,Def2;
  ( not o,a '||' o,c)& o,a '||' o,b by A1,Def2;
  hence thesis by A3,A4,PARSP_1:34;
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,PARSP_1:def 12;
  hence thesis by Def2;
end;

theorem
  a,b,c is_collinear & a,c,d is_collinear & a<>c implies b,c,d is_collinear
proof
  assume that
A1: a,b,c is_collinear and
A2: a,c,d is_collinear & a<>c;
A3: a,c,c is_collinear by Th12;
  a,c,b is_collinear by A1,Th10;
  hence thesis by A2,A3,Th13;
end;

definition
  let FdSp,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 Th26:
  parallelogram a,b,c,d implies a<>b & b<>c & c <>a & a<>d & b<>d & c <>d
proof
  assume
A1: parallelogram a,b,c,d;
A2: now
    assume a=d;
    then a,b '||' c,a by A1,Def3;
    then
A3: a,b '||' a,c by PARSP_1:23;
    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 PARSP_1:23;
    then
A5: a,b '||' a,c by PARSP_1:24;
    not a,b,c is_collinear by A1,Def3;
    hence contradiction by A5,Def2;
  end;
A6: now
    assume b=d;
    then a,b '||' c,b by A1,Def3;
    then b,a '||' b,c by PARSP_1:23;
    then
A7: a,b '||' a,c by PARSP_1:24;
    not a,b,c is_collinear by A1,Def3;
    hence contradiction by A7,Def2;
  end;
  not a,b,c is_collinear by A1,Def3;
  hence thesis by A2,A6,A4,Th12;
end;

theorem Th27:
  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 & a,c '||' c,a by PARSP_1:25;
  assume
A2: parallelogram a,b,c,d;
  then
A3: d<>b by Th26;
  a,c '||' b,d by A2,Def3;
  then
A4: a,c '||' d,b by PARSP_1:23;
  a,b '||' c,d by A2,Def3;
  then
A5: a,b '||' d,c by PARSP_1:23;
A6: ( not a,b,c is_collinear)& d<>c by A2,Def3,Th26;
A7: a,b '||' c,d & c <>a by A2,Def3,Th26;
  a,c '||' b,d & b<>a by A2,Def3,Th26;
  hence thesis by A1,A7,A5,A4,A6,A3,Th11;
end;

theorem Th28:
  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 & not a,c,b
  is_collinear & not b,a,c is_collinear & not b,c,a is_collinear & not c,a,b
  is_collinear & not c,b,a is_collinear & not b,d,a is_collinear & not a,b,d
  is_collinear & not a,d,b is_collinear & not d,a,b is_collinear & not d,b,a
  is_collinear & not c,a,d is_collinear & not a,c,d is_collinear & not a,d,c
  is_collinear & not d,a,c is_collinear & not d,c,a is_collinear & not d,b,c
  is_collinear & not b,c,d is_collinear & not b,d,c is_collinear & not c,b,d
  is_collinear & not c,d,b is_collinear
proof
  assume
A1: parallelogram a,b,c,d;
  then
A2: ( not c,d,a is_collinear)& not d,c,b is_collinear by Th27;
  ( not a,b,c is_collinear)& not b,a,d is_collinear by A1,Th27;
  hence thesis by A2,Th10;
end;

theorem Th29:
  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 Th26;
  ( not a,b,c is_collinear)& a,b '||' c,d by A1,Def3;
  hence thesis by A2,Th17;
end;

theorem Th30:
  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,Th28;
  hence thesis by A2,Def3;
end;

theorem Th31:
  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 PARSP_1:23;
  a,c '||' b,d by A1,Def3;
  then
A3: c,a '||' d,b by PARSP_1:23;
  not c,d,a is_collinear by A1,Th28;
  hence thesis by A2,A3,Def3;
end;

theorem Th32:
  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 PARSP_1:23;
  a,c '||' b,d by A1,Def3;
  then
A3: b,d '||' a,c by PARSP_1:23;
  not b,a,d is_collinear by A1,Th28;
  hence thesis by A2,A3,Def3;
end;

theorem Th33:
  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 & parallelogram d,c,b,a
proof
  assume
A1: parallelogram a,b,c,d;
  then parallelogram c,d,a,b by Th31;
  then
A2: parallelogram c,a,d,b by Th30;
  parallelogram b,a,d,c by A1,Th32;
  hence thesis by A1,A2,Th30,Th31;
end;

theorem Th34:
  not a,b,c is_collinear implies ex d st parallelogram a,b,c,d
proof
  consider d such that
A1: a,b '||' c,d & a,c '||' b,d by PARSP_1:def 12;
  assume not a,b,c is_collinear;
  then parallelogram a,b,c,d by A1,Def3;
  hence thesis;
end;

theorem Th35:
  parallelogram a,b,c,p & parallelogram a,b,c,q implies p=q
proof
  assume that
A1: parallelogram a,b,c,p and
A2: parallelogram a,b,c,q;
  a,b '||'c,p by A1,Def3;
  then
A3: b,c '||' c,b & b,a '||' c,p by PARSP_1:23,25;
  a,b '||' c,q by A2,Def3;
  then
A4: b,a '||' c,q by PARSP_1:23;
  a,c '||' b,p by A1,Def3;
  then
A5: c,a '||' b,p by PARSP_1:23;
  a,c '||' b,q by A2,Def3;
  then
A6: c,a '||' b,q by PARSP_1:23;
  not b,c,a is_collinear by A1,Th28;
  then not b,c '||' b,a by Def2;
  hence thesis by A3,A4,A5,A6,PARSP_1:34;
end;

theorem Th36:
  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;
  then not b,c '||' a,d by A2,Def1;
  hence thesis by PARSP_1:19;
end;

theorem Th37:
  parallelogram a,b,c,d implies not parallelogram a,b,d,c
proof
  assume parallelogram a,b,c,d;
  then not a,d '||' b,c by Th36;
  hence thesis by Def3;
end;

theorem Th38:
  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 Th14;
  consider q such that
A2: parallelogram a,b,p,q by A1,Th34;
  not p,q,b is_collinear by A2,Th28;
  then consider c such that
A3: parallelogram p,q,b,c by Th34;
A4: p,q '||' b,c by A3,Def3;
  p<>q & a,b '||' p,q by A2,Def3,Th26;
  then a,b '||' b,c by A4,PARSP_1:26;
  then b,a '||' b,c by PARSP_1:23;
  then b,a,c is_collinear by Def2;
  then
A5: a,b,c is_collinear by Th10;
A6: not a,q '||' b,p by A2,Th36;
  p,b '||' q,c by A3,Def3;
  then
A7: a<>c by A6,PARSP_1:23;
  b<>c by A3,Th26;
  hence thesis by A7,A5;
end;

theorem Th39:
  parallelogram a,p,b,q & parallelogram a,p,c,r implies b,c '||' q ,r
proof
  assume that
A1: parallelogram a,p,b,q and
A2: parallelogram a,p,c,r;
A3: a,p '||' c,r & a,c '||' p,r by A2,Def3;
  not a,p,c is_collinear by A2,Def3;
  then
A4: not a,p '||' a,c by Def2;
  not a,p,b is_collinear by A1,Def3;
  then
A5: not a,p '||' a,b by Def2;
  a,p '||' b,q & a,b '||' p,q by A1,Def3;
  hence thesis by A5,A4,A3,Def1;
end;

theorem Th40:
  not b,q,c is_collinear & parallelogram a,p,b,q & parallelogram a
  ,p,c,r implies parallelogram b,q,c,r
proof
  assume that
A1: not b,q,c is_collinear and
A2: parallelogram a,p,b,q and
A3: parallelogram a,p,c,r;
A4: a,p '||' c,r by A3,Def3;
  a<>p & a,p '||' b,q by A2,Def3,Th26;
  then
A5: b,q '||' c,r by A4,PARSP_1:def 12;
  b,c '||' q,r by A2,A3,Th39;
  hence thesis by A1,A5,Def3;
end;

theorem Th41:
  a,b,c is_collinear & b<>c & parallelogram a,p,b,q &
  parallelogram a,p,c,r implies parallelogram b,q,c,r
proof
  assume that
A1: a,b,c is_collinear and
A2: b<>c and
A3: parallelogram a,p,b,q and
A4: parallelogram a,p,c,r;
A5: b<>q by A3,Th26;
  a,b '||'a,c by A1,Def2;
  then
A6: a,b '||' b,c by PARSP_1:24;
  ( not a,p,b is_collinear)& a,p '||' b,q by A3,Def3;
  hence thesis by A2,A3,A4,A5,A6,Th11,Th40;
end;

theorem Th42:
  parallelogram a,p,b,q & parallelogram a,p,c,r & parallelogram b,
  q,d,s implies c,d '||' r,s
proof
  assume that
A1: parallelogram a,p,b,q and
A2: parallelogram a,p,c,r and
A3: parallelogram b,q,d,s;
A4: now
    assume
A5: not a,p,d is_collinear;
    parallelogram b,q,a,p by A1,Th33;
    then parallelogram a,p,d,s by A3,A5,Th40;
    hence thesis by A2,Th39;
  end;
A6: now
A7: a<>p by A1,Th26;
A8: ( not a,p,b is_collinear)& a,p '||' a,p by A1,Th28,PARSP_1:25;
    assume that
A9: b,q,c is_collinear and
A10: a,p,d is_collinear;
    a<>b by A1,Th26;
    then consider x such that
A11: a,b,x is_collinear and
A12: x<>a and
A13: x<>b by Th38;
    a,b '||' a,x by A11,Def2;
    then consider y such that
A14: parallelogram a,p,x,y by A12,A8,A7,Th11,Th34;
A15: not x,y,d is_collinear by A10,A14,Th29;
    parallelogram b,q,x,y by A1,A11,A13,A14,Th41;
    then
A16: parallelogram x,y,d,s by A3,A15,Th40;
    not x,y,c is_collinear by A1,A9,A11,A13,A14,Th29,Th41;
    then parallelogram x,y,c,r by A2,A14,Th40;
    hence thesis by A16,Th39;
  end;
  now
    assume not b,q,c is_collinear;
    then parallelogram b,q,c,r by A1,A2,Th40;
    hence thesis by A3,Th39;
  end;
  hence thesis by A4,A6;
end;

theorem Th43:
  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 Th14;
  ex d st parallelogram a,b,c,d by A1,Th34;
  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 Th14;
  not b,a,d is_collinear by A1,Th10;
  then consider c such that
A2: parallelogram b,a,d,c by Th34;
  parallelogram a,b,c,d by A2,Th33;
  hence thesis;
end;

definition
  let FdSp,a,b,r,s;
  pred a,b congr 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 Th45:
  a,a congr b,c implies b=c
proof
  assume a,a congr 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 Th26;
end;

theorem
  a,b congr c,c implies a=b
proof
  assume a,b congr 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 Th26;
end;

theorem
  a,b congr b,a implies a=b
proof
  assume
A1: a,b congr 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 Th37;
  end;
  hence thesis;
end;

theorem Th48:
  a,b congr c,d implies a,b '||' c,d
proof
  assume
A1: a,b congr 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,Th26;
    hence thesis by A4,PARSP_1:def 12;
  end;
  hence thesis by PARSP_1:20;
end;

theorem Th49:
  a,b congr c,d implies a,c '||' b,d
proof
  assume
A1: a,b congr c,d;
A2: now
    assume
A3: a=b;
    then c =d by A1,Th45;
    hence thesis by A3,PARSP_1:25;
  end;
  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 Th39;
  end;
  hence thesis by A2;
end;

theorem Th50:
  a,b congr c,d & not a,b,c is_collinear implies parallelogram a,b ,c,d
proof
  assume that
A1: a,b congr c,d and
A2: not a,b,c is_collinear;
  a,b '||' c,d & a,c '||' b,d by A1,Th48,Th49;
  hence thesis by A2,Def3;
end;

theorem Th51:
  parallelogram a,b,c,d implies a,b congr c,d
proof
A1: a,b '||' a,b by PARSP_1:25;
  assume
A2: parallelogram a,b,c,d;
  then
A3: ( not a,c,b is_collinear)& a<>b by Th26,Th28;
  a<>c by A2,Th26;
  then consider p such that
A4: a,c,p is_collinear and
A5: a<>p and
A6: c <>p by Th38;
  a,c '||' a,p by A4,Def2;
  then consider q such that
A7: parallelogram a,p,b,q by A5,A1,A3,Th11,Th34;
  parallelogram a,b,p,q by A7,Th33;
  then parallelogram c,d,p,q by A2,A4,A6,Th41;
  then
A8: parallelogram p,q,c,d by Th33;
  parallelogram p,q,a,b by A7,Th33;
  hence thesis by A8,Def4;
end;

theorem Th52:
  a,b congr c,d & a,b,c is_collinear & parallelogram r,s,a,b
  implies parallelogram r,s,c,d
proof
  assume that
A1: a,b congr c,d and
A2: a,b,c is_collinear and
A3: parallelogram r,s,a,b;
  now
    assume
A4: a<>b;
    then consider p,q such that
A5: parallelogram p,q,a,b and
A6: parallelogram p,q,c,d by A1,Def4;
    r,s '||' a,b & a,b '||' c,d by A1,A3,Def3,Th48;
    then
A7: r,s '||' c,d by A4,PARSP_1:26;
A8: parallelogram a,b,r,s by A3,Th33;
    parallelogram a,b,p,q by A5,Th33;
    then
A9: r,c '||' s,d by A6,A8,Th42;
    not r,s,c is_collinear by A2,A3,Th29;
    hence thesis by A7,A9,Def3;
  end;
  hence thesis by A3,Th26;
end;

theorem
  a,b congr c,x & a,b congr c,y implies x=y
proof
  assume that
A1: a,b congr c,x and
A2: a,b congr 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,Th50;
    hence thesis by Th35;
  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,Th43;
    parallelogram p,q,a,b by A8,Th33;
    then parallelogram p,q,c,x & parallelogram p,q,c,y by A1,A2,A7,Th52;
    hence thesis by Th35;
  end;
  now
    assume
A9: a=b;
    then c =x by A1,Th45;
    hence thesis by A2,A9,Th45;
  end;
  hence thesis by A5,A3;
end;

theorem
  ex d st a,b congr c,d
proof
A1: now
    assume a=b;
    then a,b congr 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,Th43;
    not p,q,c is_collinear by A4,A5,Th29;
    then consider d such that
A6: parallelogram p,q,c,d by Th34;
    parallelogram p,q,a,b by A5,Th33;
    then a,b congr 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,Th34;
    hence thesis by Th51;
  end;
  hence thesis by A1,A2;
end;

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

theorem Th56:
  r,s congr a,b & r,s congr c,d implies a,b congr c,d
proof
  assume that
A1: r,s congr a,b and
A2: r,s congr 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,Th50;
    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,Th52;
    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,Th52;
    hence thesis by A14,Def4;
  end;
  now
    assume r=s;
    then a=b & c =d by A1,A2,Th45;
    hence thesis by Def4;
  end;
  hence thesis by A10,A5,A3;
end;

theorem
  a,b congr c,d implies c,d congr a,b
proof
  assume
A1: a,b congr c,d;
  a,b congr a,b by Th55;
  hence thesis by A1,Th56;
end;

theorem
  a,b congr c,d implies b,a congr d,c
proof
  assume
A1: a,b congr 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,Th33;
    hence thesis by Def4;
  end;
  now
    assume
A4: a=b;
    then c =d by A1,Th45;
    hence thesis by A4,Def4;
  end;
  hence thesis by A2;
end;