The Mizar article:

Shear Theorems and Their Role in Affine Geometry

by
Jolanta Swierzynska, and
Bogdan Swierzynski

Received April 19, 1991

Copyright (c) 1991 Association of Mizar Users

MML identifier: CONMETR1
[ MML identifier index ]


environ

 vocabulary DIRAF, ANALOAF, AFF_1, AFF_2, ANALMETR, CONMETR, CONAFFM, CONMETR1;
 notation SUBSET_1, STRUCT_0, ANALOAF, DIRAF, AFF_1, ANALMETR, AFF_2, CONAFFM,
      CONMETR;
 constructors AFF_1, AFF_2, CONAFFM, CONMETR, XBOOLE_0;
 clusters ANALMETR, ZFMISC_1, XBOOLE_0;
 requirements SUBSET;
 theorems AFF_1, AFF_2, ANALMETR, CONAFFM, CONMETR, TRANSLAC, DIRAF;

begin
reserve X for AffinPlane;
reserve o,a,a1,a2,a3,a4,b,b1,b2,b3,b4,c,c1,c2,d,d1,d2,
        d3,d4,d5,e1,e2,x,y,z for Element of X;
reserve Y,Z,M,N,A,K,C for Subset of X;

definition let X; attr X is satisfying_minor_Scherungssatz means
:Def1: for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M // N &
         a1 in M & a3 in M & b1 in M & b3 in M & a2 in N &
         a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M &
         not b2 in M & not b4 in M & not a1 in N & not a3 in N &
         not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1
         & a1,a4 // b1,b4 holds a3,a4 // b3,b4;
  synonym X satisfies_minor_SCH;
end;

definition let X; attr X is satisfying_major_Scherungssatz means
:Def2: for o,a1,a2,a3,a4,b1,b2,b3,b4,M,N st M is_line &
         N is_line & o in M & o in N & a1 in M & a3 in M & b1 in M &
         b3 in M & a2 in N &
         a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M &
         not b2 in M & not b4 in M & not a1 in N & not a3 in N &
         not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1
         & a1,a4 // b1,b4 holds a3,a4 // b3,b4;
  synonym X satisfies_major_SCH;
end;

definition let X; attr X is satisfying_Scherungssatz means
:Def3: for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M is_line &
         N is_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N &
         a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M &
         not b2 in M & not b4 in M & not a1 in N & not a3 in N &
         not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1
         & a1,a4 // b1,b4 holds a3,a4 // b3,b4;
  synonym X satisfies_SCH;
end;

definition let X; attr X is satisfying_indirect_Scherungssatz means
:Def4: for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M is_line &
         N is_line & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N &
         a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M &
         not b1 in M & not b3 in M & not a1 in N & not a3 in N &
         not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1
         & a1,a4 // b1,b4 holds a3,a4 // b3,b4;
  synonym X satisfies_SCH*;
end;

definition let X; attr X is satisfying_minor_indirect_Scherungssatz means
:Def5: for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M // N
          & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N &
         a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M &
         not b1 in M & not b3 in M & not a1 in N & not a3 in N &
         not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1
         & a1,a4 // b1,b4 holds a3,a4 // b3,b4;
  synonym X satisfies_minor_SCH*;
end;

definition let X; attr X is satisfying_major_indirect_Scherungssatz means
:Def6: for o,a1,a2,a3,a4,b1,b2,b3,b4,M,N st M is_line & N is_line &
         o in M & o in N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N &
         a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M
         & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N
         & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
         a3,a4 // b3,b4;
  synonym X satisfies_major_SCH*;
end;

theorem Th1:
    X satisfies_SCH* iff (X satisfies_minor_SCH* & X satisfies_major_SCH*)
proof
A1:X satisfies_SCH* implies X satisfies_minor_SCH* & X satisfies_major_SCH*
 proof
  A2:X satisfies_SCH* implies X satisfies_minor_SCH*
   proof
    assume A3:X satisfies_SCH*;
      now let a1,a2,a3,a4,b1,b2,b3,b4,M,N;
    assume A4:M // N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N &
           a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M &
           not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N
           & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4;
    then M is_line & N is_line by AFF_1:50;
    hence a3,a4 // b3,b4 by A3,A4,Def4;end;
   hence thesis by Def5;end;
    X satisfies_SCH* implies X satisfies_major_SCH*
   proof
    assume X satisfies_SCH*;
    then for o,a1,a2,a3,a4,b1,b2,b3,b4,M,N holds
 M is_line & N is_line & o in M & o in N & a1 in M & a3 in M &
           b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N &
           not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N
           & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 &
           a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 by Def4
;
   hence thesis by Def6;end;
 hence thesis by A2;end;
  X satisfies_minor_SCH* & X satisfies_major_SCH* implies X satisfies_SCH*
 proof
  assume that A5:X satisfies_minor_SCH* and A6:X satisfies_major_SCH*;
    now let a1,a2,a3,a4,b1,b2,b3,b4,M,N;
  assume A7:M is_line & N is_line & a1 in M & a3 in M & b2 in M & b4 in M &
         a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M &
         not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N &
         not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4;

    now assume not M // N;
   then ex o st o in M & o in N by A7,AFF_1:72;
  hence a3,a4 // b3,b4 by A6,A7,Def6;end;
  hence a3,a4 // b3,b4 by A5,A7,Def5;end;
 hence thesis by Def4;end;
hence thesis by A1;end;

theorem
   Th2:X satisfies_SCH iff (X satisfies_minor_SCH & X satisfies_major_SCH)
proof
A1:X satisfies_SCH implies (X satisfies_minor_SCH & X satisfies_major_SCH)
proof
A2:X satisfies_SCH implies X satisfies_minor_SCH
proof
assume A3:X satisfies_SCH;
  now let a1,a2,a3,a4,b1,b2,b3,b4,M,N;
assume A4: M // N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N &
         a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M &
         not b2 in M & not b4 in M & not a1 in N & not a3 in N &
         not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1
         & a1,a4 // b1,b4;
then M is_line & N is_line by AFF_1:50;
hence a3,a4 // b3,b4 by A3,A4,Def3;end;
hence thesis by Def1;end;
  X satisfies_SCH implies X satisfies_major_SCH
proof
assume X satisfies_SCH;
then for o,a1,a2,a3,a4,b1,b2,b3,b4,M,N holds
 M is_line & N is_line & o in M & o in N & a1 in M & a3 in M &
         b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N &
         not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N
         & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2
         & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 by Def3;
hence thesis by Def2;end;
hence thesis by A2;end;
  (X satisfies_minor_SCH & X satisfies_major_SCH) implies X satisfies_SCH
proof
assume A5:X satisfies_minor_SCH & X satisfies_major_SCH;
  now let a1,a2,a3,a4,b1,b2,b3,b4,M,N;
assume A6:M is_line & N is_line & a1 in M & a3 in M & b1 in M & b3 in M
         & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M
         & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N
         & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4;

  now assume not M // N;
then ex o st o in M & o in N by A6,AFF_1:72;
hence a3,a4 // b3,b4 by A5,A6,Def2;end;
hence a3,a4 // b3,b4 by A5,A6,Def1;end;
hence thesis by Def3;end;
hence thesis by A1;end;

theorem Th3:
      X satisfies_minor_SCH* implies X satisfies_minor_SCH
proof
 assume A1:X satisfies_minor_SCH*;
   now let a1,a2,a3,a4,b1,b2,b3,b4,M,N;
 assume A2: M // N & a1 in M & a3 in M & b1 in M & b3 in M &
        a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M &
        not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N &
        not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4;
 then A3:M is_line & N is_line by AFF_1:50;
  then consider d1 such that A4:a2<>d1 & d1 in N by AFF_1:32;
    ex d2 st d2 in M & a2,a1 // d2,d1
   proof
    consider e1 such that A5:a1<>e1 & e1 in M by A3,AFF_1:32;
    consider e2 such that A6:a2,a1 // d1,e2 & d1<>e2 by DIRAF:47;
      not a1,e1 // d1,e2 proof assume a1,e1 // d1,e2; then a1,e1 // a2,a1 by A6
,AFF_1:14; then a1,e1 // a1,a2 by AFF_1:13; then LIN a1,e1,a2 by AFF_1:def 1;
    hence contradiction by A2,A3,A5,AFF_1:39;end;
    then consider d2 such that A7:LIN a1,e1,d2 & LIN
 d1,e2,d2 by AFF_1:74;take d2;
      d1,e2 // d1,d2 by A7,AFF_1:def 1; then a2,a1 // d1,d2 by A6,AFF_1:14;
   hence thesis by A2,A3,A5,A7,AFF_1:13,39;end;
  then consider d2 such that A8:d2 in M & a2,a1 // d2,d1;
    ex d3 st d3 in N & a3,a2 // d3,d2 proof
    consider e1 such that A9:a2<>e1 & e1 in N by A3,AFF_1:32;
    consider e2 such that A10:a3,a2 // d2,e2 & d2<>e2 by DIRAF:47;
      not a2,e1 // d2,e2 proof assume a2,e1 // d2,e2; then a2,e1 // a3,a2 by
A10,AFF_1:14; then a2,e1 // a2,a3 by AFF_1:13; then LIN a2,e1,a3 by AFF_1:def 1
;
     hence contradiction by A2,A3,A9,AFF_1:39;end;
    then consider d3 such that A11:LIN a2,e1,d3 & LIN
 d2,e2,d3 by AFF_1:74;take d3;
      d2,e2 // d2,d3 by A11,AFF_1:def 1; then a3,a2 // d2,d3 by A10,AFF_1:14;
hence thesis by A2,A3,A9,A11,AFF_1:13,39;end;
  then consider d3 such that A12:d3 in N & a3,a2 // d3,d2;
    ex d4 st d4 in M & a1,a4 // d1,d4
   proof
    consider e1 such that A13:a1<>e1 & e1 in M by A3,AFF_1:32;
    consider e2 such that A14:a1,a4 // d1,e2 & d1<>e2 by DIRAF:47;
      not a1,e1 // d1,e2 proof assume a1,e1 // d1,e2; then a1,e1 // a1,a4 by
A14,AFF_1:14; then LIN a1,e1,a4 by AFF_1:def 1;
    hence contradiction by A2,A3,A13,AFF_1:39;end;
    then consider d4 such that A15:LIN a1,e1,d4 & LIN
 d1,e2,d4 by AFF_1:74;take d4;
      d1,e2 // d1,d4 by A15,AFF_1:def 1;
   hence thesis by A2,A3,A13,A14,A15,AFF_1:14,39;end;
  then consider d4 such that A16:d4 in M & a1,a4 // d1,d4;
  A17:not d1 in M & not d3 in M & not d2 in N & not d4 in N
   by A2,A4,A8,A12,A16,AFF_1:59;
  then A18:a3,a4 // d3,d4 by A1,A2,A4,A8,A12,A16,Def5;
  A19:b2,b1 // d2,d1 by A2,A8,AFF_1:14;
  A20:b3,b2 // d3,d2 by A2,A12,AFF_1:14;
    b1,b4 // d1,d4 by A2,A16,AFF_1:14;
  then b3,b4 // d3,d4 by A1,A2,A4,A8,A12,A16,A17,A19,A20,Def5;
 hence a3,a4 // b3,b4 by A16,A17,A18,AFF_1:14;end;
hence thesis by Def1;end;

 theorem Th4:
       X satisfies_major_SCH* implies X satisfies_major_SCH
proof
 assume A1:X satisfies_major_SCH*;
   now let o,a1,a2,a3,a4,b1,b2,b3,b4,M,N;
 assume A2: M is_line & N is_line & o in M & o in N & a1 in M & a3 in M &
        b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M
        & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N
        & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 &
        a1,a4 // b1,b4;
 then A3:not M // N by AFF_1:59;
  A4:M // M & N // N by A2,AFF_1:55;
  A5:now assume A6:a1=a3 or a2=a4;
   A7:now assume A8:a1=a3;
    A9:not LIN o,b2,b1 by A2,AFF_1:39;
      o,b1 // o,b3 by A2,A4,AFF_1:53; then A10:LIN o,b1,b3 by AFF_1:def 1;
      b2,b1 // b2,b3 proof a2,a1 // b2,b3 by A2,A8,AFF_1:13;
    hence thesis by A2,AFF_1:14;end;
    hence a3,a4 // b3,b4 by A2,A8,A9,A10,AFF_1:23;end;
     now assume A11:a2=a4;
    A12:not LIN o,b1,b2 by A2,AFF_1:39;
      o,b2 // o,b4 by A2,A4,AFF_1:53; then A13:LIN o,b2,b4 by AFF_1:def 1;
      b1,b2 // b1,b4 proof a1,a4 // b1,b2 by A2,A11,AFF_1:13;
    hence thesis by A2,AFF_1:14;end;
   hence a3,a4 // b3,b4 by A2,A11,A12,A13,AFF_1:23;end;
  hence a3,a4 // b3,b4 by A6,A7;end;
    now assume A14:a1<>a3 & a2<>a4;
  consider d1 such that A15:o<>d1 & d1 in N by A2;
    ex d2 st d2 in M & a2,a1 // d2,d1 proof
    consider e1 such that A16:o<>e1 & e1 in M by A2;
    consider e2 such that A17:a2,a1 // d1,e2 & d1<>e2 by DIRAF:47;
      not o,e1 // d1,e2 proof assume o,e1 // d1,e2; then A18:o,e1 // a2,a1 by
A17,AFF_1:14; o,e1 // a1,a3 by A2,A4,A16,AFF_1:53; then a1,a3 // a2,a1 by A16,
A18,AFF_1:14; then a1,a3 // a1,a2 by AFF_1:13; then LIN a1,a3,a2
    by AFF_1:def 1;
    hence contradiction by A2,A14,AFF_1:39;end;
    then consider d2 such that A19:LIN o,e1,d2 & LIN
 d1,e2,d2 by AFF_1:74;take d2;
      d1,e2 // d1,d2 by A19,AFF_1:def 1; then a2,a1 // d1,d2 by A17,AFF_1:14;
hence thesis by A2,A16,A19,AFF_1:13,39;end;
  then consider d2 such that A20:d2 in M & a2,a1 // d2,d1;
    ex d3 st d3 in N & a3,a2 // d3,d2 proof
    consider e1 such that A21:o<>e1 & e1 in N by A2;
    consider e2 such that A22:a3,a2 // d2,e2 & d2<>e2 by DIRAF:47;
      not o,e1 // d2,e2 proof assume o,e1 // d2,e2; then A23:o,e1 // a3,a2 by
A22,AFF_1:14; o,e1 // a2,a4 by A2,A4,A21,AFF_1:53; then a2,a4 // a3,a2
     by A21,A23,AFF_1:14; then a2,a4 // a2,a3 by AFF_1:13; then LIN a2,a4,a3
by AFF_1:def 1;hence contradiction by A2,A14,AFF_1:39;end;
    then consider d3 such that A24:LIN o,e1,d3 & LIN
 d2,e2,d3 by AFF_1:74;take d3;
      d2,e2 // d2,d3 by A24,AFF_1:def 1; then a3,a2 // d2,d3 by A22,AFF_1:14;
hence thesis by A2,A21,A24,AFF_1:13,39;end;
  then consider d3 such that A25:d3 in N & a3,a2 // d3,d2;
    ex d4 st d4 in M & a1,a4 // d1,d4 proof
    consider e1 such that A26:o<>e1 & e1 in M by A2;
    consider e2 such that A27:a1,a4 // d1,e2 & d1<>e2 by DIRAF:47;
      not o,e1 // d1,e2 proof assume o,e1 // d1,e2; then A28:o,e1 // a1,a4 by
A27,AFF_1:14; o,e1 // a1,a3 by A2,A4,A26,AFF_1:53; then a1,a3 // a1,a4 by A26,
A28,AFF_1:14; then LIN a1,a3,a4 by AFF_1:def 1;
    hence contradiction by A2,A14,AFF_1:39;end;
    then consider d4 such that A29:LIN o,e1,d4 & LIN
 d1,e2,d4 by AFF_1:74;take d4;
   d1,e2 // d1,d4 by A29,AFF_1:def 1;
hence thesis by A2,A26,A27,A29,AFF_1:14,39;end;
  then consider d4 such that A30:d4 in M & a1,a4 // d1,d4;
  A31:d2<>o & d3<>o & d4<>o proof assume A32:not thesis;
   A33:now assume A34: d2=o; o,d1 // a2,a4 by A2,A4,A15,AFF_1:53; then a2,a4
// a2,a1 by A15,A20,A34,AFF_1:14; then LIN a2,a4,a1 by AFF_1:def 1;hence
 contradiction by A2,A14,AFF_1:39;end;

   A35:now assume A36: d3=o; o,d2 // a3,a1 by A2,A4,A20,AFF_1:53; then a3,a1
// a3,a2 by A25,A33,A36,AFF_1:14; then LIN a3,a1,a2 by AFF_1:def 1;hence
 contradiction by A2,A14,AFF_1:39;end;
     now assume A37: d4=o; d1,o // a2,a4 by A2,A4,A15,AFF_1:53; then a1,a4
//
a2,a4 by A15,A30,A37,AFF_1:14; then a4,a2 // a4,a1 by AFF_1:13; then LIN a4,
a2,a1 by AFF_1:def 1;
   hence contradiction by A2,A14,AFF_1:39;end;
  hence contradiction by A32,A33,A35;end;
  A38:not d1 in M & not d3 in M & not d2 in N & not d4 in N
   proof assume not thesis; then A39:o,d1 // M or o,d3 // M or o,d2 // N or
    o,d4 // N by A2,AFF_1:66; o,d1 // N & o,d3 // N & o,d2 // M & o,d4 // M
    by A2,A15,A20,A25,A30,AFF_1:66;
   hence contradiction by A3,A15,A31,A39,AFF_1:67;end;
  then A40:a3,a4 // d3,d4 by A1,A2,A15,A20,A25,A30,Def6;
  A41:d1<>d2 & d2<>d3 & d3<>d4 & d4<>d1 proof assume not thesis;
   then A42:o,d1 // M or o,d3 // M by A2,A20,A30,AFF_1:66; o,d1 // N & o,d3
//
N by A2,A15,A25,AFF_1:66;
  hence contradiction by A3,A15,A31,A42,AFF_1:67;end;
  A43:b2,b1 // d2,d1 by A2,A20,AFF_1:14;
  A44:b3,b2 // d3,d2 by A2,A25,AFF_1:14;
    b1,b4 // d1,d4 by A2,A30,AFF_1:14;
  then b3,b4 // d3,d4 by A1,A2,A15,A20,A25,A30,A38,A43,A44,Def6;
 hence a3,a4 // b3,b4 by A40,A41,AFF_1:14;end;
 hence a3,a4 // b3,b4 by A5;end;
hence thesis by Def2;end;

theorem
         X satisfies_SCH* implies X satisfies_SCH
proof
 assume X satisfies_SCH*;
 then X satisfies_minor_SCH* & X satisfies_major_SCH* by Th1;
 then X satisfies_minor_SCH & X satisfies_major_SCH by Th3,Th4;
hence thesis by Th2;end;

theorem Th6:
        X satisfies_des implies X satisfies_minor_SCH
proof
assume A1:X satisfies_des;
  now let a1,a2,a3,a4,b1,b2,b3,b4,M,N;
assume A2:M // N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N
       & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M &
       not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N &
       a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4;
then A3:M is_line & N is_line by AFF_1:50;
then A4:M // M & N // N by AFF_1:55;
A5:now assume A6:a1=a3 or a2=a4;
 A7:now assume A8:a1=a3;
    b1=b3 proof assume A9:b1<>b3;A10:LIN b2,b1,b3 proof
      LIN a2,a1,a3 by A8,AFF_1:16; then a2,a1 // a2,a3
    by AFF_1:def 1; then b2,b1 // a2,a3 by A2,AFF_1:14; then b2,b1 // a3,a2
by AFF_1:13; then b2,b1 // b3,b2 by A2,AFF_1:14; then b2,b1 // b2,b3 by AFF_1:
13;hence thesis by AFF_1:def 1;end;
     b1,b3 // N by A2,AFF_1:54;
  hence contradiction by A2,A9,A10,AFF_1:60;end;
 hence a3,a4 // b3,b4 by A2,A8;end;
   now assume A11:a2=a4; N // M by A2; then A12:b2,b4 // M by A2,AFF_1:54;
    LIN a1,a4,a2 by A11,AFF_1:16; then a1,a4 // a1,a2
  by AFF_1:def 1; then b1,b4 // a1,a2 by A2,AFF_1:14; then b1,b4 // a2,a1 by
AFF_1:13; then b1,b4 // b2,b1 by A2,AFF_1:14; then b1,b2 // b1,b4 by AFF_1:13
;
  then LIN b1,b2,b4 by AFF_1:def 1;
 hence a3,a4 // b3,b4 by A2,A11,A12,AFF_1:60;end;
hence a3,a4 // b3,b4 by A6,A7;end;
  now assume A13:a1<>a3 & a2<>a4;
 A14:now assume A15:not ex x,y,z st LIN x,y,z & x<>y & x<>z & y<>z;
    a1,a3 // a1,b1 by A2,A4,AFF_1:53; then A16: LIN a1,a3,b1 by AFF_1:def 1;
  A17:now assume A18:a1=b1;
   then A19:LIN a1,a4,b4 by A2,AFF_1:def 1;A20:N // M by A2;
   then a4,b4 // M by A2,AFF_1:54; then A21:a4=b4 by A2,A19,AFF_1:60;
  a1,a2 // a1,b2 by A2,A18,AFF_1:13; then A22:LIN a1,a2,b2 by AFF_1:def 1;
     a2,b2 // M by A2,A20,AFF_1:54; then a2=b2 by A2,A22,AFF_1:60;
   then a2,a3 // a2,b3 by A2,AFF_1:13; then A23:LIN a2,a3,b3 by AFF_1:def 1;
     a3,b3 // N by A2,AFF_1:54; then a3=b3 by A2,A23,AFF_1:60;
  hence a3,a4 // b3,b4 by A21,AFF_1:11;end;
    now assume A24:a3=b1;
     a2,a4 // a2,b2 by A2,A4,AFF_1:53; then A25: LIN a2,a4,b2 by AFF_1:def 1;
   A26:now assume A27:a4=b2; a1,a3 // a1,b3 by A2,A4,AFF_1:53; then A28: LIN
a1,a3,b3
    by AFF_1:def 1;
      a3<>b3 proof assume a3=b3;
     then A29:LIN a3,a2,b2 by A2,AFF_1:def 1; N // M by A2; then a2,b2 // M
by A2,AFF_1:54;
    hence contradiction by A2,A13,A27,A29,AFF_1:60;end;
    then A30:a1=b3 by A13,A15,A28; a2,a4 // a2,b4 by A2,A4,AFF_1:53; then A31
:
 LIN a2,a4,b4 by AFF_1:def 1;
      a4<>b4 proof assume a4=b4; then a4,a1 // a4,b1 by A2,AFF_1:13;
     then A32:LIN a4,a1,b1 by AFF_1:def 1; a1,b1 // N by A2,AFF_1:54;
hence contradiction by A2,A13,A24,A32,AFF_1:60;end;
    then A33:a2=b4 by A13,A15,A31;
      a3,a4 // b2,b1 by A24,A27,AFF_1:11;
    then a3,a4 // a2,a1 by A2,AFF_1:14;
   hence a3,a4 // b3,b4 by A30,A33,AFF_1:13;end;
     now assume a2=b2; then A34:LIN a2,a1,b1 by A2,AFF_1:def 1; a1,b1 // N
by A2,AFF_1:54;
   hence a3,a4 // b3,b4 by A2,A17,A34,AFF_1:60;end;
  hence a3,a4 // b3,b4 by A13,A15,A25,A26;end;
 hence a3,a4 // b3,b4 by A13,A15,A16,A17;end;
   now assume ex x,y,z st LIN x,y,z & x<>y & x<>z & y<>z;
 then consider d such that A35:LIN a1,a2,d & a1<>d & a2<>d by A2,TRANSLAC:2;
   ex Y st Y is_line & d in Y & Y // M
  proof consider Y such that A36:d in Y & M // Y by A3,AFF_1:63;take Y;
  thus thesis by A36,AFF_1:50;end;
 then consider Y such that A37:Y is_line & d in Y & Y // M;
 A38:Y // Y & M // M & N // N by A3,A37,AFF_1:55;
   ex d1 st d1 in Y & b1,b2 // b1,d1 proof
   consider e1 such that A39:d<>e1 & e1 in Y by A37,AFF_1:32;
   consider e2 such that A40:b1,b2 // b1,e2 & b1<>e2 by DIRAF:47;
     not d,e1 // b1,e2 proof assume d,e1 // b1,e2; then A41:d,e1 // b1,b2 by
A40,AFF_1:14; d,e1 // Y by A37,A38,A39,AFF_1:54; then A42:b1,b2 // Y by A39,A41
,AFF_1:46; M // Y by A37; then a1,a3 // Y by A2,AFF_1:54;
    then a1,a3 // b1,b2 by A37,A42,AFF_1:45; then a1,a3 // b2,b1 by AFF_1:13;
    then a1,a3 // a2,a1 by A2,AFF_1:14; then a1,a3 // a1,a2 by AFF_1:13;
    then LIN a1,a3,a2 by AFF_1:def 1;
   hence contradiction by A2,A3,A13,AFF_1:39;end;
   then consider d1 such that A43:LIN d,e1,d1 & LIN
 b1,e2,d1 by AFF_1:74;take d1;
     b1,e2 // b1,d1 by A43,AFF_1:def 1;
  hence thesis by A37,A39,A40,A43,AFF_1:14,39;end;
 then consider d1 such that A44:d1 in Y & b1,b2 // b1,d1;
 A45:N // Y & N // M by A2,A37,AFF_1:58;
 A46:N<>M & N<>Y & Y<>M proof assume A47:not thesis;
  A48:now assume N=Y; then A49:a2,d // a2,a4 by A2,A37,A38,AFF_1:53;
     LIN a2,d,a1 by A35,AFF_1:15; then a2,d // a2,a1 by AFF_1:def 1;
   then a2,a4 // a2,a1 by A35,A49,AFF_1:14; then LIN a2,a4,a1 by AFF_1:def 1;
   hence contradiction by A2,A3,A13,AFF_1:39;end;
    now assume Y=M; then A50:a1,d // a1,a3 by A2,A37,AFF_1:53;
     a1,a2 // a1,d by A35,AFF_1:def 1; then a1,a3 // a1,a2
   by A35,A50,AFF_1:14;
   then LIN a1,a3,a2 by AFF_1:def 1;
  hence contradiction by A2,A3,A13,AFF_1:39;end;
 hence contradiction by A2,A47,A48;end;
   LIN a2,a1,d by A35,AFF_1:15; then a2,a1 // a2,d by AFF_1:def 1;
 then A51:b2,b1 // a2,d by A2,AFF_1:14; LIN b1,b2,d1 by A44,AFF_1:def 1;
then LIN
 b2,b1,d1
 by AFF_1:15; then b2,b1 // b2,d1 by AFF_1:def 1;
 then a2,d // b2,d1 & a2,a3 // b2,b3 by A2,A51,AFF_1:13,14;
 then A52:d,a3 // d1,b3 by A1,A2,A3,A37,A44,A45,A46,AFF_2:def 11;
   a1,d // b1,d1 proof a1,a2 // a1,d by A35,AFF_1:def 1; then a2,a1 // a1,d
by AFF_1:13; then b2,b1 // a1,d by A2,AFF_1:14; then b1,b2 // a1,d by AFF_1:13;
 hence thesis by A2,A44,AFF_1:14;end;
 then A53:d,a4 // d1,b4 by A1,A2,A3,A37,A44,A46,AFF_2:def 11;
   Y // N by A2,A37,AFF_1:58;
 hence a3,a4 // b3,b4 by A1,A2,A3,A37,A44,A46,A52,A53,AFF_2:def 11;end;
hence a3,a4 // b3,b4 by A14;end;
hence a3,a4 // b3,b4 by A5;end;
hence thesis by Def1;end;

theorem Th7:
         X satisfies_DES implies X satisfies_major_SCH
proof
assume A1:X satisfies_DES;
  now let o,a1,a2,a3,a4,b1,b2,b3,b4,M,N;
assume A2:M is_line & N is_line & o in M & o in N & a1 in M & a3 in M &
       b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M
       & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N &
       not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 &
       a1,a4 // b1,b4;

then A3:M // M & N // N by AFF_1:55;
A4:now assume A5:a1=a3 or a2=a4;
 A6:now assume A7:a1=a3;
  A8:not LIN o,b2,b1 by A2,AFF_1:39;
    o,b1 // o,b3 by A2,A3,AFF_1:53; then A9:LIN o,b1,b3 by AFF_1:def 1;
    a2,a1 // b2,b3 by A2,A7,AFF_1:13; then b2,b1 // b2,b3
  by A2,AFF_1:14;hence a3,a4 // b3,b4 by A2,A7,A8,A9,AFF_1:23;end;
   now assume A10:a2=a4;
  A11:not LIN o,b1,b2 by A2,AFF_1:39;
    o,b2 // o,b4 by A2,A3,AFF_1:53; then A12:LIN o,b2,b4 by AFF_1:def 1;
    a1,a2 // b1,b2 by A2,AFF_1:13; then b1,b2 // b1,b4 by A2,A10,AFF_1:14;
  hence a3,a4 // b3,b4 by A2,A10,A11,A12,AFF_1:23;end;
hence a3,a4 // b3,b4 by A5,A6;end;
  now assume A13:a1<>a3 & a2<>a4;
 A14:now assume ex x,y,z st LIN x,y,z & x<>y & x<>z & y<>z;
  then consider d such that A15:LIN a1,a2,d & a1<>d & a2<>d by A2,TRANSLAC:2;
    LIN o,d,d by AFF_1:16;
  then consider Y such that A16:Y is_line & o in Y & d in Y & d in Y by AFF_1:
33;
    ex d1 st LIN b1,b2,d1 & d1 in Y proof
      not b1,b2 // o,d proof assume b1,b2 // o,d; then b2,b1 // o,d by AFF_1:13
;
     then A17:a2,a1 // o,d by A2,AFF_1:14; LIN a2,a1,d by A15,AFF_1:15;
     then a2,a1 // a2,d by AFF_1:def 1; then a2,d // o,d by A2,A17,AFF_1:14;
     then d,a2 // d,o by AFF_1:13; then LIN d,a2,o by AFF_1:def 1; then LIN
o,d,a2 by AFF_1:15; then A18:o,d // o,a2 by AFF_1:def 1;A19:o<>d proof assume
 o=d;
     then LIN o,a1,a2 by A15,AFF_1:15;
     hence contradiction by A2,AFF_1:39;end; then A20:Y // N by A2,A16,A18,
AFF_1:52;
       a1,a2 // a1,d by A15,AFF_1:def 1; then a2,a1 // a1,d by AFF_1:13;
     then a1,d // o,d by A2,A17,AFF_1:14; then d,o // d,a1 by AFF_1:13;
     then LIN d,o,a1 by AFF_1:def 1; then LIN o,d,a1 by AFF_1:15; then o,d
// o,a1 by AFF_1:def 1; then Y // M by A2,A16,A19,AFF_1:52; then M // N by A20,
AFF_1:58;
    hence contradiction by A2,AFF_1:59;end;
    then consider d1 such that A21:LIN b1,b2,d1 & LIN
 o,d,d1 by AFF_1:74;take d1;
      o<>d proof assume o=d; then LIN o,a1,a2 by A15,AFF_1:15;
hence contradiction by A2,AFF_1:39;end;
    hence thesis by A16,A21,AFF_1:39;end;
  then consider d1 such that A22:LIN b1,b2,d1 & d1 in Y;
  A23:o<>d proof assume o=d; then LIN o,a1,a2 by A15,AFF_1:15;
hence contradiction by A2,AFF_1:39;end;
  A24:N<>M & N<>Y & M<>Y proof assume A25:not thesis;
     now assume A26: N=Y or M=Y;
      LIN a2,d,a1 & LIN
 a1,d,a2 by A15,AFF_1:15;hence contradiction by A2,A15,A16,A26,AFF_1:39;end;
  hence contradiction by A2,A25;end;
  A27:a2,d // b2,d1 proof LIN a2,a1,d & LIN b2,b1,d1 by A15,A22,AFF_1:15;
   then A28:a2,a1 // a2,d & b2,b1 // b2,d1 by AFF_1:def 1; then b2,b1 // a2,d
by A2,AFF_1:14;hence thesis by A2,A28,AFF_1:14;end;
    a2,a3 // b2,b3 by A2,AFF_1:13;
  then A29:d,a3 // d1,b3 by A1,A2,A16,A22,A23,A24,A27,AFF_2:def 4;
    a1,d // b1,d1 proof a1,a2 // a1,d & b1,b2 // b1,d1 by A15,A22,AFF_1:def 1;
   then A30:a2,a1 // a1,d & b2,b1 // b1,d1 by AFF_1:13; then b2,b1 // a1,d by
A2,AFF_1:14;hence thesis by A2,A30,AFF_1:14;end;
  then d,a4 // d1,b4 by A1,A2,A16,A22,A23,A24,AFF_2:def 4;
 hence a3,a4 // b3,b4 by A1,A2,A16,A22,A23,A24,A29,AFF_2:def 4;end;
   now assume A31:not ex x,y,z st LIN x,y,z & x<>y & x<>z & y<>z;
A32:  LIN a1,a3,b1 by A2,AFF_1:33;
  A33:now assume A34:a1=b1;
A35:   LIN a1,a3,b3 by A2,AFF_1:33;
     a1<>b3 proof assume A36: a1=b3;
    A37:not LIN o,a2,a1 by A2,AFF_1:39;
    A38:LIN o,a1,a3 by A2,AFF_1:33;
      b2,b1 // a2,a3 by A2,A34,A36,AFF_1:13; then a2,a1 // a2,a3 by A2,AFF_1:14
;
    hence contradiction by A13,A37,A38,AFF_1:23;end;
   then A39:a3=b3 by A13,A31,A35;
     LIN a2,a4,b4 by A2,AFF_1:33; then A40:a2=b4 or a4=b4 by A13,A31;
     a2<>b4 proof assume a2=b4; then LIN a1,a4,a2
    by A2,A34,AFF_1:def 1; then LIN a2,a4,a1 by AFF_1:15;
   hence contradiction by A2,A13,AFF_1:39;end;
   hence a3,a4 // b3,b4 by A39,A40,AFF_1:11;end;
    now assume A41:a3=b1;
A42:   LIN a1,a3,b3 by A2,AFF_1:33;
     a3<>b3 proof assume a3=b3; then a3,a2 //
    b2,b1 by A2,A41,AFF_1:13
; then a3,a2 // a2,a1 by A2,AFF_1:14; then a2,a3 // a2,a1
    by AFF_1:13; then LIN a2,a3,a1 by AFF_1:def 1; then LIN a1,a3,a2 by AFF_1:
15;
hence contradiction by A2,A13,AFF_1:39;end;
   then A43:a1=b3 by A13,A31,A42;
A44:   LIN a2,a4,b2 by A2,AFF_1:33;
     a2<>b2 proof assume a2=b2; then LIN a2,a1,a3 by A2,A41,AFF_1:def 1;
    then LIN a1,a3,a2 by AFF_1:15;
   hence contradiction by A2,A13,AFF_1:39;end;
   then A45:a4=b2 by A13,A31,A44;
A46:   LIN a2,a4,b4 by A2,AFF_1:33;
     a4<>b4 proof assume a4=b4; then a4,a1 // a4,a3 by A2,A41,AFF_1:13;
    then LIN a4,a1,a3 by AFF_1:def 1; then LIN a1,a3,a4 by AFF_1:15;
hence contradiction by A2,A13,AFF_1:39;end;
   then A47:a2=b4 by A13,A31,A46;
     a3,a4 // b2,b1 by A41,A45,AFF_1:11;
   then a3,a4 // b4,b3 by A2,A43,A47,AFF_1:14;hence a3,a4 // b3,b4 by AFF_1:13;
end;
 hence a3,a4 // b3,b4 by A13,A31,A32,A33;end;
hence a3,a4 // b3,b4 by A14;end;
hence a3,a4 // b3,b4 by A4;end;
hence thesis by Def2;end;

theorem X satisfies_DES iff X satisfies_SCH
proof
  A1:X satisfies_SCH implies X satisfies_DES
proof
assume A2:X satisfies_SCH;
  now let Y,Z,M,o,a,b,c,a1,b1,c1;
assume A3: o in Y & o in Z & o in M &
o<>a & o<>b & o<>c & a in Y & a1 in Y & b in Z & b1 in Z &
c in M & c1 in M & Y is_line & Z is_line & M is_line &
Y<>Z & Y<>M & a,b // a1,b1 & a,c // a1,c1;
assume A4:not b,c // b1,c1;
A5:now let Y,Z,M,o,a,b,c,a1,b1,c1,d;
  assume A6:X satisfies_SCH;
  assume A7:o in Y & o in Z & o in M & o<>a & o<>b & o<>c & a in Y
    & a1 in Y & b in Z & b1 in Z & c in M & c1 in M & Y is_line &
    Z is_line & M is_line & Y<>Z & Y<>M & a,b // a1,b1 &
    a,c // a1,c1 & LIN b,c,d & LIN b1,c1,d;
    LIN a,a1,d or b,c // b1,c1 proof
    assume A8:not LIN a,a1,d & not b,c // b1,c1;
    A9:c <>c1 & a<>a1 & b<>b1
     proof assume A10:not thesis;
      A11:now assume A12:c =c1;
       A13:not LIN o,c,a proof assume LIN o,c,a; then a in M by A7,AFF_1:39;
then A14:o,a // M by A7,AFF_1:66; o,a // Y by A7,AFF_1:66;
        then Y // M by A7,A14,AFF_1:67;
       hence contradiction by A7,AFF_1:59;end;
         Y // Y by A7,AFF_1:55; then o,a // o,a1 by A7,AFF_1:53;
       then A15:LIN o,a,a1 by AFF_1:def 1;
         c,a // c,a1 by A7,A12,AFF_1:13;
       then A16:a=a1 by A13,A15,AFF_1:23;
       A17:not LIN o,a,b proof assume LIN o,a,b; then b in Y by A7,AFF_1:39;
then A18:o,b // Y by A7,AFF_1:66; o,b // Z by A7,AFF_1:66;
        then Y // Z by A7,A18,AFF_1:67;
       hence contradiction by A7,AFF_1:59;end;
         Z // Z by A7,AFF_1:55; then o,b // o,b1 by A7,AFF_1:53;
       then LIN o,b,b1 by AFF_1:def 1;
       then b=b1 by A7,A16,A17,AFF_1:23;
      hence contradiction by A8,A12,AFF_1:11;end;
      A19:now assume A20:a=a1;
       A21:not LIN o,a,b proof assume LIN o,a,b; then b in Y by A7,AFF_1:39;
then A22:o,b // Y by A7,AFF_1:66; o,b // Z by A7,AFF_1:66;
        then Y // Z by A7,A22,AFF_1:67;
       hence contradiction by A7,AFF_1:59;end;
         Z // Z by A7,AFF_1:55; then o,b // o,b1 by A7,AFF_1:53;
       then LIN o,b,b1 by AFF_1:def 1;
       then A23:b=b1 by A7,A20,A21,AFF_1:23;
       A24:not LIN o,a,c proof assume LIN o,a,c; then c in Y by A7,AFF_1:39;
then A25:o,c // Y by A7,AFF_1:66; o,c // M by A7,AFF_1:66;
        then Y // M by A7,A25,AFF_1:67;
       hence contradiction by A7,AFF_1:59;end;
         M // M by A7,AFF_1:55; then o,c // o,c1 by A7,AFF_1:53;
       then LIN o,c,c1 by AFF_1:def 1;
       then c =c1 by A7,A20,A24,AFF_1:23;
      hence contradiction by A8,A23,AFF_1:11;end;
        now assume A26:b=b1;
       A27:not LIN o,b,a proof assume LIN o,b,a; then a in Z by A7,AFF_1:39;
then A28:o,a // Z by A7,AFF_1:66; o,a // Y by A7,AFF_1:66;
        then Y // Z by A7,A28,AFF_1:67;
       hence contradiction by A7,AFF_1:59;end;
         Y // Y by A7,AFF_1:55; then o,a // o,a1 by A7,AFF_1:53;
       then A29:LIN o,a,a1 by AFF_1:def 1;
         b,a // b,a1 by A7,A26,AFF_1:13;
       then A30:a=a1 by A27,A29,AFF_1:23;
       A31:not LIN o,a,c proof assume LIN o,a,c; then c in Y by A7,AFF_1:39;
then A32:o,c // Y by A7,AFF_1:66; o,c // M by A7,AFF_1:66;
        then Y // M by A7,A32,AFF_1:67;
       hence contradiction by A7,AFF_1:59;end;
         M // M by A7,AFF_1:55; then o,c // o,c1 by A7,AFF_1:53;
       then LIN o,c,c1 by AFF_1:def 1;
       then c =c1 by A7,A30,A31,AFF_1:23;
      hence contradiction by A8,A26,AFF_1:11;end;
     hence contradiction by A10,A11,A19;end;
      now assume A33:b<>c;
    A34:now assume A35:b1=o;
     A36:o=a1 proof assume A37:o<>a1;
      A38:not LIN b,a,o proof assume LIN b,a,o;
       then LIN o,a,b by AFF_1:15; then b in Y by A7,AFF_1:39;
       then A39:o,b // Y by A7,AFF_1:66; o,b // Z by A7,AFF_1:66;
       then Y // Z by A7,A39,AFF_1:67;
      hence contradiction by A7,AFF_1:59;end;
      A40:a,o // a,a1 by A7,AFF_1:65;
        LIN b,o,a1 proof a1,o // a,a1 by A7,AFF_1:65;
       then a,b // a,a1 by A7,A35,A37,AFF_1:14;
       then LIN a,b,a1 by AFF_1:def 1; then LIN a1,b,a by AFF_1:15;
       then A41:a1,b // a1,a by AFF_1:def 1;
       A42:a1<>a proof assume a1=a; then LIN a,b,o by A7,A35,AFF_1:def 1
; then LIN o,a,b by AFF_1:15; then b in Y by A7,AFF_1:39; then A43:o,b // Y
by A7,AFF_1:66; o,b // Z by A7,AFF_1:66; then Y // Z by A7,A43,AFF_1:67;
hence contradiction by A7,AFF_1:59;end;
         a1,a // a1,o by A7,AFF_1:65;
       then a1,b // a1,o by A41,A42,AFF_1:14;
       then LIN a1,b,o by AFF_1:def 1;
      hence thesis by AFF_1:15;end;
     hence contradiction by A37,A38,A40,AFF_1:23;end;
       o=c1 proof assume A44:o<>c1;
      A45:not LIN a,c,o proof assume LIN a,c,o; then LIN o,a,c by AFF_1:15;
        then c in Y by A7,AFF_1:39; then A46:o,c // Y by A7,AFF_1:66;
          o,c // M by A7,AFF_1:66; then Y // M by A7,A46,AFF_1:67;
       hence contradiction by A7,AFF_1:59;end;
      A47:LIN a,o,c1 proof A48:o,c1 // o,c by A7,AFF_1:65;
       then o,c // a,c by A7,A36,A44,AFF_1:14; then c,o // c,a by AFF_1:13;
       then LIN c,o,a by AFF_1:def 1; then LIN o,a,c by AFF_1:15;
       then o,a // o,c by AFF_1:def 1; then o,a // o,c1 by A7,A48,AFF_1:14;
       then LIN o,a,c1 by AFF_1:def 1; hence thesis by AFF_1:15;end;
        c,o // c,c1 by A7,AFF_1:65;
      hence contradiction by A44,A45,A47,AFF_1:23;end;
    hence contradiction by A8,A35,AFF_1:12;end;
      now assume A49:b1<>o;
    A50:a<>b & a<>c proof assume A51:not thesis;
     A52:now assume a=b; then A53:o,a // Z by A7,AFF_1:66; o,a // Y by A7,AFF_1
:66; then Y // Z by A7,A53,AFF_1:67;
     hence contradiction by A7,AFF_1:59;end;
       now assume a=c; then A54:o,a // M by A7,AFF_1:66; o,a // Y by A7,AFF_1:
66; then Y // M by A7,A54,AFF_1:67;
     hence contradiction by A7,AFF_1:59;end;
    hence contradiction by A51,A52;end;
    A55:a1<>b1 & a1<>c1 proof assume A56:not thesis;
     A57:now assume a1=b1; then A58:o,b1 // Y by A7,AFF_1:66; o,b1 // Z by A7,
AFF_1:66; then Y // Z by A49,A58,AFF_1:67;
hence contradiction by A7,AFF_1:59;end;
       now assume a1=c1; then A59:o,a1 // M by A7,AFF_1:66;A60:o<>a1 proof
assume A61:o=a1;
       A62:not LIN a,b,o proof assume LIN a,b,o; then LIN o,a,b by AFF_1:15;
        then b in Y by A7,AFF_1:39; then A63:o,b // Y by A7,AFF_1:66;
          o,b // Z by A7,AFF_1:66; then Y // Z by A7,A63,AFF_1:67;
hence contradiction by A7,AFF_1:59;end; Z // Z by A7,AFF_1:55;
        then A64:o,b // o,b1 by A7,AFF_1:53; then a,b // o,b by A7,A49,A61,
AFF_1:14; then b,a // b,o by AFF_1:13; then LIN b,a,o by AFF_1:def 1;
        then LIN o,a,b by AFF_1:15; then o,a // o,b by AFF_1:def 1;
        then o,a // o,b1 by A7,A64,AFF_1:14; then LIN o,a,b1 by AFF_1:def 1;
       then A65:LIN a,o,b1 by AFF_1:15;
         Z // Z by A7,AFF_1:55; then b,o // b,b1 by A7,AFF_1:53;
       hence contradiction by A49,A62,A65,AFF_1:23;end;
        o,a1 // Y by A7,AFF_1:66; then Y // M by A59,A60,AFF_1:67;
hence contradiction by A7,AFF_1:59;end;
    hence contradiction by A56,A57;end;
    A66:b<>c & b1<>c1 by A8,AFF_1:12;
      LIN b,b,c by AFF_1:16;
    then consider A such that A67:A is_line & b in A & b in A & c in A by AFF_1
:33;
      LIN b1,b1,c1 by AFF_1:16;
    then consider K such that A68:K is_line & b1 in K & b1 in K & c1 in K by
AFF_1:33; LIN o,o,a by AFF_1:16;
    then consider C such that A69:C is_line & o in C & o in C & a in C by AFF_1
:33;
      ex d1 st d1 in C & c,c1 // d,d1 proof
      consider e1 such that A70:o,a // o,e1 & o<>e1 by DIRAF:47;
      consider e2 such that A71:c,c1 // d,e2 & d<>e2 by DIRAF:47;
        not o,e1 // d,e2 proof assume o,e1 // d,e2; then o,a // d,e2
      by A70,AFF_1:14; then A72:o,a // c,c1 by A71,AFF_1:14; M // M
       by A7,AFF_1:55; then c,c1 // o,c by A7,AFF_1:53;
       then o,a // o,c by A9,A72,AFF_1:14;
       then LIN o,a,c by AFF_1:def 1; then c in Y by A7,AFF_1:39;
       then A73:o,c // Y by A7,AFF_1:66; o,c // M by A7,AFF_1:66; then Y //
M
by A7,A73,AFF_1:67;
      hence contradiction by A7,AFF_1:59;end;
      then consider d1 such that A74:LIN o,e1,d1 & LIN d,e2,d1 by AFF_1:74;
      take d1; LIN o,a,e1 by A70,AFF_1:def 1; then A75:
 e1 in C by A7,A69,AFF_1:39;
        d,e2 // d,d1 by A74,AFF_1:def 1;
     hence thesis by A69,A70,A71,A74,A75,AFF_1:14,39;end;
    then consider d1 such that A76:d1 in C & c,c1 // d,d1;
      ex d2 st d2 in C & a,c // d,d2 proof
      consider e1 such that A77:o,a // o,e1 & o<>e1 by DIRAF:47;
      consider e2 such that A78:a,c // d,e2 & d<>e2 by DIRAF:47;
        not o,e1 // d,e2
       proof assume o,e1 // d,e2; then o,a // d,e2 by A77,AFF_1:14;
       then o,a // a,c by A78,AFF_1:14; then a,o // a,c by AFF_1:13;
       then LIN a,o,c by AFF_1:def 1; then c in Y by A7,AFF_1:39; then A79:o,
c // Y
       by A7,AFF_1:66; o,c // M by A7,AFF_1:66; then Y // M by A7,A79,AFF_1:67
;
       hence contradiction by A7,AFF_1:59;end;
      then consider d2 such that A80:LIN o,e1,d2 & LIN d,e2,d2 by AFF_1:74;
      take d2; LIN
 o,a,e1 by A77,AFF_1:def 1; then A81: e1 in C by A7,A69,AFF_1:39;
        d,e2 // d,d2 by A80,AFF_1:def 1;
     hence thesis by A69,A77,A78,A80,A81,AFF_1:14,39;end;
    then consider d2 such that A82:d2 in C & a,c // d,d2;
      ex d3 st d3 in A & o,b // d1,d3 proof
      consider e1 such that A83:b,c // b,e1 & b<>e1 by DIRAF:47;
      consider e2 such that A84:o,b // d1,e2 & d1<>e2 by DIRAF:47;
        not b,e1 // d1,e2
      proof assume b,e1 // d1,e2; then b,c // d1,e2 by A83,AFF_1:14;
       then A85:b,c // o,b by A84,AFF_1:14; then b,c // b,o by AFF_1:13;
       then LIN b,c,o by AFF_1:def 1; then LIN o,b,c by AFF_1:15; then A86:o,
b // o,c
       by AFF_1:def 1;A87:Z // Z & M // M by A7,AFF_1:55; then A88:
       o,b // o,b1 by A7,AFF_1:53; o,c // o,c1 by A7,A87,AFF_1:53; then o,b
// o,c1 by A7,A86,AFF_1:14; then o,b1 // o,c1 by A7,A88,AFF_1:14; then LIN o,
b1,c1 by AFF_1:def 1; then LIN b1,c1,o by AFF_1:15; then b1,c1 // b1,o
       by AFF_1:def 1;
       then b1,c1 // o,b1 by AFF_1:13; then b1,c1 // o,b by A49,A88,AFF_1:14;
      hence contradiction by A7,A8,A85,AFF_1:14;end;
      then consider d3 such that A89:LIN b,e1,d3 & LIN d1,e2,d3 by AFF_1:74;
      take d3; LIN
 b,c,e1 by A83,AFF_1:def 1; then A90: e1 in A by A66,A67,AFF_1:39;
        d1,e2 // d1,d3 by A89,AFF_1:def 1;
     hence thesis by A67,A83,A84,A89,A90,AFF_1:14,39;end;
    then consider d3 such that A91:d3 in A & o,b // d1,d3;
      ex d4 st d4 in K & d1,d3 // d1,d4 proof
      consider e1 such that A92:b1,c1 // b1,e1 & b1<>e1 by DIRAF:47;
      consider e2 such that A93:d1,d3 // d1,e2 & d1<>e2 by DIRAF:47;
        not b1,e1 // d1,e2
       proof assume b1,e1 // d1,e2; then b1,c1 // d1,e2 by A92,AFF_1:14;
        then A94:b1,c1 // d1,d3 by A93,AFF_1:14;
        A95:d1<>d3 proof assume A96: d1=d3;
         A97:d<>d1 proof assume A98: d=d1; Y // Y by A7,AFF_1:55; then o,a
//
o,a1 by A7,AFF_1:53; then LIN o,a,a1 by AFF_1:def 1; then A99:a1 in C by A7,A69
,AFF_1:39; C // C
          by A69,AFF_1:55;
          then a,a1 // a,d by A69,A76,A98,A99,AFF_1:53;
         hence contradiction by A8,AFF_1:def 1;end;
         A100:d in A by A7,A66,A67,AFF_1:39;
           M // M by A7,AFF_1:55; then c,c1 // o,c by A7,AFF_1:53;
         then o,c // d,d1 by A9,A76,AFF_1:14; then d,d1 // c,o by AFF_1:13;
         then A101:o in A by A67,A91,A96,A97,A100,AFF_1:62; A // A by A67,AFF_1
:55;
         then A102:o,b // o,c by A67,A101,AFF_1:53; then LIN
 o,b,c by AFF_1:def 1;
         then LIN b,c,o by AFF_1:15; then b,c // b,o by AFF_1:def 1;
         then A103:b,c // o,b by AFF_1:13;A104:Z // Z & M // M by A7,AFF_1:55;
         then A105:o,b // o,b1 by A7,AFF_1:53; o,c // o,c1 by A7,A104,AFF_1:53
;
         then o,b // o,c1 by A7,A102,AFF_1:14; then o,b1 // o,c1 by A7,A105,
AFF_1:14; then LIN o,b1,c1 by AFF_1:def 1; then LIN b1,c1,o by AFF_1:15;
         then b1,c1 // b1,o by AFF_1:def 1; then b1,c1 // o,b1 by AFF_1:13;
         then o,b // b1,c1 by A49,A105,AFF_1:14;hence contradiction by A7,A8,
A103,AFF_1:14;end;
          Z // Z by A7,AFF_1:55; then A106:o,b // o,b1 by A7,AFF_1:53;
        then o,b1 // d1,d3 by A7,A91,AFF_1:14; then A107:o,b1 // b1,c1 by A94,
A95,AFF_1:14; then b1,o // b1,c1 by AFF_1:13; then LIN b1,o,c1 by AFF_1:def 1
; then LIN o,b1,c1 by AFF_1:15; then o,b1 // o,c1
        by AFF_1:def 1;
        then A108:o,b // o,c1 by A49,A106,AFF_1:14;
        A109:o<>c1 proof assume A110:o=c1;
         A111:not LIN a,c,o proof assume LIN a,c,o; then LIN o,a,c by AFF_1:15;
          then c in Y by A7,AFF_1:39; then A112:o,c // Y by A7,AFF_1:66;
            o,c // M by A7,AFF_1:66; then Y // M by A7,A112,AFF_1:67;
hence contradiction by A7,AFF_1:59;end;
           Y // Y by A7,AFF_1:55; then a,o // a,a1 by A7,AFF_1:53;
         then A113:LIN a,o,a1 by AFF_1:def 1;
           c,o // c,a1 proof
           Y // Y by A7,AFF_1:55; then a1,o // a,a1 by A7,AFF_1:53;
         then a,c // a,a1
         by A7,A55,A110,AFF_1:14; then LIN a,c,a1 by AFF_1:def 1; then LIN a1
,c,a by AFF_1:15; then A114:a1,c // a1,a by AFF_1:def 1; Y // Y by A7,AFF_1:55
;
          then a1,a // a1,o by A7,AFF_1:53; then a1,c // a1,o by A9,A114,AFF_1:
14; then LIN a1,c,o by AFF_1:def 1; then LIN c,o,a1 by AFF_1:15;
         hence thesis by AFF_1:def 1;end;
        hence contradiction by A55,A110,A111,A113,AFF_1:23;end;
          M // M by A7,AFF_1:55; then o,c // o,c1 by A7,AFF_1:53;
        then o,b // o,c by A108,A109,AFF_1:14; then LIN o,b,c by AFF_1:def 1;
        then LIN b,o,c by AFF_1:15; then b,o // b,c by AFF_1:def 1; then o,b
// b,c
        by AFF_1:13; then o,b1 // b,c by A7,A106,AFF_1:14;hence contradiction
by A8,A49,A107,AFF_1:14;end;
      then consider d4 such that A115:LIN b1,e1,d4 & LIN d1,e2,d4 by AFF_1:74;
      take d4; LIN b1,c1,e1 by A92,AFF_1:def 1; then A116: e1 in K by A66,A68,
AFF_1:39;

        d1,e2 // d1,d4 by A115,AFF_1:def 1;
     hence thesis by A68,A92,A93,A115,A116,AFF_1:14,39;end;
    then consider d4 such that A117:d4 in K & d1,d3 // d1,d4;
    A118:c in A & b in A & d in A & d3 in A by A7,A33,A67,A91,AFF_1:39;
    A119:not o in A & not a in A & not d1 in A & not d2 in A
     proof assume A120:not thesis;
      A121:now assume A122:o in
 A; A // A by A67,AFF_1:55; then A123:o,b // o,c by A67,A122,AFF_1:53;
then LIN o,b,c by AFF_1:def 1; then LIN
 b,c,o by AFF_1:15;
       then A124:b,c // b,o by AFF_1:def 1; Z // Z by A7,AFF_1:55;
       then A125:o,b // o,b1 by A7,AFF_1:53; M // M by A7,AFF_1:55;
       then o,c // o,c1 by A7,AFF_1:53; then o,b // o,c1 by A7,A123,AFF_1:14;
       then o,b1 // o,c1 by A7,A125,AFF_1:14; then LIN o,b1,c1 by AFF_1:def 1
;
       then LIN b1,c1,o by AFF_1:15; then b1,c1 // b1,o by AFF_1:def 1;
       then b1,c1 // o,b1 by AFF_1:13; then o,b // b1,c1 by A49,A125,AFF_1:14
;
       then b,o // b1,c1 by AFF_1:13;
      hence contradiction by A7,A8,A124,AFF_1:14;end;

      A126:now assume A127:a in A; A // A by A67,AFF_1:55; then A128:
      a,b // a,c by A67,A127,AFF_1:53;
       A129:a<>b proof assume a=b; then A130:o,b // Y by A7,AFF_1:66; o,b //
Z by A7,AFF_1:66; then Y // Z by A7,A130,AFF_1:67;
        hence contradiction by A7,AFF_1:59;end;
         a<>c proof assume a=c; then A131:o,c // Y by A7,AFF_1:66; o,c // M
by A7,AFF_1:66; then Y // M by A7,A131,AFF_1:67;
        hence contradiction by A7,AFF_1:59;end;
       then a,b // a1,c1 by A7,A128,AFF_1:14; then a1,b1 // a1,c1 by A7,A129,
AFF_1:14; then LIN a1,b1,c1 by AFF_1:def 1; then LIN b1,c1,a1 by AFF_1:15;
       then b1,c1 // b1,a1 by AFF_1:def 1; then A132:a1,b1 // b1,c1 by AFF_1:13
;
       A133:a1<>b1 proof assume a1=b1;
        then A134:o,b1 // Y by A7,AFF_1:66; o,b1 // Z by A7,AFF_1:66;
        then Y // Z by A49,A134,AFF_1:67;
       hence contradiction by A7,AFF_1:59;end;
         LIN a,b,c by A128,AFF_1:def 1; then LIN b,c,a by AFF_1:15; then b,c
// b,a
       by AFF_1:def 1; then b,c // a,b by AFF_1:13; then b,c // a1,b1 by A7,
A129,AFF_1:14;
      hence contradiction by A8,A132,A133,AFF_1:14;end;

      A135:now assume A136:d1 in A;A137:d<>d1 proof assume A138: d=d1;
  Y // Y by A7,AFF_1:55; then o,a // o,a1 by A7,AFF_1:53;
        then LIN o,a,a1 by AFF_1:def 1; then A139:a1 in
 C by A7,A69,AFF_1:39; C // C by A69,AFF_1:55; then a,a1 // a,d by A69,A76,A138
,A139,AFF_1:53;
hence contradiction by A8,AFF_1:def 1;end;
       A140:d in A by A7,A66,A67,AFF_1:39; d,d1 // c,c1 by A76,AFF_1:13;
       then A141:c1 in A by A67,A136,A137,A140,AFF_1:62; M // M by A7,AFF_1:55
;
       then c,c1 // c,o by A7,AFF_1:53; then LIN c,c1,o by AFF_1:def 1;
hence contradiction by A9,A67,A121,A141,AFF_1:39;end;
        now assume A142:d2 in A;A143:d<>d2 proof assume A144: d=d2;
  Y // Y by A7,AFF_1:55; then o,a // o,a1 by A7,AFF_1:53;
        then LIN o,a,a1 by AFF_1:def 1; then A145:a1 in
 C by A7,A69,AFF_1:39; C // C by A69,AFF_1:55; then a,a1 // a,d by A69,A82,A144
,A145,AFF_1:53;
hence contradiction by A8,AFF_1:def 1;end;
       A146:d in A by A7,A66,A67,AFF_1:39; d,d2 // c,a by A82,AFF_1:13;
hence contradiction by A67,A126,A142,A143,A146,AFF_1:62;end;
     hence contradiction by A120,A121,A126,A135;end;
    A147:not c in C & not b in C & not d in C & not d3 in C
     proof assume A148:not thesis;
     A149: now assume A150:c in C; C // C by A69,AFF_1:55; then o,a // o,c
by A69,A150,AFF_1:53; then LIN
 o,a,c by AFF_1:def 1; then c in Y by A7,AFF_1:39;
      then A151:o,c // Y by A7,AFF_1:66; o,c // M by A7,AFF_1:66;
      then Y // M by A7,A151,AFF_1:67;
     hence contradiction by A7,AFF_1:59;end;
     A152:now assume A153:b in C; C // C by A69,AFF_1:55; then o,a // o,b by
A69,A153,AFF_1:53; then LIN
 o,a,b by AFF_1:def 1; then b in Y by A7,AFF_1:39;
      then A154:o,b // Y by A7,AFF_1:66; o,b // Z by A7,AFF_1:66;
      then Y // Z by A7,A154,AFF_1:67;
     hence contradiction by A7,AFF_1:59;end;

     A155: now assume A156:d in
 C; C // C by A69,AFF_1:55; then A157:o,a // a,d by A69,A156,AFF_1:53; Y //
Y
by A7,AFF_1:55; then o,a // a,a1 by A7,AFF_1:53;
      then a,a1 // a,d by A7,A157,AFF_1:14;
     hence contradiction by A8,AFF_1:def 1;end;
        now assume A158:d3 in C;A159:d1<>d3 proof assume A160: d1=d3;
       A161:d<>d1 proof assume A162: d=d1; Y // Y by A7,AFF_1:55; then o,a
//
o,a1 by A7,AFF_1:53; then LIN o,a,a1 by AFF_1:def 1; then A163:a1 in C by A7,
A69,AFF_1:39; C // C by A69,AFF_1:55;
        then a,a1 // a,d by A69,A76,A162,A163,AFF_1:53;
       hence contradiction by A8,AFF_1:def 1;end;
       A164:d in A by A7,A66,A67,AFF_1:39; d,d1 // c,c1 by A76,AFF_1:13;
       then A165:c1 in A by A67,A91,A160,A161,A164,AFF_1:62; A // A by A67,
AFF_1:55;
       then A166:c,c1 // c,b by A67,A165,AFF_1:53; M // M by A7,AFF_1:55;
       then c,o // c,c1 by A7,AFF_1:53; then c,o // c,b by A9,A166,AFF_1:14;
then A167:       LIN c,o,b by AFF_1:def 1; then LIN o,b,c by AFF_1:15;
then A168:o,b // o,c
       by AFF_1:def 1; M // M & Z // Z by A7,AFF_1:55; then A169:o,b // o,b1
&
       o,c // o,c1 by A7,AFF_1:53; then o,b1 // o,c by A7,A168,AFF_1:14;
       then o,b1 // o,c1 by A7,A169,AFF_1:14; then LIN o,b1,c1 by AFF_1:def 1
;
       then LIN b1,c1,o by AFF_1:15; then b1,c1 // b1,o by AFF_1:def 1;
       then b1,c1 // o,b1 by AFF_1:13; then A170:o,b // b1,c1 by A49,A169,AFF_1
:14; LIN b,c,o by A167,AFF_1:15;
       then b,c // b,o by AFF_1:def 1; then b,c // o,b by AFF_1:13;
hence contradiction by A7,A8,A170,AFF_1:14;end;
        d1,d3 // o,b by A91,AFF_1:13;
     hence contradiction by A69,A76,A152,A158,A159,AFF_1:62;end;
     hence contradiction by A148,A149,A152,A155;end;
    A171:a,c // d2,d by A82,AFF_1:13;
      c,o // d,d1 proof M // M by A7,AFF_1:55; then c,c1 // c,o by A7,AFF_1:53
;hence thesis by A9,A76,AFF_1:14;end;
    then A172:a,b // d2,d3 by A6,A67,A69,A76,A82,A91,A118,A119,A147,A171,Def3;
    A173:o in C & a1 in C & d1 in C & d2 in C
     proof
        a1 in C proof Y // Y by A7,AFF_1:55; then o,a // o,a1 by A7,AFF_1:53;
      then LIN o,a,a1 by AFF_1:def 1; hence thesis by A7,A69,AFF_1:39;end;
     hence thesis by A69,A76,A82;end;
    A174:c1 in K & b1 in K & d in K & d4 in K
     proof
        d in K proof b1<>c1 by A8,AFF_1:12;
      hence thesis by A7,A68,AFF_1:39;end;
     hence thesis by A68,A117;end;
    A175:not o in K & not a1 in K & not d1 in K & not d2 in K
     proof assume A176:not thesis;
      A177:now assume A178:o in K; K // K by A68,AFF_1:55; then A179:
      o,b1 // o,c1 by A68,A178,AFF_1:53; then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o
       by AFF_1:15; then A180:b1,c1 // b1,o by AFF_1:def 1; Z // Z
       by A7,AFF_1:55;
       then A181:o,b1 // o,b by A7,AFF_1:53; then A182:o,b // o,c1 by A49,A179,
AFF_1:14;
       A183:o<>c1 proof assume A184:o=c1;
        A185:a1<>o proof assume A186:a1=o;
       A187:not LIN a,b,o proof assume LIN a,b,o; then LIN o,a,b by AFF_1:15;
        then b in Y by A7,AFF_1:39; then A188:o,b // Y by A7,AFF_1:66;
          o,b // Z by A7,AFF_1:66; then Y // Z by A7,A188,AFF_1:67;
hence contradiction by A7,AFF_1:59;end; Z // Z by A7,AFF_1:55;
        then A189:o,b // o,b1 by A7,AFF_1:53; then a,b // o,b by A7,A49,A186,
AFF_1:14; then b,a // b,o by AFF_1:13; then LIN b,a,o by AFF_1:def 1;
        then LIN o,a,b by AFF_1:15; then o,a // o,b by AFF_1:def 1;
        then o,a // o,b1 by A7,A189,AFF_1:14; then LIN o,a,b1 by AFF_1:def 1;
       then A190:LIN a,o,b1 by AFF_1:15;
         Z // Z by A7,AFF_1:55; then b,o // b,b1 by A7,AFF_1:53;
       hence contradiction by A49,A187,A190,AFF_1:23;end;
        A191:not LIN c,a,o proof assume LIN c,a,o; then LIN o,a,c by AFF_1:15
;
         then c in Y by A7,AFF_1:39; then A192:o,c // Y by A7,AFF_1:66;
           o,c // M by A7,AFF_1:66; then Y // M by A7,A192,AFF_1:67;
hence contradiction by A7,AFF_1:59;end;
        A193:LIN c,o,a1 proof Y // Y by A7,AFF_1:55;
         then A194:a1,o // o,a by A7,AFF_1:53; then a,c // o,a by A7,A184,A185,
AFF_1:14; then a,c // a,o by AFF_1:13; then LIN a,c,o by AFF_1:def 1;
         then LIN o,c,a by AFF_1:15; then o,c // o,a by AFF_1:def 1;
         then o,c // a1,o by A7,A194,AFF_1:14; then o,c // o,a1 by AFF_1:13;
         then LIN o,c,a1 by AFF_1:def 1;hence thesis by AFF_1:15;end;
          Y // Y by A7,AFF_1:55; then a,o // a,a1 by A7,AFF_1:53;
        hence contradiction by A185,A191,A193,AFF_1:23;end;
         M // M by A7,AFF_1:55; then o,c // o,c1 by A7,AFF_1:53;
       then o,b // o,c by A182,A183,AFF_1:14; then LIN o,b,c by AFF_1:def 1;
       then LIN b,c,o by AFF_1:15; then b,c // b,o by AFF_1:def 1; then b,c
// o,b
       by AFF_1:13; then b,c // o,b1 by A7,A181,AFF_1:14; then b,c // b1,o
by AFF_1:13;
      hence contradiction by A8,A49,A180,AFF_1:14;end;
      A195:now assume A196:a1 in K; K // K by A68,AFF_1:55; then A197:
      a1,b1 // a1,c1
       by A68,A196,AFF_1:53; then LIN a1,b1,c1 by AFF_1:def 1; then LIN
 b1,c1,a1 by AFF_1:15; then b1,c1 // b1,a1 by AFF_1:def 1; then A198:b1,c1 //
a1,b1
       by AFF_1:13; a,b // a1,c1 by A7,A55,A197,AFF_1:14; then a,b // a,c
       by A7,A55,AFF_1:14; then LIN a,b,c by AFF_1:def 1; then LIN b,c,a by
AFF_1:15; then b,c // b,a by AFF_1:def 1; then b,c // a,b by AFF_1:13;
       then b,c // a1,b1 by A7,A50,AFF_1:14;hence contradiction by A8,A55,A198,
AFF_1:14;end;

      A199:now assume A200:d1 in K;A201:d in K by A7,A66,A68,AFF_1:39;
       A202:d<>d1 proof assume A203: d=d1; C // C by A69,AFF_1:55; then A204:
o
,a // a,d by A69,A76,A203,AFF_1:53; Y // Y by A7,AFF_1:55; then o,a // a,a1
by A7,AFF_1:53; then a,a1 // a,d by A7,A204,AFF_1:14;
       hence contradiction by A8,AFF_1:def 1;end;
         d,d1 // c1,c by A76,AFF_1:13; then A205:c in K by A68,A200,A201,A202,
AFF_1:62;
         M // M by A7,AFF_1:55; then c,c1 // c,o by A7,AFF_1:53;
       then LIN c,c1,o by AFF_1:def 1;
      hence contradiction by A9,A68,A177,A205,AFF_1:39;end;
        now assume A206:d2 in K;A207:d in K by A7,A66,A68,AFF_1:39;
       A208:d<>d2 proof assume A209: d=d2;
         Y // Y by A7,AFF_1:55; then A210:o,a // a,a1 by A7,AFF_1:53;
         C // C by A69,AFF_1:55; then o,a // a,d by A69,A82,A209,AFF_1:53;
       then a,a1 // a,d by A7,A210,AFF_1:14;
       hence contradiction by A8,AFF_1:def 1;end;
         d,d2 // a1,c1 by A7,A50,A82,AFF_1:14; then d,d2 // c1,a1 by AFF_1:13;
      hence contradiction by A68,A195,A206,A207,A208,AFF_1:62;end;
     hence contradiction by A176,A177,A195,A199;end;
    A211:not c1 in C & not b1 in C & not d in C & not d4 in C
     proof assume A212:not thesis;
      A213:now assume A214:c1 in C; M // M by A7,AFF_1:55; then o,c1 // c1,c
       by A7,AFF_1:53;
       hence contradiction by A68,A69,A147,A175,A214,AFF_1:62;end;
      A215:now assume A216:b1 in C; Z // Z by A7,AFF_1:55; then o,b1 // o,b
       by A7,AFF_1:53;
      hence contradiction by A49,A69,A147,A216,AFF_1:62;end;
        now assume A217:d4 in C;
         d1,d4 // d1,d3 by A117,AFF_1:13;
      hence contradiction by A69,A76,A117,A147,A175,A217,AFF_1:62;end;
     hence contradiction by A147,A212,A213,A215;end;
    A218:a1,c1 // d2,d proof a<>c
      proof assume A219:a=c;A220:o,a // Y by A7,AFF_1:66; o,a // M by A7,A219,
AFF_1:66; then Y // M by A7,A220,AFF_1:67;
      hence contradiction by A7,AFF_1:59;end;
      then a1,c1 // d,d2 by A7,A82,AFF_1:14;
     hence thesis by AFF_1:13;end;
    A221:c1,o // d,d1 proof M // M by A7,AFF_1:55; then c1,o // c,c1 by A7,
AFF_1:53;hence thesis by A9,A76,AFF_1:14;end;
      o,b1 // d1,d4 proof
      A222:o,b // o,b1 by A7,AFF_1:65; o,b // d1,d4 by A76,A91,A117,A147,AFF_1:
14;
      hence thesis by A7,A222,AFF_1:14;end;
    then A223:a1,b1 // d2,d4 by A6,A68,A69,A173,A174,A175,A211,A218,A221,Def3;
    A224:d1<>d2 proof assume d1=d2;
     then a,c // c,c1 by A76,A82,A147,AFF_1:14; then c,c1 // c,a
     by AFF_1:13;
     then LIN c,c1,a by AFF_1:def 1; then a in M by A7,A9,AFF_1:39;
     then A225:o,a // M by A7,AFF_1:66; o,a // Y by A7,AFF_1:66; then Y // M
by A7,A225,AFF_1:67;
    hence contradiction by A7,AFF_1:59;end;
    A226:d4<>d3 proof assume A227: d4=d3;
       d=d3 proof assume A228:d<>d3;
      A229:d in A & d in K by A7,A66,A67,A68,AFF_1:39;
      A230:A // A & K // K by A67,A68,AFF_1:55;
      then A231:b1,c1 // d,d3 by A68,A117,A227,A229,AFF_1:53;
        b,c // d,d3 by A67,A91,A229,A230,AFF_1:53;
     hence contradiction by A8,A228,A231,AFF_1:14;end;
     then A232:o,b // d,d1 by A91,AFF_1:13;
     A233:M // M & Z // Z by A7,AFF_1:55; then o,c // c,c1 by A7,AFF_1:53;
     then o,c // d,d1 by A9,A76,AFF_1:14;
     then A234:o,b // o,c by A76,A147,A232,AFF_1:14
; then LIN o,b,c by AFF_1:def 1;
     then LIN b,c,o by AFF_1:15; then b,c // b,o by AFF_1:def 1;
     then A235:b,c // o,b by AFF_1:13;
     A236:o,b // o,b1 & o,c // o,c1 by A7,A233,AFF_1:53;
     then o,b1 // o,c by A7,A234,AFF_1:14; then o,b1 // o,c1 by A7,A236,AFF_1:
14;
     then LIN o,b1,c1 by AFF_1:def 1; then LIN b1,c1,o by AFF_1:15;
     then b1,c1 // b1,o by AFF_1:def 1; then b1,c1 // o,b1 by AFF_1:13;
     then o,b // b1,c1 by A49,A236,AFF_1:14;hence contradiction by A7,A8,A235,
AFF_1:14
;end;
      d2,d3 // a1,b1 by A7,A50,A172,AFF_1:14;
    then d2,d3 // d2,d4 by A55,A223,AFF_1:14; then LIN d2,d3,d4 by AFF_1:def 1;
    then LIN d4,d3,d2 by AFF_1:15; then A237:d4,d3 // d4,d2 by AFF_1:def 1;
      LIN d1,d3,d4 by A117,AFF_1:def 1; then LIN d4,d3,d1 by AFF_1:15;
    then d4,d3 // d4,d1 by AFF_1:def 1; then A238: d4,d2 // d4,d1 by A226,A237,
AFF_1:14;

      not LIN d4,d2,d1
     proof assume LIN d4,d2,d1; then LIN d1,d2,d4 by AFF_1:15;
hence contradiction by A69,A76,A82,A211,A224,AFF_1:39;end;
    hence contradiction by A238,AFF_1:def 1;end;
    hence contradiction by A34;end;
    hence contradiction by A8,AFF_1:12;end;
  hence LIN a,a1,d or b,c // b1,c1;end;
A239:now assume Z // M; then A240:b in M & b1 in M by A3,AFF_1:59; M // M by A3
,AFF_1:55;
hence contradiction by A3,A4,A240,AFF_1:53;end;
  now assume A241:not Z // M;
 A242:Y // Y & Z // Z & M // M by A3,AFF_1:55;
 A243:not a in Z & not a in M proof assume A244:not thesis;
  A245:now assume a in Z; then A246:o,a // Z by A3,AFF_1:66; o,a // Y by A3,
AFF_1:66; then Y // Z by A3,A246,AFF_1:67;
  hence contradiction by A3,AFF_1:59;end;
    now assume a in M; then A247:o,a // M by A3,AFF_1:66; o,a // Y by A3,AFF_1:
66; then Y // M by A3,A247,AFF_1:67;
  hence contradiction by A3,AFF_1:59;end;
 hence contradiction by A244,A245;end;
 A248:a<>a1 & b<>b1 & c <>c1
  proof assume A249:not thesis;
   A250:now assume A251:a=a1;
    A252:not LIN a,o,b proof assume LIN a,o,b; then LIN o,b,a by AFF_1:15;
hence contradiction by A3,A243,AFF_1:39;end;
    A253:LIN a,b,b1 by A3,A251,AFF_1:def 1;
      o,b // o,b1 by A3,A242,AFF_1:53;
    then A254:b=b1 by A252,A253,AFF_1:23;
    A255:not LIN a,o,c proof assume LIN a,o,c; then LIN o,c,a by AFF_1:15;
hence contradiction by A3,A243,AFF_1:39;end;
    A256:LIN a,c,c1 by A3,A251,AFF_1:def 1;
      o,c // o,c1 by A3,A242,AFF_1:53;
    then c =c1 by A255,A256,AFF_1:23;
   hence contradiction by A4,A254,AFF_1:11;end;

   A257:now assume A258:b=b1;
    A259:not LIN b,o,a by A3,A243,AFF_1:39;
      b,a // b,a1 by A3,A258,AFF_1:13;
    then A260:LIN b,a,a1 by AFF_1:def 1;
      o,a // o,a1 by A3,A242,AFF_1:53;
    hence contradiction by A250,A259,A260,AFF_1:23;end;
     now assume A261:c =c1;
    A262:not LIN c,o,a by A3,A243,AFF_1:39;
      c,a // c,a1 by A3,A261,AFF_1:13;
    then A263:LIN c,a,a1 by AFF_1:def 1; o,a // o,a1 by A3,A242,AFF_1:53;
    hence contradiction by A250,A262,A263,AFF_1:23;end;
  hence contradiction by A249,A250,A257;end;
A264:a1<>o & b1<>o & c1<>o proof assume A265:not thesis;
 A266:now assume A267:a1=o;
       A268:o=b1 proof assume A269:o<>b1;
        A270:not LIN b,a,o proof assume LIN b,a,o; then LIN o,b,a by AFF_1:15
;
         hence contradiction by A3,A243,AFF_1:39;end;
          b,o // b,b1 by A3,A242,AFF_1:53; then A271:LIN b,o,b1 by AFF_1:def 1;
          a,o // a,b1 proof A272:o,b1 // o,b
         by A3,A242,AFF_1:53; then a,b // o,b by A3,A267,A269,AFF_1:14;
         then b,a // b,o by AFF_1:13; then LIN b,a,o by AFF_1:def 1;
then LIN o,a,b
         by AFF_1:15; then o,a // o,b by AFF_1:def 1; then o,a // o,b1 by A3,
A272,AFF_1:14; then LIN o,a,b1 by AFF_1:def 1; then LIN
 a,o,b1 by AFF_1:15;
         hence thesis by AFF_1:def 1;end;
        hence contradiction by A269,A270,A271,AFF_1:23;end;
         o=c1 proof assume A273:o<>c1;
        A274:not LIN c,a,o proof assume LIN c,a,o; then LIN o,c,a by AFF_1:15
;
         hence contradiction by A3,A243,AFF_1:39;end;
          c,o // c,c1 by A3,A242,AFF_1:53; then A275:LIN c,o,c1 by AFF_1:def 1;
          a,o // a,c1 proof A276:o,c1 // o,c
         by A3,A242,AFF_1:53; then a,c // o,c by A3,A267,A273,AFF_1:14;
         then c,o // c,a by AFF_1:13; then LIN c,o,a by AFF_1:def 1;
then LIN o,c,a
         by AFF_1:15; then o,c // o,a by AFF_1:def 1; then o,c1 // o,a by A3,
A276,AFF_1:14; then LIN o,c1,a by AFF_1:def 1; then LIN
 a,o,c1 by AFF_1:15;
        hence thesis by AFF_1:def 1;end;
        hence contradiction by A273,A274,A275,AFF_1:23;end;
       hence contradiction by A4,A268,AFF_1:12;end;

 A277:now assume A278:b1=o;
  A279:not LIN a,b,o proof assume LIN a,b,o; then LIN o,b,a by AFF_1:15;
hence contradiction by A3,A243,AFF_1:39;end;
    a,o // a,a1 by A3,A242,AFF_1:53; then A280:LIN a,o,a1 by AFF_1:def 1;
    b,o // b,a1 proof A281:a1,o // a,a1 by A3,A242,AFF_1:53; then a,b // a,a1
by A3,A266,A278,AFF_1:14; then LIN
 a,b,a1 by AFF_1:def 1; then LIN
 a1,b,a by AFF_1:15; then a1,b // a1,a by AFF_1:def 1;
   then a1,b // a,a1 by AFF_1:13; then a1,b // a1,o by A248,A281,AFF_1:14;
   then LIN a1,b,o by AFF_1:def 1; then LIN b,o,a1 by AFF_1:15;
  hence thesis by AFF_1:def 1;end;
 hence contradiction by A266,A279,A280,AFF_1:23;end;
   now assume A282:c1=o;
  A283:not LIN a,c,o proof assume LIN a,c,o; then LIN o,c,a by AFF_1:15;
hence contradiction by A3,A243,AFF_1:39;end;
    a,o // a,a1 by A3,A242,AFF_1:53; then A284:LIN a,o,a1 by AFF_1:def 1;
    c,o // c,a1 proof A285:a1,o // a,a1 by A3,A242,AFF_1:53; then a,c // a,a1
by A3,A266,A282,AFF_1:14; then LIN
 a,c,a1 by AFF_1:def 1; then LIN
 a1,a,c by AFF_1:15; then a1,a // a1,c by AFF_1:def 1;
   then a,a1 // a1,c by AFF_1:13; then a1,o // a1,c by A248,A285,AFF_1:14;
   then LIN a1,o,c by AFF_1:def 1; then LIN c,o,a1 by AFF_1:15;
  hence thesis by AFF_1:def 1;end;
 hence contradiction by A266,A283,A284,AFF_1:23;end;
hence contradiction by A265,A266,A277;end;
 consider d such that A286:LIN b,c,d & LIN b1,c1,d by A4,AFF_1:74;
 A287:LIN a,a1,d by A2,A3,A4,A5,A286;
   ex d1 st a,b // d,d1 & d1 in Z proof
   consider e1 such that A288:o,b // o,e1 & o<>e1 by DIRAF:47;
   consider e2 such that A289:a,b // d,e2 & d<>e2 by DIRAF:47;
     not o,e1 // d,e2
    proof assume o,e1 // d,e2; then o,b // d,e2 by A288,AFF_1:14;
     then o,b // a,b by A289,AFF_1:14; then b,o // b,a by AFF_1:13;
     then LIN b,o,a by AFF_1:def 1;
    hence contradiction by A3,A243,AFF_1:39;end;
   then consider d1 such that A290:LIN o,e1,d1 & LIN d,e2,d1 by AFF_1:74;
   take d1; o,e1 // o,d1 by A290,AFF_1:def 1; then o,b // o,d1 by A288,AFF_1:14
;
   then A291: LIN o,b,d1 by AFF_1:def 1;
     d,e2 // d,d1 by A290,AFF_1:def 1;
  hence thesis by A3,A289,A291,AFF_1:14,39;end;
 then consider d1 such that A292:a,b // d,d1 & d1 in Z;
   ex d2 st a,c // d,d2 & d2 in M proof
   consider e1 such that A293:o,c // o,e1 & o<>e1 by DIRAF:47;
   consider e2 such that A294:a,c // d,e2 & d<>e2 by DIRAF:47;
     not o,e1 // d,e2
    proof assume o,e1 // d,e2; then o,c // d,e2 by A293,AFF_1:14;
     then o,c // a,c by A294,AFF_1:14; then c,o // c,a by AFF_1:13;
     then LIN c,o,a by AFF_1:def 1;
    hence contradiction by A3,A243,AFF_1:39;end;
   then consider d2 such that A295:LIN o,e1,d2 & LIN d,e2,d2 by AFF_1:74;
   take d2; o,e1 // o,d2 by A295,AFF_1:def 1; then o,c // o,d2 by A293,AFF_1:14
;
   then A296: LIN o,c,d2 by AFF_1:def 1;
     d,e2 // d,d2 by A295,AFF_1:def 1;
  hence thesis by A3,A294,A296,AFF_1:14,39;end;
 then consider d2 such that A297:a,c // d,d2 & d2 in M;
 A298:d1<>d2 proof assume d1=d2; then A299:o,d1 // M
  by A3,A297,AFF_1:66;A300:o<>d1 proof assume A301: o=d1;
   A302:a,a1 // a,d by A287,AFF_1:def 1;A303:o<>d proof assume o=d;
then LIN o,b,c by A286,AFF_1:15; then c in Z by A3,AFF_1:39;
    then A304:o,c // Z by A3,AFF_1:66; o,c // M by A3,AFF_1:66;
hence contradiction by A3,A241,A304,AFF_1:67;end;
     a,o // a,a1 by A3,A242,AFF_1:53;
   then a,o // a,d by A248,A302,AFF_1:14; then LIN a,o,d by AFF_1:def 1;
then LIN
 o,a,d
   by AFF_1:15; then o,a // o,d by AFF_1:def 1; then a,o // d,o by AFF_1:13;
   then a,b // a,o by A292,A301,A303,AFF_1:14; then LIN
 a,b,o by AFF_1:def 1;
   then LIN o,b,a by AFF_1:15;
  hence contradiction by A3,A243,AFF_1:39;end;
    o,d1 // Z by A3,A292,AFF_1:66;
 hence contradiction by A241,A299,A300,AFF_1:67;end;
 A305:now assume A306:b1,c1 // d1,d2;
    ex d5 st LIN b,c,d5 & LIN d1,d2,d5 proof
   consider e1 such that A307:b,c // b,e1 & b<>e1 by DIRAF:47;
   consider e2 such that A308:d1,d2 // d1,e2 & d1<>e2 by DIRAF:47;
     not b,e1 // d1,e2
    proof assume b,e1 // d1,e2; then b,e1 // d1,d2 by A308,AFF_1:14;
     then b,c // d1,d2 by A307,AFF_1:14;
    hence contradiction by A4,A298,A306,AFF_1:14;end;
   then consider d5 such that A309:LIN b,e1,d5 & LIN d1,e2,d5 by AFF_1:74;
   take d5;
     d1,e2 // d1,d5 & b,e1 // b,d5 by A309,AFF_1:def 1; then d1,d2 // d1,d5 &
   b,c // b,d5 by A307,A308,AFF_1:14;
   hence thesis by AFF_1:def 1;end;
  then consider d5 such that A310:LIN b,c,d5 & LIN d1,d2,d5;
  A311:d in Y by A3,A248,A287,AFF_1:39;

  A312:now assume A313:LIN a,d,d5;
   A314:not LIN a,b,d proof assume LIN a,b,d; then A315:LIN a,d,b by AFF_1:15;
      a<>d proof assume A316: a=d; then LIN a,b,c by A286,AFF_1:15;
     then a,b // a,c by AFF_1:def 1;
     then a1,b1 // a,c by A3,A243,AFF_1:14; then a1,b1 // a1,c1 by A3,A243,
AFF_1:14; then LIN a1,b1,c1 by AFF_1:def 1; then LIN b1,c1,a1 by AFF_1:15;
     then b1,c1 // b1,a1 by AFF_1:def 1; then A317:b1,c1 // a1,b1 by AFF_1:13;
     A318:a1<>b1 proof assume A319: a1=b1;
        o,a1 // o,a by A3,A242,AFF_1:53; then LIN o,a1,a by AFF_1:def 1;
hence contradiction by A3,A243,A264,A319,AFF_1:39;end;
       b,c // b,a by A286,A316,AFF_1:def 1; then b,c // a,b
     by AFF_1:13; then b,c // a1,b1 by A3,A243,AFF_1:14;hence contradiction
by A4,A317,A318,AFF_1:14;end;
    then b in Y by A3,A311,A315,AFF_1:39; then A320:o,b // Y by A3,AFF_1:66;
      o,b // Z by A3,AFF_1:66; then Y // Z by A3,A320,AFF_1:67;
hence contradiction by A3,AFF_1:59;end;
     b,d // b,d5 proof A321:b<>c by A4,AFF_1:12;
     A322:b,c // b,d by A286,AFF_1:def 1;
      b,c // b,d5 by A310,AFF_1:def 1;hence thesis by A321,A322,AFF_1:14;end;
   then LIN d1,d2,d by A310,A313,A314,AFF_1:23; then LIN d,d1,d2
   by AFF_1:15; then A323:d,d1 // d,d2 by AFF_1:def 1;
   A324:o<>d proof assume A325: o=d; then LIN o,b,c by A286,AFF_1:15;
then A326:o,b // o,c by AFF_1:def 1;A327:o,b // o,b1 &
    o,c // o,c1 by A3,A242,AFF_1:53; then o,b1 // o,c by A3,A326,AFF_1:14;
    then o,b1 // o,c1 by A3,A327,AFF_1:14; then LIN o,b1,c1 by AFF_1:def 1;
    then LIN b1,c1,o by AFF_1:15; then b1,c1 // b1,o by AFF_1:def 1;
    then A328:b1,c1 // o,b1 by AFF_1:13; b,c // b,o by A286,A325,AFF_1:def 1;
    then b,c // o,b by AFF_1:13; then b,c // o,b1 by A3,A327,AFF_1:14;
hence contradiction by A4,A264,A328,AFF_1:14;end;
   A329:d<>d1 proof assume d=d1; then A330:o,d // Z by A3,A292,AFF_1:66; o,d
// Y by A3,A311,AFF_1:66; then Y // Z by A324,A330,AFF_1:67;
    hence contradiction by A3,AFF_1:59;end;
   A331:d<>d2 proof assume d=d2; then A332:o,d // M by A3,A297,AFF_1:66; o,d
// Y by A3,A311,AFF_1:66; then Y // M by A324,A332,AFF_1:67;
    hence contradiction by A3,AFF_1:59;end;
     a,b // d,d2 by A292,A323,A329,AFF_1:14;
   then A333:a,b // a,c by A297,A331,AFF_1:14;
   then a1,b1 // a,c by A3,A243,AFF_1:14; then a1,b1 // a1,c1 by A3,A243,AFF_1:
14; then LIN a1,b1,c1 by AFF_1:def 1; then LIN b1,c1,a1 by AFF_1:15;
   then b1,c1 // b1,a1 by AFF_1:def 1; then A334:b1,c1 // a1,b1 by AFF_1:13;
   A335:a1<>b1 proof assume A336: a1=b1;
      o,a1 // o,a by A3,A242,AFF_1:53; then LIN o,a1,a by AFF_1:def 1;
hence contradiction by A3,A243,A264,A336,AFF_1:39;end;
     LIN a,b,c by A333,AFF_1:def 1; then LIN b,c,a by AFF_1:15; then b,c // b
,
a
   by AFF_1:def 1; then b,c // a,b by AFF_1:13; then b,c // a1,b1 by A3,A243,
AFF_1:14;
  hence contradiction by A4,A334,A335,AFF_1:14;end;
     not b,c // d1,d2 by A4,A298,A306,AFF_1:14;
 hence contradiction by A2,A3,A5,A292,A297,A310,A311,A312;end;
   now assume A337:not b1,c1 // d1,d2;
  then consider d5 such that A338:LIN b1,c1,d5 & LIN d1,d2,d5 by AFF_1:74;
  A339:d in Y by A3,A248,A287,AFF_1:39;
  A340:a1,b1 // d,d1 by A3,A243,A292,AFF_1:14;
    a1,c1 // d,d2 by A3,A243,A297,AFF_1:14;
  then A341:LIN a1,d,d5 by A2,A3,A5,A264,A292,A297,A337,A338,A339,A340;
  A342:not LIN a1,b1,d proof assume LIN a1,b1,d; then A343:LIN a1,d,b1 by AFF_1
:15; a1<>d proof assume A344: a1=d; then LIN a1,b1,c1 by A286,AFF_1:15;
then A345:a1,b1 // a1,c1 by AFF_1:def 1;
    A346:a1<>b1 & a1<>c1 proof assume A347: not thesis;
  o,a1 // o,a by A3,A242,AFF_1:53; then LIN o,a1,a by AFF_1:def 1;
hence contradiction by A3,A243,A264,A347,AFF_1:39;end;
    then a,b // a1,c1 by A3,A345,AFF_1:14; then a,b // a,c by A3,A346,AFF_1:14;
    then LIN a,b,c by AFF_1:def 1; then LIN b,c,a by AFF_1:15; then b,c // b
,a
    by AFF_1:def 1; then A348:b,c // a,b by AFF_1:13;
      b1,c1 // b1,a1 by A286,A344,AFF_1:def 1;
    then b1,c1 // a1,b1 by AFF_1:13; then b1,c1 // a,b by A3,A346,AFF_1:14;
   hence contradiction by A3,A4,A243,A348,AFF_1:14;end;
   then b1 in Y by A3,A339,A343,AFF_1:39; then o,b1 // o,a by A3,A242,AFF_1:53;
   then LIN o,b1,a by AFF_1:def 1;
  hence contradiction by A3,A243,A264,AFF_1:39;end;
    b1,d // b1,d5 proof A349:b1<>c1 by A4,AFF_1:12;
   A350:b1,c1 // b1,d5 by A338,AFF_1:def 1; b1,c1 // b1,d by A286,AFF_1:def 1
;
   hence thesis by A349,A350,AFF_1:14;end;
  then d=d5 by A341,A342,AFF_1:23; then LIN d,d1,d2 by A338,AFF_1:15;
  then A351:d,d1 // d,d2 by AFF_1:def 1;
  A352:d<>o proof assume A353: d=o; then LIN o,b,c by A286,AFF_1:15;
   then A354:o,b // o,c by AFF_1:def 1;A355:o,b // o,b1 & o,c // o,c1 by A3,
A242,AFF_1:53; then o,b1 // o,c by A3,A354,AFF_1:14; then o,b1 // o,c1 by A3,
A355,AFF_1:14; then LIN o,b1,c1 by AFF_1:def 1; then LIN
 b1,c1,o by AFF_1:15;
   then b1,c1 // b1,o by AFF_1:def 1; then A356:b1,c1 // o,b1 by AFF_1:13;
     b,c // b,o by A286,A353,AFF_1:def 1; then b,c // o,b
   by AFF_1:13; then b,c // o,b1 by A3,A355,AFF_1:14;hence contradiction by A4,
A264,A356,AFF_1:14;end;
  A357:d<>d1 proof assume A358: d=d1; o,d // o,a by A3,A242,A339,AFF_1:53;
then LIN o,d,a by AFF_1:def 1;
  hence contradiction by A3,A243,A292,A352,A358,AFF_1:39;end;
  A359:d<>d2 proof assume A360: d=d2; o,d // o,a by A3,A242,A339,AFF_1:53;
then LIN o,d,a by AFF_1:def 1;
  hence contradiction by A3,A243,A297,A352,A360,AFF_1:39;end;
    a,b // d,d2 by A292,A351,A357,AFF_1:14;
  then A361:a,b // a,c by A297,A359,AFF_1:14;
  A362:a1<>b1 proof assume A363: a1=b1; o,a1 // o,a by A3,A242,AFF_1:53;
then LIN o,a1,a by AFF_1:def 1;hence contradiction by A3,A243,A264,A363,AFF_1:
39;
end;
    a1,b1 // a,c by A3,A243,A361,AFF_1:14; then a1,b1 // a1,c1 by A3,A243,AFF_1
:14; then LIN a1,b1,c1 by AFF_1:def 1; then LIN b1,c1,a1 by AFF_1:15;
  then b1,c1 // b1,a1 by AFF_1:def 1; then A364:b1,c1 // a1,b1 by AFF_1:13;
    LIN a,b,c by A361,AFF_1:def 1; then LIN b,c,a by AFF_1:15; then b,c // b,
a
by AFF_1:def 1; then b,c // a,b by AFF_1:13; then b,c // a1,b1 by A3,A243,AFF_1
:14;
 hence contradiction by A4,A362,A364,AFF_1:14;end;
hence contradiction by A305;end;
hence contradiction by A239; end;
hence thesis by AFF_2:def 4;end;

  X satisfies_DES implies X satisfies_SCH
 proof
  assume A365:X satisfies_DES; then X satisfies_TDES by AFF_2:26;
  then X satisfies_TDES_1 by AFF_2:17; then X satisfies_des_1 by AFF_2:27;
  then X satisfies_des by AFF_2:21; then A366:X satisfies_minor_SCH by Th6;
    X satisfies_major_SCH by A365,Th7; hence thesis by A366,Th2;end;
hence thesis by A1;end;

theorem Th9:
        X satisfies_pap iff X satisfies_minor_SCH*
proof
 A1:X satisfies_pap implies X satisfies_minor_SCH* proof
  assume A2:X satisfies_pap;
    now let a1,a2,a3,a4,b1,b2,b3,b4,M,N;
  assume A3:M // N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N &
         a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M
         & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N
         & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4;
   then A4:M is_line & N is_line by AFF_1:50;
     a1,a2 // b2,b1 & b2,b3 // a3,a2 by A3,AFF_1:13;
   then a1,b3 // a3,b1 by A2,A3,A4,AFF_2:def 13;
   then A5:b1,a3 // b3,a1 by AFF_1:13;
     a4,a1 // b1,b4 by A3,AFF_1:13;
   then a4,a3 // b3,b4 by A2,A3,A4,A5,AFF_2:def 13;
  hence a3,a4 // b3,b4 by AFF_1:13;end;
 hence thesis by Def5;end;
   X satisfies_minor_SCH* implies X satisfies_pap proof
  assume A6:X satisfies_minor_SCH*;
    now let M,N,a,b,c,a1,b1,c1;
  assume A7:M is_line & N is_line & a in M & b in M & c in M & M // N &
         M<>N & a1 in N & b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1;
   then A8:not a in N & not b in N & not c in N by AFF_1:59;
   A9:not a1 in M & not b1 in M & not c1 in M by A7,AFF_1:59;
   A10:a,b1 // a1,b & b,c1 // b1,c by A7,AFF_1:13;
     b1,b // b,b1 by AFF_1:11;
   then a,c1 // a1,c by A6,A7,A8,A9,A10,Def5;
  hence a,c1 // c,a1 by AFF_1:13;end;
 hence thesis by AFF_2:def 13;end;
hence thesis by A1;end;

theorem Th10:
          X satisfies_PAP iff X satisfies_major_SCH*
 proof
 A1:X satisfies_PAP implies X satisfies_major_SCH* proof
  assume A2:X satisfies_PAP; then A3:X satisfies_DES by AFF_2:25;
    now let o,a1,a2,a3,a4,b1,b2,b3,b4,M,N;
  assume A4:M is_line & N is_line & o in M & o in N & a1 in M & a3 in M &
         b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N &
         not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N &
         not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,b2 &
         a2,a1 // b2,b1 & a1,a4 // b1,b4;
  then A5:M // M & N // N by AFF_1:55;
  A6:now assume A7:a1<>a3 & a2<>a4;
   A8:b1<>b3 proof assume A9:b1=b3; A10:not LIN o,a2,a1 by A4,AFF_1:39;
      o,a1 // o,a3 by A4,A5,AFF_1:53; then A11:LIN o,a1,a3 by AFF_1:def 1;
      b2,b1 // a2,a3 by A4,A9,AFF_1:13; then a2,a1 // a2,a3 by A4,AFF_1:14;
   hence contradiction by A7,A10,A11,AFF_1:23;end;
     ex x,y,z st LIN x,y,z & x<>y & x<>z & y<>z proof assume A12:not thesis;
      o,a1 // o,a3 by A4,A5,AFF_1:53; then LIN o,a1,a3 by AFF_1:def 1;
    hence contradiction by A4,A7,A12;end;
    then consider d such that A13:LIN a2,a1,d & a2<>d & a1<>d by A4,TRANSLAC:2;
    A14:o<>d proof assume o=d; then LIN o,a1,a2 by A13,AFF_1:15;
    hence contradiction by A4,AFF_1:39;end;
      LIN o,d,d by AFF_1:16;
    then consider Y such that A15:Y is_line & o in Y & d in Y & d in Y by AFF_1
:33;
      ex d1 st LIN b1,b2,d1 & d1 in Y proof
     consider e1 such that A16:b1,b2 // b1,e1 & b1<>e1 by DIRAF:47;
     consider e2 such that A17:o,d // o,e2 & o<>e2 by DIRAF:47;
       not b1,e1 // o,e2 proof assume b1,e1 // o,e2; then b1,b2 // o,e2 by A16,
AFF_1:14; then b1,b2 // o,d by A17,AFF_1:14; then b2,b1 // o,d by AFF_1:13;
      then A18:a2,a1 // o,d by A4,AFF_1:14; a2,a1 // a2,d
      by A13,AFF_1:def 1;
      then a2,d // o,d by A4,A18,AFF_1:14; then d,o // d,a2 by AFF_1:13;
then LIN
 d,o,a2
      by AFF_1:def 1; then A19:LIN o,a2,d by AFF_1:15;
      A20:not LIN o,a1,a2 by A4,AFF_1:39;
        LIN a1,a2,d by A13,AFF_1:15; then a1,a2 // a1,d by AFF_1:def 1;
     hence contradiction by A13,A19,A20,AFF_1:23;end;
     then consider d1 such that A21:LIN b1,e1,d1 & LIN
 o,e2,d1 by AFF_1:74;take d1;
       o,e2 // o,d1 by A21,AFF_1:def 1; then o,d // o,d1 by A17,AFF_1:14;
then A22:     LIN o,d,d1 by AFF_1:def 1; b1,e1 // b1,d1
     by A21,AFF_1:def 1; then b1,b2 // b1,d1 by A16,AFF_1:14;
    hence thesis by A14,A15,A22,AFF_1:39,def 1;end;
    then consider d1 such that A23:LIN b1,b2,d1 & d1 in Y;
      ex c1 st c1 in N & a1,a4 // b2,c1 proof
     consider e1 such that A24:a1,a4 // b2,e1 & b2<>e1 by DIRAF:47;
     consider e2 such that A25:a2,a4 // a2,e2 & a2<>e2 by DIRAF:47;
       not b2,e1 // a2,e2 proof assume b2,e1 // a2,e2; then a1,a4 // a2,e2 by
A24,AFF_1:14; then a1,a4 // a2,a4 by A25,AFF_1:14; then a4,a2 // a4,a1 by AFF_1
:13; then LIN a4,a2,a1 by AFF_1:def 1;
     hence contradiction by A4,A7,AFF_1:39;end;
     then consider c1 such that A26:LIN b2,e1,c1 & LIN a2,e2,c1 by AFF_1:74;
take c1;
       a2,e2 // a2,c1 by A26,AFF_1:def 1; then a2,a4 // a2,c1 by A25,AFF_1:14;
then A27:     LIN a2,a4,c1 by AFF_1:def 1;
       b2,e1 // b2,c1 by A26,AFF_1:def 1;
    hence thesis by A4,A7,A24,A27,AFF_1:14,39;end;
    then consider c1 such that A28:c1 in N & a1,a4 // b2,c1;
      ex c2 st c2 in M & a2,a3 // b1,c2 proof
     consider e1 such that A29:a2,a3 // b1,e1 & b1<>e1 by DIRAF:47;
     consider e2 such that A30:a1,a3 // a1,e2 & a1<>e2 by DIRAF:47;
       not b1,e1 // a1,e2 proof assume b1,e1 // a1,e2; then a2,a3 // a1,e2 by
A29,AFF_1:14; then a2,a3 // a1,a3 by A30,AFF_1:14; then a3,a1 // a3,a2 by AFF_1
:13; then LIN a3,a1,a2 by AFF_1:def 1;
     hence contradiction by A4,A7,AFF_1:39;end;
     then consider c2 such that A31:LIN b1,e1,c2 & LIN a1,e2,c2 by AFF_1:74;
take c2;
       a1,e2 // a1,c2 by A31,AFF_1:def 1; then a1,a3 // a1,c2 by A30,AFF_1:14;
then A32:     LIN a1,a3,c2 by AFF_1:def 1;
       b1,e1 // b1,c2 by A31,AFF_1:def 1;hence thesis by A4,A7,A29,A32,AFF_1:14
,39;end;
    then consider c2 such that A33:c2 in M & a2,a3 // b1,c2;
    A34:M<>N & M<>Y & N<>Y proof assume A35:not thesis;
     A36:now assume A37: M=Y; LIN a1,d,a2 by A13,AFF_1:15;
     hence contradiction by A4,A13,A15,A37,AFF_1:39;end;
       now assume A38: N=Y; LIN a2,d,a1 by A13,AFF_1:15;
     hence contradiction by A4,A13,A15,A38,AFF_1:39;end;
    hence contradiction by A4,A35,A36;end;
      a2,d // b1,d1 proof A39:a2,a1 // a2,d & b1,b2 // b1,d1 by A13,A23,AFF_1:
def 1; then b2,b1 // b1,d1 by AFF_1:13; then a2,a1 // b1,d1
    by A4,AFF_1:14; hence thesis by A4,A39,AFF_1:14;end;
    then A40:d,a3 // d1,c2 by A3,A4,A14,A15,A23,A33,A34,AFF_2:def 4;
      a1,d // b2,d1 proof LIN a1,a2,d & LIN b2,b1,d1 by A13,A23,AFF_1:15;
     then A41:a1,a2 // a1,d & b2,b1 // b2,d1 by AFF_1:def 1; then a2,a1 // a1,
d by AFF_1:13; then b2,b1 // a1,d by A4,AFF_1:14;
    hence thesis by A4,A41,AFF_1:14;end;
    then d,a4 // d1,c1 by A3,A4,A14,A15,A23,A28,A34,AFF_2:def 4;
    then A42:a3,a4 // c2,c1 by A3,A4,A14,A15,A23,A28,A33,A34,A40,AFF_2:def 4;
    A43:c1<>c2 proof assume c1=c2; then a3,a2 // b1,c1 by A33,AFF_1:13;
     then A44:b3,b2 // b1,c1 by A4,AFF_1:14;
     A45:b1<>c1 proof assume b1=c1; then a1,a4 // a2,a1 by A4,A28,AFF_1:14;
      then a1,a4 // a1,a2 by AFF_1:13; then LIN a1,a4,a2 by AFF_1:def 1;
      then LIN a2,a4,a1 by AFF_1:15;hence contradiction by A4,A7,AFF_1:39;end
;
       b1,c1 // b3,b1 by A4,A5,A28,AFF_1:53; then b3,b1 // b3,b2 by A44,A45,
AFF_1:14;
     then LIN
 b3,b1,b2 by AFF_1:def 1;hence contradiction by A4,A8,AFF_1:39;end;
    A46:o<>c1 & o<>c2 proof assume A47:not thesis;
     A48:now assume o=c1; then A49:o,b2 // a1,a4 by A28,AFF_1:13;
       o,b2 // a1,a3 by A4,A5,AFF_1:53; then a1,a3 // a1,a4 by A4,A49,AFF_1:14
;
then LIN a1,a3,a4
      by AFF_1:def 1;hence contradiction by A4,A7,AFF_1:39;end;
       now assume o=c2; then A50:o,b1 // a2,a3 by A33,AFF_1:13; o,b1 // a2,
a4
by A4,A5,AFF_1:53; then a2,a4 // a2,a3 by A4,A50,AFF_1:14; then LIN
 a2,a4,a3 by AFF_1:def 1;hence contradiction by A4,A7,AFF_1:39;end;
    hence contradiction by A47,A48;end;
      b1,b4 // b2,c1 by A4,A28,AFF_1:14; then A51:b4,b1 // b2,c1 by AFF_1:13;
      a3,a2 // c2,b1 by A33,AFF_1:13; then b3,b2 // c2,b1 by A4,AFF_1:14;
    then b2,b3 // c2,b1 by AFF_1:13;
    then b4,b3 // c2,c1 by A2,A4,A28,A33,A46,A51,AFF_2:def 2;
    then b4,b3 // a3,a4 by A42,A43,AFF_1:14;
   hence a3,a4 // b3,b4 by AFF_1:13;end;
    now assume A52:a1=a3 or a2=a4;
   A53:now assume A54:a1=a3; A55:not LIN o,b2,b1 by A4,AFF_1:39;
      o,b1 // o,b3 by A4,A5,AFF_1:53; then A56:LIN o,b1,b3 by AFF_1:def 1;
      a2,a1 // b2,b3 by A4,A54,AFF_1:13; then b2,b1 // b2,b3 by A4,AFF_1:14;
    hence a3,a4 // b3,b4 by A4,A54,A55,A56,AFF_1:23;end;
     now assume A57:a2=a4; A58:not LIN o,b1,b2 by A4,AFF_1:39;
      o,b2 // o,b4 by A4,A5,AFF_1:53; then A59:LIN o,b2,b4 by AFF_1:def 1;
      a1,a4 // b1,b2 by A4,A57,AFF_1:13; then b1,b2 // b1,b4 by A4,AFF_1:14;
hence a3,a4 // b3,b4 by A4,A57,A58,A59,AFF_1:23;end;
  hence a3,a4 // b3,b4 by A52,A53;end;
  hence a3,a4 // b3,b4 by A6;end;
 hence thesis by Def6;end;
   X satisfies_major_SCH* implies X satisfies_PAP proof
  assume A60:X satisfies_major_SCH*;
    now let M,N,o,a,b,c,a1,b1,c1;
  assume A61:M is_line & N is_line & M<>N & o in M & o in N & o<>a & o<>a1
         & o<>b & o<>b1 & o<>c & o<>c1 & a in M & b in M & c in M & a1 in N &
         b1 in N & c1 in N & a,b1 // b,a1 & b,c1 // c,b1;
  A62:not a in N & not b in N & not c in N & not a1 in M & not b1 in M &
  not c1 in M proof assume A63:not thesis;
     o,a // o,a & o,b // o,b & o,c // o,c & o,a1 // o,a1 & o,b1 //
   o,b1 & o,c1 // o,c1
   by AFF_1:11; then M // N by A61,A63,AFF_1:52;
  hence contradiction by A61,AFF_1:59;end;
  A64:a,b1 // a1,b & b,c1 // b1,c by A61,AFF_1:13;
    b1,b // b,b1 by AFF_1:11; then a,c1 // a1,c by A60,A61,A62,A64,Def6;
  hence a,c1 // c,a1 by AFF_1:13;end;
 hence thesis by AFF_2:def 2;end;
hence thesis by A1;end;

theorem
          X satisfies_PPAP iff X satisfies_SCH*
 proof
 A1:X satisfies_PPAP implies X satisfies_SCH* proof
  assume X satisfies_PPAP;
  then X satisfies_PAP & X satisfies_pap by AFF_2:24;
  then X satisfies_major_SCH* & X satisfies_minor_SCH* by Th9,Th10;
 hence thesis by Th1;end;
   X satisfies_SCH* implies X satisfies_PPAP proof
  assume X satisfies_SCH*;
  then X satisfies_minor_SCH* & X satisfies_major_SCH* by Th1;
  then X satisfies_PAP & X satisfies_pap by Th9,Th10;
 hence thesis by AFF_2:24;end;
 hence thesis by A1;end;

theorem
         X satisfies_major_SCH* implies X satisfies_minor_SCH*
 proof assume X satisfies_major_SCH*;
 then X satisfies_PAP by Th10;
 then X satisfies_pap by AFF_2:23;
 hence thesis by Th9;end;

reserve X for OrtAfPl;
reserve o',a',a1',a2',a3',a4',b',b1',b2',b3',b4',c',c1'
 for Element of X;
reserve o,a,a1,a2,a3,a4,b,b1,b2,b3,b4,c,c1
        for Element of Af(X);
reserve M',N' for Subset of X;
reserve A,M,N for Subset of Af(X);

theorem
             Af(X) satisfies_SCH iff SCH_holds_in X
proof
A1:Af(X) satisfies_SCH implies SCH_holds_in X
 proof
  assume A2:Af(X) satisfies_SCH;
    now let a1',a2',a3',a4',b1',b2',b3',b4',M',N';
  assume A3:M' is_line & N' is_line & a1' in M' & a3' in M' & b1' in M' & b3'
in M'
           & a2' in N' & a4' in N' & b2' in N' & b4' in N' & not a4' in M' &
           not a2' in M' & not b2' in M' & not b4' in M' & not a1' in N' &
           not a3' in N' & not b1' in N' & not b3' in N' & a3',a2' // b3',b2' &
           a2',a1' // b2',b1' & a1',a4' // b1',b4';
  reconsider M=M',N=N' as Subset of Af(X) by ANALMETR:57;
  A4:M is_line & N is_line by A3,ANALMETR:58;
  reconsider a1=a1',a2=a2',a3=a3',a4=a4',b1=b1',b2=b2',b3=b3',b4=b4'
  as Element of Af(X) by ANALMETR:47;
    a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 by A3,ANALMETR:48;
  then a3,a4 // b3,b4 by A2,A3,A4,Def3;
  hence a3',a4' // b3',b4' by ANALMETR:48;end;
 hence thesis by CONMETR:def 6;end;
  SCH_holds_in X implies Af(X) satisfies_SCH
 proof
  assume A5:SCH_holds_in X;
    now let a1,a2,a3,a4,b1,b2,b3,b4,M,N;
  assume A6:M is_line & N is_line & a1 in M & a3 in M & b1 in M & b3 in M & a2
in N
           & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2
in M
           & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in
 N &
           a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4;
  reconsider M'=M,N'=N as Subset of X by ANALMETR:57;
  A7:M' is_line & N' is_line by A6,ANALMETR:58;
  reconsider a1'=a1,a2'=a2,a3'=a3,a4'=a4,b1'=b1,b2'=b2,b3'=b3,b4'=b4
  as Element of X by ANALMETR:47;
    a3',a2' // b3',b2' & a2',a1' // b2',b1' & a1',a4' // b1',b4'
  by A6,ANALMETR:48;
  then a3',a4' // b3',b4' by A5,A6,A7,CONMETR:def 6;
  hence a3,a4 // b3,b4 by ANALMETR:48;end;
 hence thesis by Def3;end;
hence thesis by A1;end;

theorem
             TDES_holds_in X iff Af(X) satisfies_TDES
 proof
   Af(X) satisfies_TDES implies TDES_holds_in X proof
  assume A1:Af(X) satisfies_TDES;
    now let o',a',a1',b',b1',c',c1';
  assume A2:o'<>a' & o'<>a1' & o'<>b' & o'<>b1' & o'<>c' & o'<>c1' &
           not LIN b',b1',a' & not LIN b',b1',c' & LIN o',a',a1' & LIN
 o',b',b1' &
           LIN
 o',c',c1' & a',b' // a1',b1' & a',b' // o',c' & b',c' // b1',c1';
  reconsider o=o',a=a',a1=a1',b=b',b1=b1',c =c',c1=c1' as Element of the
             carrier of Af(X) by ANALMETR:47;
  A3:not LIN b,b1,a & not LIN b,b1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1
     by A2,ANALMETR:55;
  A4:a,b // a1,b1 & a,b // o,c & b,c // b1,c1 by A2,ANALMETR:48;
  consider M such that A5:M is_line & o in M & c in M & c1 in M by A3,AFF_1:33;
  A6:M // M by A5,AFF_1:55;
  A7:not b in M proof assume b in M; then A8:o,b // b,c by A5,A6,AFF_1:53;
     LIN b,b1,o by A3,AFF_1:15; then b,b1 // b,o by AFF_1:def 1; then b,b1 //
o,b
   by AFF_1:13; then b,b1 // b,c by A2,A8,AFF_1:14;
  hence contradiction by A3,AFF_1:def 1;end;
  A9:o<>c & b<>a by A2,A3,AFF_1:16;
  A10:b,a // b1,a1 & b,c // b1,c1 by A4,AFF_1:13;
    b,a // o,c by A4,AFF_1:13; then b,a // M by A2,A5,AFF_1:41;
  then a,c // a1,c1 by A1,A3,A5,A7,A9,A10,AFF_2:def 7;
  hence a',c' // a1',c1' by ANALMETR:48;end;
 hence thesis by CONMETR:def 5;end;
 hence thesis by CONMETR:7;end;

theorem
             Af(X) satisfies_des iff des_holds_in X
 proof
   des_holds_in X implies Af(X) satisfies_des proof
  assume A1:des_holds_in X;
    now let A,M,N,a,b,c,a1,b1,c1;
  assume A2:A // M & A // N & a in A & a1 in A &
    b in M & b1 in M & c in N & c1 in N & A is_line & M is_line &
    N is_line & A<>M & A<>N & a,b // a1,b1 & a,c // a1,c1;
  reconsider a'=a,a1'=a1,b'=b,b1'=b1,c'=c,c1'=c1
             as Element of X by ANALMETR:47;
    b,c // b1,c1
  proof assume A3:not b,c // b1,c1;
   A4:a<>a1 proof assume A5:a=a1;
    A6:b=b1 proof assume A7:b<>b1; LIN a,b,b1 by A2,A5,AFF_1:def 1; then LIN
 b,b1,a
    by AFF_1:15; then a in M by A2,A7,AFF_1:39;
    hence contradiction by A2,AFF_1:59;end;
      c =c1 proof assume A8:c <>c1; LIN a,c,c1 by A2,A5,AFF_1:def 1;
    then LIN c,c1,a by AFF_1:15; then a in N by A2,A8,AFF_1:39;
    hence contradiction by A2,AFF_1:59;end;
    hence contradiction by A3,A6,AFF_1:11;end;
   A9:not LIN a',a1',b' & not LIN a',a1',c' proof
    assume LIN a',a1',b' or LIN a',a1',c'; then LIN a,a1,b or LIN
 a,a1,c by ANALMETR:55;
    then b in A or c in A by A2,A4,AFF_1:39;
   hence contradiction by A2,AFF_1:59;end;
     a,a1 // b,b1 & a,a1 // c,c1 by A2,AFF_1:53;
   then A10:a',a1' // b',b1' & a',a1' // c',c1' by ANALMETR:48;
     a',b' // a1',b1' & a',c' // a1',c1' by A2,ANALMETR:48;
   then b',c' // b1',c1' by A1,A9,A10,CONMETR:def 8;hence contradiction by A3,
ANALMETR:48;end;
  hence b,c // b1,c1;end;
  hence thesis by AFF_2:def 11;end;
 hence thesis by CONMETR:8;end;

theorem
            PAP_holds_in X iff Af(X) satisfies_PAP
proof
A1:PAP_holds_in X implies Af(X) satisfies_PAP
proof
assume A2:PAP_holds_in X;
  now let M,N,o,a,b,c,a1,b1,c1;
assume A3: M is_line & N is_line & M<>N &
   o in M & o in N & o<>a & o<>a1 & o<>b & o<>b1 & o<>c & o<>c1 & a in M &
   b in M & c in M & a1 in N & b1 in N & c1 in N &
   a,b1 // b,a1 & b,c1 // c,b1;
   reconsider M'=M,N'=N as Subset of X by ANALMETR:57;
   reconsider a'=a,b'=b,c'=c,a1'=a1,b1'=b1,c1'=c1
               as Element of X by ANALMETR:47;
   A4:M' is_line & N' is_line by A3,ANALMETR:58;
     b,a1 // a,b1 by A3,AFF_1:13;
   then A5:b',a1' // a',b1' & b',c1' // c',b1' by A3,ANALMETR:48;
    not c1' in M' & not b' in N' proof assume c1' in M' or b' in N';
    then A6:o,c1 // M or o,b // N by A3,AFF_1:66; o,c1 // N & o,b // M
    by A3,AFF_1:66;
    then M // N by A3,A6,AFF_1:67;
   hence contradiction by A3,AFF_1:59;end;
   then a',c1' // c',a1' by A2,A3,A4,A5,CONMETR:def 2;
   hence a,c1 // c,a1 by ANALMETR:48;end;
hence thesis by AFF_2:def 2;end;
  Af(X) satisfies_PAP implies PAP_holds_in X
proof
assume A7:Af(X) satisfies_PAP;
  now let o',a1',a2',a3',b1',b2',b3',M',N';
assume A8:M' is_line & N' is_line & o' in M' & a1' in M' & a2' in M' & a3' in
 M'
    & o' in N' & b1' in N' & b2' in N' & b3' in N' & not b2' in M' & not a3' in
 N'
    & o'<>a1' & o'<>a2' & o'<>a3' & o'<>b1' & o'<>b2' & o'<>b3' &
    a3',b2' // a2',b1' & a3',b3' // a1',b1';
    reconsider M=M',N=N' as Subset of Af(X) by ANALMETR:57;
    reconsider a1=a1',a2=a2',a3=a3',b1=b1',b2=b2',b3=b3'
               as Element of Af(X) by ANALMETR:47;
   A9:M is_line & N is_line by A8,ANALMETR:58;
     now assume M<>N;
     a3,b2 // a2,b1 & a3,b3 // a1,b1 by A8,ANALMETR:48;
   then a3,b2 // a2,b1 & a1,b1 // a3,b3 by AFF_1:13;
   then a1,b2 // a2,b3 by A7,A8,A9,AFF_2:def 2;
   hence a1',b2' // a2',b3' by ANALMETR:48;end;
   hence a1',b2' // a2',b3' by A8;end;
hence thesis by CONMETR:def 2;end;
hence thesis by A1;end;

theorem
             DES_holds_in X iff Af(X) satisfies_DES
proof
A1:DES_holds_in X implies Af(X) satisfies_DES
 proof assume A2:DES_holds_in X;
    now let A,M,N,o,a,b,c,a1,b1,c1;
  assume A3:o in A & o in M & o in N & o<>a & o<>b & o<>c & a in A & a1 in A &
         b in M & b1 in M & c in N & c1 in
 N & A is_line & M is_line & N is_line
         & A<>M & A<>N & a,b // a1,b1 & a,c // a1,c1;
  assume A4:not b,c // b1,c1;
  reconsider o'=o,a'=a,a1'=a1,b'=b,b1'=b1,c'=c,c1'=c1
             as Element of X by ANALMETR:47;
  A5:A // A & M // M & N // N by A3,AFF_1:55;
  A6: LIN o',a',a1' & LIN o',b',b1' & LIN o',c',c1' proof
     o,a // o,a1 & o,b // o,b1 & o,c // o,c1 by A3,A5,AFF_1:53; then LIN o,a,
a1
&
   LIN o,b,b1 & LIN o,c,c1 by AFF_1:def 1;hence thesis by ANALMETR:55;end;
  A7:o'<>a1' & o'<>b1' & o'<>c1' proof assume A8:not thesis;
   A9:now assume A10:o'=a1';
    A11:o=b1 proof assume A12:o<>b1;
     A13:not LIN b,a,o proof assume LIN b,a,o; then LIN
 o,a,b by AFF_1:15; then b in A
      by A3,AFF_1:39; then o,b // A & o,b // M by A3,AFF_1:66; then A // M
by A3,AFF_1:67;hence contradiction by A3,AFF_1:59;end;
       LIN o,b,b1 by A6,ANALMETR:55; then A14:LIN b,o,b1 by AFF_1:15;
       a,o // a,b1 proof A15:o,b1 // o,b by A3,A5,AFF_1:53; then a,b // o,b by
A3,A10,A12,AFF_1:14; then b,a // b,o by AFF_1:13;
      then LIN b,a,o by AFF_1:def 1; then LIN
 o,a,b by AFF_1:15; then o,a // o,b by AFF_1:def 1; then o,a // o,b1 by A3,A15,
AFF_1:14; then LIN o,a,b1 by AFF_1:def 1; then LIN a,o,b1
      by AFF_1:15;hence thesis by AFF_1:def 1;end;
     hence contradiction by A12,A13,A14,AFF_1:23;end;
      o=c1 proof assume A16:o<>c1;
     A17:not LIN c,a,o proof assume LIN c,a,o; then LIN o,a,c by AFF_1:15;
then c in A by A3,AFF_1:39; then o,c // A & o,c // N by A3,AFF_1:66; then A
// N by A3,AFF_1:67;hence contradiction by A3,AFF_1:59;end;
       LIN o,c,c1 by A6,ANALMETR:55; then A18:LIN c,o,c1 by AFF_1:15;
       a,o // a,c1 proof A19:o,c // o,c1 by A3,A5,AFF_1:53; then a,c // o,c by
A3,A10,A16,AFF_1:14; then c,a // c,o by AFF_1:13;
      then LIN c,a,o by AFF_1:def 1; then LIN o,a,c by AFF_1:15; then o,a //
o,c by AFF_1:def 1; then o,a // o,c1 by A3,A19,AFF_1:14; then LIN o,a,c1 by
AFF_1:def 1; then LIN a,o,c1 by AFF_1:15;hence thesis by AFF_1:def 1;end;
     hence contradiction by A16,A17,A18,AFF_1:23;end;
    hence contradiction by A4,A11,AFF_1:12;end;

   A20:now assume A21:o'=b1';
    A22:not LIN a,b,o proof assume LIN a,b,o; then LIN
 o,a,b by AFF_1:15; then b in A by A3,AFF_1:39; then o,b // A & o,b // M by A3,
AFF_1:66; then A // M by A3,AFF_1:67;hence contradiction by A3,AFF_1:59;
end;
      LIN o,a,a1 by A6,ANALMETR:55; then A23:LIN a,o,a1 by AFF_1:15;
      b,o // b,a1 proof A24:a1,o // a,o by A3,A5,AFF_1:53;
     then a,b // a,o by A3,A9,A21,AFF_1:14; then LIN a,b,o by AFF_1:def 1;
     then LIN o,b,a by AFF_1:15; then o,b // o,a by AFF_1:def 1; then o,b //
a,o by AFF_1:13; then o,b // a1,o by A3,A24,AFF_1:14; then o,b // o,a1 by AFF_1
:13;
     then LIN o,b,a1 by AFF_1:def 1; then LIN b,o,a1 by AFF_1:15;hence
 thesis by AFF_1:def 1;end; hence contradiction by A9,A22,A23,AFF_1:23;end;
     now assume A25:o'=c1';
    A26:not LIN a,c,o proof assume LIN a,c,o; then LIN
 o,a,c by AFF_1:15; then c in A by A3,AFF_1:39; then o,c // A & o,c // N by A3,
AFF_1:66; then A // N by A3,AFF_1:67;hence contradiction by A3,AFF_1:59;
end;
     LIN o,a,a1 by A6,ANALMETR:55; then A27:LIN a,o,a1 by AFF_1:15;
     c,o // c,a1 proof A28:a1,o // a,o by A3,A5,AFF_1:53;
     then a,c // a,o by A3,A9,A25,AFF_1:14; then LIN a,c,o by AFF_1:def 1;
     then LIN o,c,a by AFF_1:15; then o,c // o,a by AFF_1:def 1; then o,c //
a,o by AFF_1:13; then o,c // a1,o by A3,A28,AFF_1:14; then o,c // o,a1 by AFF_1
:13;
     then LIN o,c,a1 by AFF_1:def 1; then LIN c,o,a1 by AFF_1:15;hence
 thesis by AFF_1:def 1;end;
    hence contradiction by A9,A26,A27,AFF_1:23;end;
  hence contradiction by A8,A9,A20;end;
  A29:not LIN b',b1',a' & not LIN a',a1',c' proof assume LIN b',b1',a' or LIN
 a',a1',c';
   then A30:LIN b,b1,a or LIN a,a1,c by ANALMETR:55;
   A31:a<>a1 proof assume A32:a=a1;
    A33:b=b1 proof assume A34:b<>b1;A35:not LIN o,a,b proof assume LIN
 o,a,b;
      then b in A by A3,AFF_1:39; then A36:o,b // A by A3,AFF_1:66; o,b // M
by A3,AFF_1:66; then A // M by A3,A36,AFF_1:67;
     hence contradiction by A3,AFF_1:59;end; LIN o,b,b1 by A6,ANALMETR:55;
hence contradiction by A3,A32,A34,A35,AFF_1:23;end;
      c =c1 proof assume A37:c <>c1;A38:not LIN o,a,c proof assume LIN o,a,c;
      then c in A by A3,AFF_1:39; then A39:o,c // A by A3,AFF_1:66; o,c // N
by A3,AFF_1:66; then A // N by A3,A39,AFF_1:67;
     hence contradiction by A3,AFF_1:59;end; LIN o,c,c1 by A6,ANALMETR:55;
hence contradiction by A3,A32,A37,A38,AFF_1:23;end;
    hence contradiction by A4,A33,AFF_1:11;end;
     b<>b1 proof assume A40:b=b1;
    A41:not LIN o,b,a proof assume LIN o,b,a; then a in M by A3,AFF_1:39;
     then A42:o,a // M by A3,AFF_1:66; o,a // A by A3,AFF_1:66; then A // M
by A3,A42,AFF_1:67;hence contradiction by A3,AFF_1:59;end;
    A43:LIN o,a,a1 by A6,ANALMETR:55;
      b,a // b,a1 by A3,A40,AFF_1:13;
    hence contradiction by A31,A41,A43,AFF_1:23;end;
   then a in M or c in A by A3,A30,A31,AFF_1:39; then A44:o,a // M
   or o,c // A by A3,AFF_1:66; o,a // A & o,c // N by A3,AFF_1:66; then A //
M or A // N by A3,A44,AFF_1:67;hence contradiction by A3,AFF_1:59;end;
    a',b' // a1',b1' & a',c' // a1',c1' by A3,ANALMETR:48;
  then b',c' // b1',c1' by A2,A3,A6,A7,A29,CONAFFM:def 1;
  hence contradiction by A4,ANALMETR:48;end;
  hence thesis by AFF_2:def 4;end;
  Af(X) satisfies_DES implies DES_holds_in X
 proof
 assume A45:Af(X) satisfies_DES;
   now let o',a',a1',b',b1',c',c1';
 assume A46:o'<>a' & o'<>a1' & o'<>b' & o'<>b1' & o'<>c' & o'<>c1' &
        not LIN b',b1',a' & not LIN a',a1',c' & LIN o',a',a1' & LIN o',b',b1' &
        LIN o',c',c1' & a',b' // a1',b1' & a',c' // a1',c1';
 reconsider o=o',a=a',a1=a1',b=b',b1=b1',c =c',c1=c1'
            as Element of Af(X) by ANALMETR:47;
 A47:not LIN b,b1,a & not LIN a,a1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1
    by A46,ANALMETR:55;
 then consider A such that A48:A is_line & o in A & a in A & a1 in
 A by AFF_1:33;
 consider M such that A49:M is_line & o in M & b in M & b1 in
 M by A47,AFF_1:33;
 consider N such that A50:N is_line & o in N & c in N & c1 in
 N by A47,AFF_1:33;
 A51:A // A & M // M & N // N by A48,A49,A50,AFF_1:55;
 A52:A<>M & A<>N proof assume not thesis;
  then b,b1 // b,a or a,a1 // a,c by A48,A49,A50,A51,AFF_1:53;hence
 contradiction by A47,AFF_1:def 1;end;
   a,b // a1,b1 & a,c // a1,c1 by A46,ANALMETR:48;
 then b,c // b1,c1 by A45,A46,A48,A49,A50,A52,AFF_2:def 4;
 hence b',c' // b1',c1' by ANALMETR:48;end;
 hence thesis by CONAFFM:def 1;end;
hence thesis by A1;end;

Back to top