:: Shear Theorems and Their Role in Affine Geometry
:: by Jolanta \'Swierzy\'nska and Bogdan \'Swierzy\'nski
::
:: Received April 19, 1991
:: Copyright (c) 1991-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies DIRAF, SUBSET_1, ANALOAF, AFF_1, AFF_2, ANALMETR, CONMETR,
CONAFFM, CONMETR1;
notations STRUCT_0, ANALOAF, DIRAF, AFF_1, ANALMETR, AFF_2, CONAFFM, CONMETR;
constructors AFF_1, AFF_2, CONAFFM, CONMETR;
registrations STRUCT_0, ANALMETR;
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
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;
end;
definition
let X;
attr X is satisfying_major_Scherungssatz means
for o,a1,a2,a3,a4,b1,
b2,b3,b4,M,N st M is being_line & N is being_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;
end;
definition
let X;
attr X is satisfying_Scherungssatz means
for a1,a2,a3,a4,b1,b2,b3,b4,
M,N st M is being_line & N is being_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;
end;
definition
let X;
attr X is satisfying_indirect_Scherungssatz means
for a1,a2,a3,a4,b1,
b2,b3,b4,M,N st M is being_line & N is being_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;
end;
definition
let X;
attr X is satisfying_minor_indirect_Scherungssatz means
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;
end;
definition
let X;
attr X is satisfying_major_indirect_Scherungssatz means
for o,a1,a2,
a3,a4,b1,b2,b3,b4,M,N st M is being_line & N is being_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;
end;
theorem Th1:
X is satisfying_indirect_Scherungssatz iff X is
satisfying_minor_indirect_Scherungssatz & X is
satisfying_major_indirect_Scherungssatz
proof
A1: X is satisfying_indirect_Scherungssatz implies X is
satisfying_minor_indirect_Scherungssatz
proof
assume
A2: X is satisfying_indirect_Scherungssatz;
now
let a1,a2,a3,a4,b1,b2,b3,b4,M,N;
assume that
A3: M // N and
A4: a1 in M and
A5: a3 in M and
A6: b2 in M and
A7: b4 in M and
A8: a2 in N and
A9: a4 in N and
A10: b1 in N and
A11: b3 in N and
A12: not a4 in M and
A13: not a2 in M and
A14: not b1 in M and
A15: not b3 in M and
A16: not a1 in N and
A17: not a3 in N and
A18: not b2 in N and
A19: not b4 in N and
A20: a3,a2 // b3,b2 and
A21: a2,a1 // b2,b1 and
A22: a1,a4 // b1,b4;
A23: N is being_line by A3,AFF_1:36;
M is being_line by A3,AFF_1:36;
hence a3,a4 // b3,b4 by A2,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,A15,A16
,A17,A18,A19,A20,A21,A22,A23;
end;
hence thesis;
end;
A24: X is satisfying_minor_indirect_Scherungssatz & X is
satisfying_major_indirect_Scherungssatz implies X is
satisfying_indirect_Scherungssatz
proof
assume that
A25: X is satisfying_minor_indirect_Scherungssatz and
A26: X is satisfying_major_indirect_Scherungssatz;
now
let a1,a2,a3,a4,b1,b2,b3,b4,M,N;
assume that
A27: M is being_line and
A28: N is being_line and
A29: a1 in M and
A30: a3 in M and
A31: b2 in M and
A32: b4 in M and
A33: a2 in N and
A34: a4 in N and
A35: b1 in N and
A36: b3 in N and
A37: not a4 in M and
A38: not a2 in M and
A39: not b1 in M and
A40: not b3 in M and
A41: not a1 in N and
A42: not a3 in N and
A43: not b2 in N and
A44: not b4 in N and
A45: a3,a2 // b3,b2 and
A46: a2,a1 // b2,b1 and
A47: a1,a4 // b1,b4;
now
assume not M // N;
then ex o st o in M & o in N by A27,A28,AFF_1:58;
hence a3,a4 // b3,b4 by A26,A27,A28,A29,A30,A31,A32,A33,A34,A35,A36,A37
,A38,A39,A40,A41,A42,A43,A44,A45,A46,A47;
end;
hence
a3,a4 // b3,b4 by A25,A29,A30,A31,A32,A33,A34,A35,A36,A37,A38,A39,A40,A41
,A42,A43,A44,A45,A46,A47;
end;
hence thesis;
end;
thus thesis by A1,A24;
end;
theorem Th2:
X is satisfying_Scherungssatz iff X is
satisfying_minor_Scherungssatz & X is satisfying_major_Scherungssatz
proof
A1: X is satisfying_Scherungssatz implies X is satisfying_minor_Scherungssatz
proof
assume
A2: X is satisfying_Scherungssatz;
now
let a1,a2,a3,a4,b1,b2,b3,b4,M,N;
assume that
A3: M // N and
A4: a1 in M and
A5: a3 in M and
A6: b1 in M and
A7: b3 in M and
A8: a2 in N and
A9: a4 in N and
A10: b2 in N and
A11: b4 in N and
A12: not a4 in M and
A13: not a2 in M and
A14: not b2 in M and
A15: not b4 in M and
A16: not a1 in N and
A17: not a3 in N and
A18: not b1 in N and
A19: not b3 in N and
A20: a3,a2 // b3,b2 and
A21: a2,a1 // b2,b1 and
A22: a1,a4 // b1,b4;
A23: N is being_line by A3,AFF_1:36;
M is being_line by A3,AFF_1:36;
hence a3,a4 // b3,b4 by A2,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,A15,A16
,A17,A18,A19,A20,A21,A22,A23;
end;
hence thesis;
end;
A24: X is satisfying_minor_Scherungssatz & X is
satisfying_major_Scherungssatz implies X is satisfying_Scherungssatz
proof
assume that
A25: X is satisfying_minor_Scherungssatz and
A26: X is satisfying_major_Scherungssatz;
now
let a1,a2,a3,a4,b1,b2,b3,b4,M,N;
assume that
A27: M is being_line and
A28: N is being_line and
A29: a1 in M and
A30: a3 in M and
A31: b1 in M and
A32: b3 in M and
A33: a2 in N and
A34: a4 in N and
A35: b2 in N and
A36: b4 in N and
A37: not a4 in M and
A38: not a2 in M and
A39: not b2 in M and
A40: not b4 in M and
A41: not a1 in N and
A42: not a3 in N and
A43: not b1 in N and
A44: not b3 in N and
A45: a3,a2 // b3,b2 and
A46: a2,a1 // b2,b1 and
A47: a1,a4 // b1,b4;
now
assume not M // N;
then ex o st o in M & o in N by A27,A28,AFF_1:58;
hence a3,a4 // b3,b4 by A26,A27,A28,A29,A30,A31,A32,A33,A34,A35,A36,A37
,A38,A39,A40,A41,A42,A43,A44,A45,A46,A47;
end;
hence
a3,a4 // b3,b4 by A25,A29,A30,A31,A32,A33,A34,A35,A36,A37,A38,A39,A40,A41
,A42,A43,A44,A45,A46,A47;
end;
hence thesis;
end;
thus thesis by A1,A24;
end;
theorem Th3:
X is satisfying_minor_indirect_Scherungssatz implies X is
satisfying_minor_Scherungssatz
proof
assume
A1: X is satisfying_minor_indirect_Scherungssatz;
now
let a1,a2,a3,a4,b1,b2,b3,b4,M,N;
assume that
A2: M // N and
A3: a1 in M and
A4: a3 in M and
A5: b1 in M and
A6: b3 in M and
A7: a2 in N and
A8: a4 in N and
A9: b2 in N and
A10: b4 in N and
A11: not a4 in M and
A12: not a2 in M and
A13: not b2 in M and
A14: not b4 in M and
A15: not a1 in N and
A16: not a3 in N and
A17: not b1 in N and
A18: not b3 in N and
A19: a3,a2 // b3,b2 and
A20: a2,a1 // b2,b1 and
A21: a1,a4 // b1,b4;
A22: N is being_line by A2,AFF_1:36;
then consider d1 such that
a2<>d1 and
A23: d1 in N by AFF_1:20;
A24: not d1 in M by A2,A8,A11,A23,AFF_1:45;
A25: M is being_line by A2,AFF_1:36;
ex d2 st d2 in M & a2,a1 // d2,d1
proof
consider e1 such that
A26: a1<>e1 and
A27: e1 in M by A25,AFF_1:20;
consider e2 such that
A28: a2,a1 // d1,e2 and
A29: d1<>e2 by DIRAF:40;
not a1,e1 // d1,e2
proof
assume a1,e1 // d1,e2;
then a1,e1 // a2,a1 by A28,A29,AFF_1:5;
then a1,e1 // a1,a2 by AFF_1:4;
then LIN a1,e1,a2 by AFF_1:def 1;
hence contradiction by A3,A12,A25,A26,A27,AFF_1:25;
end;
then consider d2 such that
A30: LIN a1,e1,d2 and
A31: LIN d1,e2,d2 by AFF_1:60;
take d2;
d1,e2 // d1,d2 by A31,AFF_1:def 1;
then a2,a1 // d1,d2 by A28,A29,AFF_1:5;
hence thesis by A3,A25,A26,A27,A30,AFF_1:4,25;
end;
then consider d2 such that
A32: d2 in M and
A33: a2,a1 // d2,d1;
A34: not d2 in N by A2,A8,A11,A32,AFF_1:45;
ex d3 st d3 in N & a3,a2 // d3,d2
proof
consider e1 such that
A35: a2<>e1 and
A36: e1 in N by A22,AFF_1:20;
consider e2 such that
A37: a3,a2 // d2,e2 and
A38: d2<>e2 by DIRAF:40;
not a2,e1 // d2,e2
proof
assume a2,e1 // d2,e2;
then a2,e1 // a3,a2 by A37,A38,AFF_1:5;
then a2,e1 // a2,a3 by AFF_1:4;
then LIN a2,e1,a3 by AFF_1:def 1;
hence contradiction by A7,A16,A22,A35,A36,AFF_1:25;
end;
then consider d3 such that
A39: LIN a2,e1,d3 and
A40: LIN d2,e2,d3 by AFF_1:60;
take d3;
d2,e2 // d2,d3 by A40,AFF_1:def 1;
then a3,a2 // d2,d3 by A37,A38,AFF_1:5;
hence thesis by A7,A22,A35,A36,A39,AFF_1:4,25;
end;
then consider d3 such that
A41: d3 in N and
A42: a3,a2 // d3,d2;
A43: not d3 in M by A2,A8,A11,A41,AFF_1:45;
ex d4 st d4 in M & a1,a4 // d1,d4
proof
consider e1 such that
A44: a1<>e1 and
A45: e1 in M by A25,AFF_1:20;
consider e2 such that
A46: a1,a4 // d1,e2 and
A47: d1<>e2 by DIRAF:40;
not a1,e1 // d1,e2
proof
assume a1,e1 // d1,e2;
then a1,e1 // a1,a4 by A46,A47,AFF_1:5;
then LIN a1,e1,a4 by AFF_1:def 1;
hence contradiction by A3,A11,A25,A44,A45,AFF_1:25;
end;
then consider d4 such that
A48: LIN a1,e1,d4 and
A49: LIN d1,e2,d4 by AFF_1:60;
take d4;
d1,e2 // d1,d4 by A49,AFF_1:def 1;
hence thesis by A3,A25,A44,A45,A46,A47,A48,AFF_1:5,25;
end;
then consider d4 such that
A50: d4 in M and
A51: a1,a4 // d1,d4;
A52: not d4 in N by A2,A8,A11,A50,AFF_1:45;
A53: b2,b1 // d2,d1 by A3,A12,A20,A33,AFF_1:5;
A54: b1,b4 // d1,d4 by A3,A11,A21,A51,AFF_1:5;
b3,b2 // d3,d2 by A4,A12,A19,A42,AFF_1:5;
then
A55: b3,b4 // d3,d4 by A1,A2,A5,A6,A9,A10,A13,A14,A17,A18,A23,A32,A41,A50,A24
,A43,A34,A52,A53,A54;
a3,a4 // d3,d4 by A1,A2,A3,A4,A7,A8,A11,A12,A15,A16,A23,A32,A33,A41,A42,A50
,A51,A24,A43,A34,A52;
hence a3,a4 // b3,b4 by A50,A43,A55,AFF_1:5;
end;
hence thesis;
end;
theorem Th4:
X is satisfying_major_indirect_Scherungssatz implies X is
satisfying_major_Scherungssatz
proof
assume
A1: X is satisfying_major_indirect_Scherungssatz;
now
let o,a1,a2,a3,a4,b1,b2,b3,b4,M,N;
assume that
A2: M is being_line and
A3: N is being_line and
A4: o in M and
A5: o in N and
A6: a1 in M and
A7: a3 in M and
A8: b1 in M and
A9: b3 in M and
A10: a2 in N and
A11: a4 in N and
A12: b2 in N and
A13: b4 in N and
A14: not a4 in M and
A15: not a2 in M and
A16: not b2 in M and
A17: not b4 in M and
A18: not a1 in N and
A19: not a3 in N and
A20: not b1 in N and
A21: not b3 in N and
A22: a3,a2 // b3,b2 and
A23: a2,a1 // b2,b1 and
A24: a1,a4 // b1,b4;
A25: now
assume that
A26: a1<>a3 and
A27: a2<>a4;
consider d1 such that
A28: o<>d1 and
A29: d1 in N by A4,A11,A14;
A30: ex d4 st d4 in M & a1,a4 // d1,d4
proof
consider e1 such that
A31: o<>e1 and
A32: e1 in M by A5,A6,A18;
consider e2 such that
A33: a1,a4 // d1,e2 and
A34: d1<>e2 by DIRAF:40;
not o,e1 // d1,e2
proof
assume o,e1 // d1,e2;
then
A35: o,e1 // a1,a4 by A33,A34,AFF_1:5;
o,e1 // a1,a3 by A2,A4,A6,A7,A32,AFF_1:39,41;
then a1,a3 // a1,a4 by A31,A35,AFF_1:5;
then LIN a1,a3,a4 by AFF_1:def 1;
hence contradiction by A2,A6,A7,A14,A26,AFF_1:25;
end;
then consider d4 such that
A36: LIN o,e1,d4 and
A37: LIN d1,e2,d4 by AFF_1:60;
take d4;
d1,e2 // d1,d4 by A37,AFF_1:def 1;
hence thesis by A2,A4,A31,A32,A33,A34,A36,AFF_1:5,25;
end;
A38: ex d2 st d2 in M & a2,a1 // d2,d1
proof
consider e1 such that
A39: o<>e1 and
A40: e1 in M by A5,A6,A18;
consider e2 such that
A41: a2,a1 // d1,e2 and
A42: d1<>e2 by DIRAF:40;
not o,e1 // d1,e2
proof
assume o,e1 // d1,e2;
then
A43: o,e1 // a2,a1 by A41,A42,AFF_1:5;
o,e1 // a1,a3 by A2,A4,A6,A7,A40,AFF_1:39,41;
then a1,a3 // a2,a1 by A39,A43,AFF_1:5;
then a1,a3 // a1,a2 by AFF_1:4;
then LIN a1,a3,a2 by AFF_1:def 1;
hence contradiction by A2,A6,A7,A15,A26,AFF_1:25;
end;
then consider d2 such that
A44: LIN o,e1,d2 and
A45: LIN d1,e2,d2 by AFF_1:60;
take d2;
d1,e2 // d1,d2 by A45,AFF_1:def 1;
then a2,a1 // d1,d2 by A41,A42,AFF_1:5;
hence thesis by A2,A4,A39,A40,A44,AFF_1:4,25;
end;
consider d4 such that
A46: d4 in M and
A47: a1,a4 // d1,d4 by A30;
consider d2 such that
A48: d2 in M and
A49: a2,a1 // d2,d1 by A38;
A50: b2,b1 // d2,d1 by A6,A15,A23,A49,AFF_1:5;
ex d3 st d3 in N & a3,a2 // d3,d2
proof
consider e1 such that
A51: o<>e1 and
A52: e1 in N by A4,A11,A14;
consider e2 such that
A53: a3,a2 // d2,e2 and
A54: d2<>e2 by DIRAF:40;
not o,e1 // d2,e2
proof
assume o,e1 // d2,e2;
then
A55: o,e1 // a3,a2 by A53,A54,AFF_1:5;
o,e1 // a2,a4 by A3,A5,A10,A11,A52,AFF_1:39,41;
then a2,a4 // a3,a2 by A51,A55,AFF_1:5;
then a2,a4 // a2,a3 by AFF_1:4;
then LIN a2,a4,a3 by AFF_1:def 1;
hence contradiction by A3,A10,A11,A19,A27,AFF_1:25;
end;
then consider d3 such that
A56: LIN o,e1,d3 and
A57: LIN d2,e2,d3 by AFF_1:60;
take d3;
d2,e2 // d2,d3 by A57,AFF_1:def 1;
then a3,a2 // d2,d3 by A53,A54,AFF_1:5;
hence thesis by A3,A5,A51,A52,A56,AFF_1:4,25;
end;
then consider d3 such that
A58: d3 in N and
A59: a3,a2 // d3,d2;
A60: d2<>o & d3<>o & d4<>o
proof
A61: now
assume
A62: d4=o;
d1,o // a2,a4 by A3,A5,A10,A11,A29,AFF_1:39,41;
then a1,a4 // a2,a4 by A28,A47,A62,AFF_1:5;
then a4,a2 // a4,a1 by AFF_1:4;
then LIN a4, a2,a1 by AFF_1:def 1;
hence contradiction by A3,A10,A11,A18,A27,AFF_1:25;
end;
A63: now
assume
A64: d2=o;
o,d1 // a2,a4 by A3,A5,A10,A11,A29,AFF_1:39,41;
then a2,a4 // a2,a1 by A28,A49,A64,AFF_1:5;
then LIN a2,a4,a1 by AFF_1:def 1;
hence contradiction by A3,A10,A11,A18,A27,AFF_1:25;
end;
A65: now
assume
A66: d3=o;
o,d2 // a3,a1 by A2,A4,A6,A7,A48,AFF_1:39,41;
then a3,a1 // a3,a2 by A59,A63,A66,AFF_1:5;
then LIN a3,a1,a2 by AFF_1:def 1;
hence contradiction by A2,A6,A7,A15,A26,AFF_1:25;
end;
assume not thesis;
hence contradiction by A63,A65,A61;
end;
A67: not d1 in M & not d3 in M & not d2 in N & not d4 in N
proof
assume not thesis;
then
A68: o,d1 // M or o,d3 // M or o,d2 // N or o,d4 // N by A2,A3,A4,A5,
AFF_1:52;
A69: o,d3 // N by A3,A5,A58,AFF_1:52;
A70: o,d4 // M by A2,A4,A46,AFF_1:52;
A71: o,d2 // M by A2,A4,A48,AFF_1:52;
o,d1 // N by A3,A5,A29,AFF_1:52;
hence contradiction by A4,A5,A11,A14,A28,A60,A68,A69,A71,A70,AFF_1:45
,53;
end;
A72: b1,b4 // d1,d4 by A6,A14,A24,A47,AFF_1:5;
A73: d1<>d2 & d2<>d3 & d3<>d4 & d4<>d1
proof
assume not thesis;
then
A74: o,d1 // M or o,d3 // M by A2,A4,A48,A46,AFF_1:52;
A75: o,d3 // N by A3,A5,A58,AFF_1:52;
o,d1 // N by A3,A5,A29,AFF_1:52;
hence contradiction by A4,A5,A11,A14,A28,A60,A74,A75,AFF_1:45,53;
end;
b3,b2 // d3,d2 by A7,A15,A22,A59,AFF_1:5;
then
A76: b3,b4 // d3,d4 by A1,A2,A3,A4,A5,A8,A9,A12,A13,A16,A17,A20,A21,A29,A48
,A58,A46,A67,A50,A72;
a3,a4 // d3,d4 by A1,A2,A3,A4,A5,A6,A7,A10,A11,A14,A15,A18,A19,A29,A48
,A49,A58,A59,A46,A47,A67;
hence a3,a4 // b3,b4 by A73,A76,AFF_1:5;
end;
now
A77: now
o,b2 // o,b4 by A3,A5,A12,A13,AFF_1:39,41;
then
A78: LIN o,b2,b4 by AFF_1:def 1;
assume
A79: a2=a4;
then a1,a4 // b1,b2 by A23,AFF_1:4;
then b1,b2 // b1,b4 by A6,A14,A24,AFF_1:5;
hence a3,a4 // b3,b4 by A2,A4,A5,A8,A16,A20,A22,A79,A78,AFF_1:14,25;
end;
A80: now
o,b1 // o,b3 by A2,A4,A8,A9,AFF_1:39,41;
then
A81: LIN o,b1,b3 by AFF_1:def 1;
assume
A82: a1=a3;
then a2,a1 // b2,b3 by A22,AFF_1:4;
then b2,b1 // b2,b3 by A6,A15,A23,AFF_1:5;
hence a3,a4 // b3,b4 by A3,A4,A5,A12,A16,A20,A24,A82,A81,AFF_1:14,25;
end;
assume a1=a3 or a2=a4;
hence a3,a4 // b3,b4 by A80,A77;
end;
hence a3,a4 // b3,b4 by A25;
end;
hence thesis;
end;
theorem
X is satisfying_indirect_Scherungssatz implies X is satisfying_Scherungssatz
proof
assume
A1: X is satisfying_indirect_Scherungssatz;
then X is satisfying_major_indirect_Scherungssatz;
then
A2: X is satisfying_major_Scherungssatz by Th4;
X is satisfying_minor_indirect_Scherungssatz by A1,Th1;
then X is satisfying_minor_Scherungssatz by Th3;
hence thesis by A2,Th2;
end;
theorem Th6:
X is translational implies X is satisfying_minor_Scherungssatz
proof
assume
A1: X is translational;
now
let a1,a2,a3,a4,b1,b2,b3,b4,M,N;
assume that
A2: M // N and
A3: a1 in M and
A4: a3 in M and
A5: b1 in M and
A6: b3 in M and
A7: a2 in N and
A8: a4 in N and
A9: b2 in N and
A10: b4 in N and
A11: not a4 in M and
A12: not a2 in M and
A13: not b2 in M and
not b4 in M and
A14: not a1 in N and
A15: not a3 in N and
A16: not b1 in N and
not b3 in N and
A17: a3,a2 // b3,b2 and
A18: a2,a1 // b2,b1 and
A19: a1,a4 // b1,b4;
A20: M is being_line by A2,AFF_1:36;
A21: N is being_line by A2,AFF_1:36;
A22: now
assume that
A23: a1<>a3 and
A24: a2<>a4;
A25: now
assume ex x,y,z st LIN x,y,z & x<>y & x<>z & y<>z;
then consider d such that
A26: LIN a1,a2,d and
A27: a1<>d and
A28: a2<>d by TRANSLAC:1;
A29: ex Y st Y is being_line & d in Y & Y // M
proof
consider Y such that
A30: d in Y and
A31: M // Y by A20,AFF_1:49;
take Y;
thus thesis by A30,A31,AFF_1:36;
end;
LIN a2,a1,d by A26,AFF_1:6;
then a2,a1 // a2,d by AFF_1:def 1;
then
A32: b2,b1 // a2,d by A3,A12,A18,AFF_1:5;
A33: a2,a3 // b2,b3 by A17,AFF_1:4;
consider Y such that
A34: Y is being_line and
A35: d in Y and
A36: Y // M by A29;
A37: Y // N by A2,A36,AFF_1:44;
A38: N<>M & N<>Y & Y<>M
proof
A39: now
LIN a2,d,a1 by A26,AFF_1:6;
then
A40: a2,d // a2,a1 by AFF_1:def 1;
assume N=Y;
then a2,d // a2,a4 by A7,A8,A34,A35,AFF_1:39,41;
then a2,a4 // a2,a1 by A28,A40,AFF_1:5;
then LIN a2,a4,a1 by AFF_1:def 1;
hence contradiction by A7,A8,A14,A21,A24,AFF_1:25;
end;
A41: now
assume Y=M;
then
A42: a1,d // a1,a3 by A3,A4,A35,A36,AFF_1:39;
a1,a2 // a1,d by A26,AFF_1:def 1;
then a1,a3 // a1,a2 by A27,A42,AFF_1:5;
then LIN a1,a3,a2 by AFF_1:def 1;
hence contradiction by A3,A4,A12,A20,A23,AFF_1:25;
end;
assume not thesis;
hence contradiction by A8,A11,A39,A41;
end;
A43: Y // Y by A34,AFF_1:41;
ex d1 st d1 in Y & b1,b2 // b1,d1
proof
consider e1 such that
A44: d<>e1 and
A45: e1 in Y by A34,AFF_1:20;
consider e2 such that
A46: b1,b2 // b1,e2 and
A47: b1<>e2 by DIRAF:40;
not d,e1 // b1,e2
proof
assume d,e1 // b1,e2;
then d,e1 // b1,b2 by A46,A47,AFF_1:5;
then
A48: b1,b2 // Y by A35,A43,A44,A45,AFF_1:32,40;
a1,a3 // Y by A3,A4,A36,AFF_1:40;
then a1,a3 // b1,b2 by A34,A48,AFF_1:31;
then a1,a3 // b2,b1 by AFF_1:4;
then a1,a3 // a2,a1 by A5,A13,A18,AFF_1:5;
then a1,a3 // a1,a2 by AFF_1:4;
then LIN a1,a3,a2 by AFF_1:def 1;
hence contradiction by A3,A4,A12,A20,A23,AFF_1:25;
end;
then consider d1 such that
A49: LIN d,e1,d1 and
A50: LIN b1,e2,d1 by AFF_1:60;
take d1;
b1,e2 // b1,d1 by A50,AFF_1:def 1;
hence thesis by A34,A35,A44,A45,A46,A47,A49,AFF_1:5,25;
end;
then consider d1 such that
A51: d1 in Y and
A52: b1,b2 // b1,d1;
a1,a2 // a1,d by A26,AFF_1:def 1;
then a2,a1 // a1,d by AFF_1:4;
then b2,b1 // a1,d by A3,A12,A18,AFF_1:5;
then b1,b2 // a1,d by AFF_1:4;
then a1,d // b1,d1 by A5,A13,A52,AFF_1:5;
then
A53: d,a4 // d1,b4 by A1,A2,A3,A5,A8,A10,A19,A20,A21,A34,A35,A36,A51,A38,
AFF_2:def 11;
LIN b1,b2,d1 by A52,AFF_1:def 1;
then LIN b2,b1,d1 by AFF_1:6;
then b2,b1 // b2,d1 by AFF_1:def 1;
then
A54: a2,d // b2,d1 by A5,A13,A32,AFF_1:5;
N // Y by A2,A36,AFF_1:44;
then d,a3 // d1,b3 by A1,A2,A4,A6,A7,A9,A20,A21,A34,A35,A51,A38,A54,A33
,AFF_2:def 11;
hence a3,a4 // b3,b4 by A1,A4,A6,A8,A10,A20,A21,A34,A35,A36,A51,A38,A53
,A37,AFF_2:def 11;
end;
now
assume
A55: not ex x,y,z st LIN x,y,z & x<>y & x<>z & y<>z;
A56: now
assume
A57: a1=b1;
then
A58: LIN a1,a4,b4 by A19,AFF_1:def 1;
a1,a2 // a1,b2 by A18,A57,AFF_1:4;
then
A59: LIN a1,a2,b2 by AFF_1:def 1;
a2,b2 // M by A2,A7,A9,AFF_1:40;
then a2=b2 by A3,A12,A59,AFF_1:46;
then a2,a3 // a2,b3 by A17,AFF_1:4;
then
A60: LIN a2,a3,b3 by AFF_1:def 1;
a3,b3 // N by A2,A4,A6,AFF_1:40;
then
A61: a3=b3 by A7,A15,A60,AFF_1:46;
a4,b4 // M by A2,A8,A10,AFF_1:40;
then a4=b4 by A3,A11,A58,AFF_1:46;
hence a3,a4 // b3,b4 by A61,AFF_1:2;
end;
A62: now
assume
A63: a3=b1;
A64: now
A65: a4<>b4
proof
assume a4=b4;
then a4,a1 // a4,b1 by A19,AFF_1:4;
then
A66: LIN a4,a1,b1 by AFF_1:def 1;
a1,b1 // N by A2,A3,A5,AFF_1:40;
hence contradiction by A8,A14,A23,A63,A66,AFF_1:46;
end;
a2,a4 // a2,b4 by A7,A8,A10,A21,AFF_1:39,41;
then LIN a2,a4,b4 by AFF_1:def 1;
then
A67: a2=b4 by A24,A55,A65;
assume
A68: a4=b2;
A69: a3<>b3
proof
assume a3=b3;
then
A70: LIN a3,a2,b2 by A17,AFF_1:def 1;
a2,b2 // M by A2,A7,A9,AFF_1:40;
hence contradiction by A4,A12,A24,A68,A70,AFF_1:46;
end;
a1,a3 // a1,b3 by A3,A4,A6,A20,AFF_1:39,41;
then LIN a1,a3,b3 by AFF_1:def 1;
then
A71: a1=b3 by A23,A55,A69;
a3,a4 // b2,b1 by A63,A68,AFF_1:2;
then a3,a4 // a2,a1 by A5,A13,A18,AFF_1:5;
hence a3,a4 // b3,b4 by A71,A67,AFF_1:4;
end;
A72: now
assume a2=b2;
then
A73: LIN a2,a1,b1 by A18,AFF_1:def 1;
a1,b1 // N by A2,A3,A5,AFF_1:40;
hence a3,a4 // b3,b4 by A7,A14,A56,A73,AFF_1:46;
end;
a2,a4 // a2,b2 by A7,A8,A9,A21,AFF_1:39,41;
then LIN a2,a4,b2 by AFF_1:def 1;
hence a3,a4 // b3,b4 by A24,A55,A64,A72;
end;
a1,a3 // a1,b1 by A3,A4,A5,A20,AFF_1:39,41;
then LIN a1,a3,b1 by AFF_1:def 1;
hence a3,a4 // b3,b4 by A23,A55,A56,A62;
end;
hence a3,a4 // b3,b4 by A25;
end;
now
A74: now
assume
A75: a1=a3;
b1=b3
proof
LIN a2,a1,a3 by A75,AFF_1:7;
then a2,a1 // a2,a3 by AFF_1:def 1;
then b2,b1 // a2,a3 by A3,A12,A18,AFF_1:5;
then b2,b1 // a3,a2 by AFF_1:4;
then b2,b1 // b3,b2 by A4,A12,A17,AFF_1:5;
then b2,b1 // b2,b3 by AFF_1:4;
then
A76: LIN b2,b1,b3 by AFF_1:def 1;
assume
A77: b1<>b3;
b1,b3 // N by A2,A5,A6,AFF_1:40;
hence contradiction by A9,A16,A77,A76,AFF_1:46;
end;
hence a3,a4 // b3,b4 by A19,A75;
end;
A78: now
assume
A79: a2=a4;
then LIN a1,a4,a2 by AFF_1:7;
then a1,a4 // a1,a2 by AFF_1:def 1;
then b1,b4 // a1,a2 by A3,A11,A19,AFF_1:5;
then b1,b4 // a2,a1 by AFF_1:4;
then b1,b4 // b2,b1 by A3,A12,A18,AFF_1:5;
then b1,b2 // b1,b4 by AFF_1:4;
then
A80: LIN b1,b2,b4 by AFF_1:def 1;
b2,b4 // M by A2,A9,A10,AFF_1:40;
hence a3,a4 // b3,b4 by A5,A13,A17,A79,A80,AFF_1:46;
end;
assume a1=a3 or a2=a4;
hence a3,a4 // b3,b4 by A74,A78;
end;
hence a3,a4 // b3,b4 by A22;
end;
hence thesis;
end;
theorem Th7:
X is Desarguesian implies X is satisfying_major_Scherungssatz
proof
assume
A1: X is Desarguesian;
now
let o,a1,a2,a3,a4,b1,b2,b3,b4,M,N;
assume that
A2: M is being_line and
A3: N is being_line and
A4: o in M and
A5: o in N and
A6: a1 in M and
A7: a3 in M and
A8: b1 in M and
A9: b3 in M and
A10: a2 in N and
A11: a4 in N and
A12: b2 in N and
A13: b4 in N and
A14: not a4 in M and
A15: not a2 in M and
A16: not b2 in M and
not b4 in M and
A17: not a1 in N and
A18: not a3 in N and
A19: not b1 in N and
not b3 in N and
A20: a3,a2 // b3,b2 and
A21: a2,a1 // b2,b1 and
A22: a1,a4 // b1,b4;
A23: now
A24: now
assume ex x,y,z st LIN x,y,z & x<>y & x<>z & y<>z;
then consider d such that
A25: LIN a1,a2,d and
A26: a1<>d and
A27: a2<>d by TRANSLAC:1;
LIN o,d,d by AFF_1:7;
then consider Y such that
A28: Y is being_line and
A29: o in Y and
A30: d in Y and
d in Y by AFF_1:21;
a1,a2 // a1,d by A25,AFF_1:def 1;
then a2,a1 // a1,d by AFF_1:4;
then
A31: b2,b1 // a1,d by A6,A15,A21,AFF_1:5;
A32: N<>M & N<>Y & M<>Y
proof
A33: now
A34: LIN a1,d,a2 by A25,AFF_1:6;
assume
A35: N=Y or M=Y;
LIN a2,d,a1 by A25,AFF_1:6;
hence contradiction by A2,A3,A6,A10,A15,A17,A26,A27,A30,A35,A34,
AFF_1:25;
end;
assume not thesis;
hence contradiction by A11,A14,A33;
end;
A36: ex d1 st LIN b1,b2,d1 & d1 in Y
proof
not b1,b2 // o,d
proof
A37: o<>d
proof
assume o=d;
then LIN o,a1,a2 by A25,AFF_1:6;
hence contradiction by A2,A4,A5,A6,A15,A17,AFF_1:25;
end;
assume b1,b2 // o,d;
then b2,b1 // o,d by AFF_1:4;
then
A38: a2,a1 // o,d by A8,A16,A21,AFF_1:5;
a1,a2 // a1,d by A25,AFF_1:def 1;
then a2,a1 // a1,d by AFF_1:4;
then a1,d // o,d by A6,A15,A38,AFF_1:5;
then d,o // d,a1 by AFF_1:4;
then LIN d,o,a1 by AFF_1:def 1;
then LIN o,d,a1 by AFF_1:6;
then o,d // o,a1 by AFF_1:def 1;
then
A39: Y // M by A2,A4,A5,A6,A17,A28,A29,A30,A37,AFF_1:38;
LIN a2,a1,d by A25,AFF_1:6;
then a2,a1 // a2,d by AFF_1:def 1;
then a2,d // o,d by A6,A15,A38,AFF_1:5;
then d,a2 // d,o by AFF_1:4;
then LIN d,a2,o by AFF_1:def 1;
then LIN o,d,a2 by AFF_1:6;
then o,d // o,a2 by AFF_1:def 1;
then Y // N by A3,A4,A5,A10,A15,A28,A29,A30,A37,AFF_1:38;
then M // N by A39,AFF_1:44;
hence contradiction by A4,A5,A11,A14,AFF_1:45;
end;
then consider d1 such that
A40: LIN b1,b2,d1 and
A41: LIN o,d,d1 by AFF_1:60;
take d1;
o<>d
proof
assume o=d;
then LIN o,a1,a2 by A25,AFF_1:6;
hence contradiction by A2,A4,A5,A6,A15,A17,AFF_1:25;
end;
hence thesis by A28,A29,A30,A40,A41,AFF_1:25;
end;
LIN a2,a1,d by A25,AFF_1:6;
then a2,a1 // a2,d by AFF_1:def 1;
then
A42: b2,b1 // a2,d by A6,A15,A21,AFF_1:5;
A43: o<>d
proof
assume o=d;
then LIN o,a1,a2 by A25,AFF_1:6;
hence contradiction by A2,A4,A5,A6,A15,A17,AFF_1:25;
end;
consider d1 such that
A44: LIN b1,b2,d1 and
A45: d1 in Y by A36;
b1,b2 // b1,d1 by A44,AFF_1:def 1;
then b2,b1 // b1,d1 by AFF_1:4;
then a1,d // b1,d1 by A8,A16,A31,AFF_1:5;
then
A46: d,a4 // d1,b4 by A1,A2,A3,A4,A5,A6,A8,A11,A13,A14,A17,A22,A28,A29,A30
,A45,A43,A32,AFF_2:def 4;
LIN b2,b1,d1 by A44,AFF_1:6;
then b2,b1 // b2,d1 by AFF_1:def 1;
then
A47: a2,d // b2,d1 by A8,A16,A42,AFF_1:5;
a2,a3 // b2,b3 by A20,AFF_1:4;
then d,a3 // d1,b3 by A1,A2,A3,A4,A5,A7,A9,A10,A12,A15,A18,A28,A29,A30
,A45,A43,A32,A47,AFF_2:def 4;
hence
a3,a4 // b3,b4 by A1,A2,A3,A4,A5,A7,A9,A11,A13,A14,A18,A28,A29,A30,A45
,A43,A32,A46,AFF_2:def 4;
end;
assume that
A48: a1<>a3 and
A49: a2<>a4;
now
assume
A50: not ex x,y,z st LIN x,y,z & x<>y & x<>z & y<>z;
A51: now
assume
A52: a1=b1;
A53: a2<>b4
proof
assume a2=b4;
then LIN a1,a4,a2 by A22,A52,AFF_1:def 1;
then LIN a2,a4,a1 by AFF_1:6;
hence contradiction by A3,A10,A11,A17,A49,AFF_1:25;
end;
A54: a1<>b3
proof
assume a1=b3;
then b2,b1 // a2,a3 by A20,A52,AFF_1:4;
then
A55: a2,a1 // a2,a3 by A8,A16,A21,AFF_1:5;
LIN o,a1,a3 by A2,A4,A6,A7,AFF_1:21;
hence contradiction by A3,A4,A5,A10,A15,A17,A48,A55,AFF_1:14,25;
end;
LIN a2,a4,b4 by A3,A10,A11,A13,AFF_1:21;
then
A56: a2=b4 or a4=b4 by A49,A50;
LIN a1,a3,b3 by A2,A6,A7,A9,AFF_1:21;
then a3=b3 by A48,A50,A54;
hence a3,a4 // b3,b4 by A56,A53,AFF_1:2;
end;
A57: now
assume
A58: a3=b1;
A59: a2<>b2
proof
assume a2=b2;
then LIN a2,a1,a3 by A21,A58,AFF_1:def 1;
then LIN a1,a3,a2 by AFF_1:6;
hence contradiction by A2,A6,A7,A15,A48,AFF_1:25;
end;
A60: a3<>b3
proof
assume a3=b3;
then a3,a2 // b2,b1 by A20,A58,AFF_1:4;
then a3,a2 // a2,a1 by A8,A16,A21,AFF_1:5;
then a2,a3 // a2,a1 by AFF_1:4;
then LIN a2,a3,a1 by AFF_1:def 1;
then LIN a1,a3,a2 by AFF_1:6;
hence contradiction by A2,A6,A7,A15,A48,AFF_1:25;
end;
A61: a4<>b4
proof
assume a4=b4;
then a4,a1 // a4,a3 by A22,A58,AFF_1:4;
then LIN a4,a1,a3 by AFF_1:def 1;
then LIN a1,a3,a4 by AFF_1:6;
hence contradiction by A2,A6,A7,A14,A48,AFF_1:25;
end;
LIN a2,a4,b4 by A3,A10,A11,A13,AFF_1:21;
then
A62: a2=b4 by A49,A50,A61;
LIN a2,a4,b2 by A3,A10,A11,A12,AFF_1:21;
then a4=b2 by A49,A50,A59;
then
A63: a3,a4 // b2,b1 by A58,AFF_1:2;
LIN a1,a3,b3 by A2,A6,A7,A9,AFF_1:21;
then a1=b3 by A48,A50,A60;
then a3,a4 // b4,b3 by A8,A16,A21,A62,A63,AFF_1:5;
hence a3,a4 // b3,b4 by AFF_1:4;
end;
LIN a1,a3,b1 by A2,A6,A7,A8,AFF_1:21;
hence a3,a4 // b3,b4 by A48,A50,A51,A57;
end;
hence a3,a4 // b3,b4 by A24;
end;
now
A64: now
o,b2 // o,b4 by A3,A5,A12,A13,AFF_1:39,41;
then
A65: LIN o,b2,b4 by AFF_1:def 1;
assume
A66: a2=a4;
a1,a2 // b1,b2 by A21,AFF_1:4;
then b1,b2 // b1,b4 by A6,A14,A22,A66,AFF_1:5;
hence a3,a4 // b3,b4 by A2,A4,A5,A8,A16,A19,A20,A66,A65,AFF_1:14,25;
end;
A67: now
o,b1 // o,b3 by A2,A4,A8,A9,AFF_1:39,41;
then
A68: LIN o,b1,b3 by AFF_1:def 1;
assume
A69: a1=a3;
then a2,a1 // b2,b3 by A20,AFF_1:4;
then b2,b1 // b2,b3 by A6,A15,A21,AFF_1:5;
hence a3,a4 // b3,b4 by A3,A4,A5,A12,A16,A19,A22,A69,A68,AFF_1:14,25;
end;
assume a1=a3 or a2=a4;
hence a3,a4 // b3,b4 by A67,A64;
end;
hence a3,a4 // b3,b4 by A23;
end;
hence thesis;
end;
theorem
X is Desarguesian iff X is satisfying_Scherungssatz
proof
A1: X is satisfying_Scherungssatz implies X is Desarguesian
proof
assume
A2: X is satisfying_Scherungssatz;
now
let Y,Z,M,o,a,b,c,a1,b1,c1;
assume that
A3: o in Y and
A4: o in Z and
A5: o in M and
A6: o<>a and
A7: o<>b and
A8: o<>c and
A9: a in Y and
A10: a1 in Y and
A11: b in Z and
A12: b1 in Z and
A13: c in M and
A14: c1 in M and
A15: Y is being_line and
A16: Z is being_line and
A17: M is being_line and
A18: Y<>Z and
A19: Y<>M and
A20: a,b // a1,b1 and
A21: a,c // a1,c1;
assume
A22: not b,c // b1,c1;
A23: now
let Y,Z,M,o,a,b,c,a1,b1,c1,d;
assume
A24: X is satisfying_Scherungssatz;
assume that
A25: o in Y and
A26: o in Z and
A27: o in M and
A28: o<>a and
A29: o<>b and
A30: o<>c and
A31: a in Y and
A32: a1 in Y and
A33: b in Z and
A34: b1 in Z and
A35: c in M and
A36: c1 in M and
A37: Y is being_line and
A38: Z is being_line and
A39: M is being_line and
A40: Y<>Z and
A41: Y<>M and
A42: a,b // a1,b1 and
A43: a,c // a1,c1 and
A44: LIN b,c,d and
A45: LIN b1,c1,d;
LIN a,a1,d or b,c // b1,c1
proof
assume that
A46: not LIN a,a1,d and
A47: not b,c // b1,c1;
A48: c <>c1 & a<>a1 & b<>b1
proof
A49: now
A50: not LIN o,a,c
proof
assume LIN o,a,c;
then c in Y by A25,A28,A31,A37,AFF_1:25;
then
A51: o,c // Y by A25,A37,AFF_1:52;
o,c // M by A27,A35,A39,AFF_1:52;
hence contradiction by A25,A27,A30,A41,A51,AFF_1:45,53;
end;
o,c // o,c1 by A27,A35,A36,A39,AFF_1:39,41;
then
A52: LIN o,c,c1 by AFF_1:def 1;
A53: not LIN o,b,a
proof
assume LIN o,b,a;
then a in Z by A26,A29,A33,A38,AFF_1:25;
then
A54: o,a // Z by A26,A38,AFF_1:52;
o,a // Y by A25,A31,A37,AFF_1:52;
hence contradiction by A25,A26,A28,A40,A54,AFF_1:45,53;
end;
o,a // o,a1 by A25,A31,A32,A37,AFF_1:39,41;
then
A55: LIN o,a,a1 by AFF_1:def 1;
assume
A56: b=b1;
then b,a // b,a1 by A42,AFF_1:4;
then a=a1 by A53,A55,AFF_1:14;
then c =c1 by A43,A50,A52,AFF_1:14;
hence contradiction by A47,A56,AFF_1:2;
end;
A57: now
A58: not LIN o,a,b
proof
assume LIN o,a,b;
then b in Y by A25,A28,A31,A37,AFF_1:25;
then
A59: o,b // Y by A25,A37,AFF_1:52;
o,b // Z by A26,A33,A38,AFF_1:52;
hence contradiction by A25,A26,A29,A40,A59,AFF_1:45,53;
end;
o,b // o,b1 by A26,A33,A34,A38,AFF_1:39,41;
then
A60: LIN o,b,b1 by AFF_1:def 1;
A61: not LIN o,c,a
proof
assume LIN o,c,a;
then a in M by A27,A30,A35,A39,AFF_1:25;
then
A62: o,a // M by A27,A39,AFF_1:52;
o,a // Y by A25,A31,A37,AFF_1:52;
hence contradiction by A25,A27,A28,A41,A62,AFF_1:45,53;
end;
o,a // o,a1 by A25,A31,A32,A37,AFF_1:39,41;
then
A63: LIN o,a,a1 by AFF_1:def 1;
assume
A64: c =c1;
then c,a // c,a1 by A43,AFF_1:4;
then a=a1 by A61,A63,AFF_1:14;
then b=b1 by A42,A58,A60,AFF_1:14;
hence contradiction by A47,A64,AFF_1:2;
end;
A65: now
A66: not LIN o,a,c
proof
assume LIN o,a,c;
then c in Y by A25,A28,A31,A37,AFF_1:25;
then
A67: o,c // Y by A25,A37,AFF_1:52;
o,c // M by A27,A35,A39,AFF_1:52;
hence contradiction by A25,A27,A30,A41,A67,AFF_1:45,53;
end;
A68: not LIN o,a,b
proof
assume LIN o,a,b;
then b in Y by A25,A28,A31,A37,AFF_1:25;
then
A69: o,b // Y by A25,A37,AFF_1:52;
o,b // Z by A26,A33,A38,AFF_1:52;
hence contradiction by A25,A26,A29,A40,A69,AFF_1:45,53;
end;
assume
A70: a=a1;
o,c // o,c1 by A27,A35,A36,A39,AFF_1:39,41;
then LIN o,c,c1 by AFF_1:def 1;
then
A71: c =c1 by A43,A70,A66,AFF_1:14;
o,b // o,b1 by A26,A33,A34,A38,AFF_1:39,41;
then LIN o,b,b1 by AFF_1:def 1;
then b=b1 by A42,A70,A68,AFF_1:14;
hence contradiction by A47,A71,AFF_1:2;
end;
assume not thesis;
hence contradiction by A57,A65,A49;
end;
now
assume
A72: b<>c;
A73: now
assume
A74: b1<>o;
A75: a1<>b1 & a1<>c1
proof
A76: now
A77: o<>a1
proof
A78: not LIN a,b,o
proof
assume LIN a,b,o;
then LIN o,a,b by AFF_1:6;
then b in Y by A25,A28,A31,A37,AFF_1:25;
then
A79: o,b // Y by A25,A37,AFF_1:52;
o,b // Z by A26,A33,A38,AFF_1:52;
hence contradiction by A25,A26,A29,A40,A79,AFF_1:45,53;
end;
A80: o,b // o,b1 by A26,A33,A34,A38,AFF_1:39,41;
assume o=a1;
then a,b // o,b by A42,A74,A80,AFF_1:5;
then b,a // b,o by AFF_1:4;
then LIN b,a,o by AFF_1:def 1;
then LIN o,a,b by AFF_1:6;
then o,a // o,b by AFF_1:def 1;
then o,a // o,b1 by A29,A80,AFF_1:5;
then LIN o,a,b1 by AFF_1:def 1;
then
A81: LIN a,o,b1 by AFF_1:6;
b,o // b,b1 by A26,A33,A34,A38,AFF_1:39,41;
hence contradiction by A74,A78,A81,AFF_1:14;
end;
assume a1=c1;
then
A82: o,a1 // M by A27,A36,A39,AFF_1:52;
o,a1 // Y by A25,A32,A37,AFF_1:52;
hence contradiction by A25,A27,A41,A82,A77,AFF_1:45,53;
end;
A83: now
assume a1=b1;
then
A84: o,b1 // Y by A25,A32,A37,AFF_1:52;
o,b1 // Z by A26,A34,A38,AFF_1:52;
hence contradiction by A25,A26,A40,A74,A84,AFF_1:45,53;
end;
assume not thesis;
hence contradiction by A83,A76;
end;
LIN o,o,a by AFF_1:7;
then consider C such that
A85: C is being_line and
A86: o in C and
o in C and
A87: a in C by AFF_1:21;
A88: ex d2 st d2 in C & a,c // d,d2
proof
consider e2 such that
A89: a,c // d,e2 and
A90: d<>e2 by DIRAF:40;
consider e1 such that
A91: o,a // o,e1 and
A92: o<>e1 by DIRAF:40;
LIN o,a,e1 by A91,AFF_1:def 1;
then
A93: e1 in C by A28,A85,A86,A87,AFF_1:25;
not o,e1 // d,e2
proof
assume o,e1 // d,e2;
then o,a // d,e2 by A91,A92,AFF_1:5;
then o,a // a,c by A89,A90,AFF_1:5;
then a,o // a,c by AFF_1:4;
then LIN a,o,c by AFF_1:def 1;
then c in Y by A25,A28,A31,A37,AFF_1:25;
then
A94: o, c // Y by A25,A37,AFF_1:52;
o,c // M by A27,A35,A39,AFF_1:52;
hence contradiction by A25,A27,A30,A41,A94,AFF_1:45,53;
end;
then consider d2 such that
A95: LIN o,e1,d2 and
A96: LIN d,e2,d2 by AFF_1:60;
take d2;
d,e2 // d,d2 by A96,AFF_1:def 1;
hence thesis by A85,A86,A92,A89,A90,A95,A93,AFF_1:5,25;
end;
A97: ex d1 st d1 in C & c,c1 // d,d1
proof
consider e2 such that
A98: c,c1 // d,e2 and
A99: d<>e2 by DIRAF:40;
consider e1 such that
A100: o,a // o,e1 and
A101: o<>e1 by DIRAF:40;
LIN o,a,e1 by A100,AFF_1:def 1;
then
A102: e1 in C by A28,A85,A86,A87,AFF_1:25;
not o,e1 // d,e2
proof
assume o,e1 // d,e2;
then o,a // d,e2 by A100,A101,AFF_1:5;
then
A103: o,a // c,c1 by A98,A99,AFF_1:5;
c,c1 // o,c by A27,A35,A36,A39,AFF_1:39,41;
then o,a // o,c by A48,A103,AFF_1:5;
then LIN o,a,c by AFF_1:def 1;
then c in Y by A25,A28,A31,A37,AFF_1:25;
then
A104: o,c // Y by A25,A37,AFF_1:52;
o,c // M by A27,A35,A39,AFF_1:52;
hence contradiction by A25,A27,A30,A41,A104,AFF_1:45,53;
end;
then consider d1 such that
A105: LIN o,e1,d1 and
A106: LIN d,e2,d1 by AFF_1:60;
take d1;
d,e2 // d,d1 by A106,AFF_1:def 1;
hence thesis by A85,A86,A101,A98,A99,A105,A102,AFF_1:5,25;
end;
consider d2 such that
A107: d2 in C and
A108: a,c // d,d2 by A88;
consider d1 such that
A109: d1 in C and
A110: c,c1 // d,d1 by A97;
c,c1 // c,o by A27,A35,A36,A39,AFF_1:39,41;
then
A111: c,o // d,d1 by A48,A110,AFF_1:5;
o,a // o,a1 by A25,A31,A32,A37,AFF_1:39,41;
then LIN o,a,a1 by AFF_1:def 1;
then
A112: a1 in C by A28,A85,A86,A87,AFF_1:25;
LIN b,b,c by AFF_1:7;
then consider A such that
A113: A is being_line and
A114: b in A and
b in A and
A115: c in A by AFF_1:21;
A116: d in A by A44,A72,A113,A114,A115,AFF_1:25;
A117: b<>c by A47,AFF_1:3;
A118: ex d3 st d3 in A & o,b // d1,d3
proof
consider e2 such that
A119: o,b // d1,e2 and
A120: d1<>e2 by DIRAF:40;
consider e1 such that
A121: b,c // b,e1 and
A122: b<>e1 by DIRAF:40;
LIN b,c,e1 by A121,AFF_1:def 1;
then
A123: e1 in A by A117,A113,A114,A115,AFF_1:25;
not b,e1 // d1,e2
proof
assume b,e1 // d1,e2;
then b,c // d1,e2 by A121,A122,AFF_1:5;
then
A124: b,c // o,b by A119,A120,AFF_1:5;
then b,c // b,o by AFF_1:4;
then LIN b,c,o by AFF_1:def 1;
then LIN o,b,c by AFF_1:6;
then
A125: o, b // o,c by AFF_1:def 1;
A126: o,b // o,b1 by A26,A33,A34,A38,AFF_1:39,41;
o,c // o,c1 by A27,A35,A36,A39,AFF_1:39,41;
then o,b // o,c1 by A30,A125,AFF_1:5;
then o,b1 // o,c1 by A29,A126,AFF_1:5;
then LIN o, b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:6;
then b1,c1 // b1,o by AFF_1:def 1;
then b1,c1 // o,b1 by AFF_1:4;
then b1,c1 // o,b by A74,A126,AFF_1:5;
hence contradiction by A29,A47,A124,AFF_1:5;
end;
then consider d3 such that
A127: LIN b,e1,d3 and
A128: LIN d1,e2,d3 by AFF_1:60;
take d3;
d1,e2 // d1,d3 by A128,AFF_1:def 1;
hence thesis by A113,A114,A122,A119,A120,A127,A123,AFF_1:5,25;
end;
A129: not o in A & not a in A & not d1 in A & not d2 in A
proof
A130: now
A131: a<>b
proof
assume a=b;
then
A132: o,b // Y by A25,A31,A37,AFF_1:52;
o,b // Z by A26,A33,A38,AFF_1:52;
hence contradiction by A25,A26,A29,A40,A132,AFF_1:45,53;
end;
A133: a1<>b1
proof
assume a1=b1;
then
A134: o,b1 // Y by A25,A32,A37,AFF_1:52;
o,b1 // Z by A26,A34,A38,AFF_1:52;
hence contradiction by A25,A26,A40,A74,A134,AFF_1:45,53;
end;
assume a in A;
then
A135: a,b // a,c by A113,A114,A115,AFF_1:39,41;
a<>c
proof
assume a=c;
then
A136: o,c // Y by A25,A31,A37,AFF_1:52;
o,c // M by A27,A35,A39,AFF_1:52;
hence contradiction by A25,A27,A30,A41,A136,AFF_1:45,53;
end;
then a,b // a1,c1 by A43,A135,AFF_1:5;
then a1,b1 // a1,c1 by A42,A131,AFF_1:5;
then LIN a1,b1,c1 by AFF_1:def 1;
then LIN b1,c1,a1 by AFF_1:6;
then b1,c1 // b1,a1 by AFF_1:def 1;
then
A137: a1,b1 // b1,c1 by AFF_1:4;
LIN a,b,c by A135,AFF_1:def 1;
then LIN b,c,a by AFF_1:6;
then b, c // b,a by AFF_1:def 1;
then b,c // a,b by AFF_1:4;
then b,c // a1,b1 by A42,A131,AFF_1:5;
hence contradiction by A47,A137,A133,AFF_1:5;
end;
A138: now
A139: d<>d2
proof
o,a // o,a1 by A25,A31,A32,A37,AFF_1:39,41;
then LIN o,a,a1 by AFF_1:def 1;
then
A140: a1 in C by A28,A85,A86,A87,AFF_1:25;
assume d=d2;
then a,a1 // a,d by A85,A87,A107,A140,AFF_1:39,41;
hence contradiction by A46,AFF_1:def 1;
end;
assume
A141: d2 in A;
A142: d,d2 // c,a by A108,AFF_1:4;
d in A by A44,A117,A113,A114,A115,AFF_1:25;
hence contradiction by A113,A115,A130,A141,A139,A142,AFF_1:48
;
end;
A143: now
assume o in A;
then
A144: o,b // o,c by A113,A114,A115,AFF_1:39,41;
A145: o,b // o,b1 by A26,A33,A34,A38,AFF_1:39,41;
o,c // o,c1 by A27,A35,A36,A39,AFF_1:39,41;
then o,b // o,c1 by A30,A144,AFF_1:5;
then o,b1 // o,c1 by A29,A145,AFF_1:5;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:6;
then b1,c1 // b1,o by AFF_1:def 1;
then b1,c1 // o,b1 by AFF_1:4;
then o,b // b1,c1 by A74,A145,AFF_1:5;
then
A146: b,o // b1,c1 by AFF_1:4;
LIN o,b,c by A144,AFF_1:def 1;
then LIN b,c,o by AFF_1:6;
then b,c // b,o by AFF_1:def 1;
hence contradiction by A29,A47,A146,AFF_1:5;
end;
A147: now
A148: d<>d1
proof
o,a // o,a1 by A25,A31,A32,A37,AFF_1:39,41;
then LIN o,a,a1 by AFF_1:def 1;
then
A149: a1 in C by A28,A85,A86,A87,AFF_1:25;
assume d=d1;
then a,a1 // a,d by A85,A87,A109,A149,AFF_1:39,41;
hence contradiction by A46,AFF_1:def 1;
end;
assume
A150: d1 in A;
c,c1 // c,o by A27,A35,A36,A39,AFF_1:39,41;
then
A151: LIN c,c1,o by AFF_1:def 1;
A152: d,d1 // c,c1 by A110,AFF_1:4;
d in A by A44,A117,A113,A114,A115,AFF_1:25;
then c1 in A by A113,A115,A150,A148,A152,AFF_1:48;
hence contradiction by A48,A113,A115,A143,A151,AFF_1:25;
end;
assume not thesis;
hence contradiction by A143,A130,A147,A138;
end;
LIN b1,b1,c1 by AFF_1:7;
then consider K such that
A153: K is being_line and
A154: b1 in K and
b1 in K and
A155: c1 in K by AFF_1:21;
b1<>c1 by A47,AFF_1:3;
then
A156: d in K by A45,A153,A154,A155,AFF_1:25;
consider d3 such that
A157: d3 in A and
A158: o,b // d1,d3 by A118;
A159: b1<>c1 by A47,AFF_1:3;
ex d4 st d4 in K & d1,d3 // d1,d4
proof
consider e2 such that
A160: d1,d3 // d1,e2 and
A161: d1<>e2 by DIRAF:40;
consider e1 such that
A162: b1,c1 // b1,e1 and
A163: b1<>e1 by DIRAF:40;
LIN b1,c1,e1 by A162,AFF_1:def 1;
then
A164: e1 in K by A159,A153,A154,A155,AFF_1:25;
not b1,e1 // d1,e2
proof
A165: o<>c1
proof
A166: not LIN a,c,o
proof
assume LIN a,c,o;
then LIN o,a,c by AFF_1:6;
then c in Y by A25,A28,A31,A37,AFF_1:25;
then
A167: o,c // Y by A25,A37,AFF_1:52;
o,c // M by A27,A35,A39,AFF_1:52;
hence contradiction by A25,A27,A30,A41,A167,AFF_1:45,53;
end;
assume
A168: o=c1;
a1,o // a,a1 by A25,A31,A32,A37,AFF_1:39,41;
then a,c // a,a1 by A43,A75,A168,AFF_1:5;
then LIN a,c,a1 by AFF_1:def 1;
then LIN a1,c,a by AFF_1:6;
then
A169: a1,c // a1,a by AFF_1:def 1;
a1,a // a1,o by A25,A31,A32,A37,AFF_1:39,41;
then a1,c // a1,o by A48,A169,AFF_1:5;
then LIN a1,c,o by AFF_1:def 1;
then LIN c,o,a1 by AFF_1:6;
then
A170: c,o // c,a1 by AFF_1:def 1;
a,o // a,a1 by A25,A31,A32,A37,AFF_1:39,41;
then LIN a,o,a1 by AFF_1:def 1;
hence contradiction by A75,A168,A166,A170,AFF_1:14;
end;
A171: d1<>d3
proof
A172: d<>d1
proof
o,a // o,a1 by A25,A31,A32,A37,AFF_1:39,41;
then LIN o,a,a1 by AFF_1:def 1;
then
A173: a1 in C by A28,A85,A86,A87,AFF_1:25;
assume d=d1;
then a,a1 // a,d by A85,A87,A109,A173,AFF_1:39,41;
hence contradiction by A46,AFF_1:def 1;
end;
assume
A174: d1=d3;
c,c1 // o,c by A27,A35,A36,A39,AFF_1:39,41;
then o,c // d,d1 by A48,A110,AFF_1:5;
then
A175: d,d1 // c,o by AFF_1:4;
A176: o,b // o,b1 by A26,A33,A34,A38,AFF_1:39,41;
d in A by A44,A117,A113,A114,A115,AFF_1:25;
then o in A by A113,A115,A157,A174,A172,A175,AFF_1:48;
then
A177: o,b // o,c by A113,A114,A115,AFF_1:39,41;
o,c // o,c1 by A27,A35,A36,A39,AFF_1:39,41;
then o,b // o,c1 by A30,A177,AFF_1:5;
then o,b1 // o,c1 by A29,A176,AFF_1:5;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:6;
then b1,c1 // b1,o by AFF_1:def 1;
then b1,c1 // o,b1 by AFF_1:4;
then
A178: o,b // b1,c1 by A74,A176,AFF_1:5;
LIN o,b,c by A177,AFF_1:def 1;
then LIN b,c,o by AFF_1:6;
then b,c // b,o by AFF_1:def 1;
then b,c // o,b by AFF_1:4;
hence contradiction by A29,A47,A178,AFF_1:5;
end;
assume b1,e1 // d1,e2;
then b1,c1 // d1,e2 by A162,A163,AFF_1:5;
then
A179: b1,c1 // d1,d3 by A160,A161,AFF_1:5;
A180: o,b // o,b1 by A26,A33,A34,A38,AFF_1:39,41;
then o,b1 // d1,d3 by A29,A158,AFF_1:5;
then
A181: o,b1 // b1,c1 by A179,A171,AFF_1:5;
then b1,o // b1,c1 by AFF_1:4;
then LIN b1,o,c1 by AFF_1:def 1;
then LIN o,b1,c1 by AFF_1:6;
then o,b1 // o,c1 by AFF_1:def 1;
then
A182: o,b // o,c1 by A74,A180,AFF_1:5;
o,c // o,c1 by A27,A35,A36,A39,AFF_1:39,41;
then o,b // o,c by A182,A165,AFF_1:5;
then LIN o,b,c by AFF_1:def 1;
then LIN b,o,c by AFF_1:6;
then b,o // b,c by AFF_1:def 1;
then o,b // b,c by AFF_1:4;
then o,b1 // b,c by A29,A180,AFF_1:5;
hence contradiction by A47,A74,A181,AFF_1:5;
end;
then consider d4 such that
A183: LIN b1,e1,d4 and
A184: LIN d1,e2,d4 by AFF_1:60;
take d4;
d1,e2 // d1,d4 by A184,AFF_1:def 1;
hence thesis by A153,A154,A163,A160,A161,A183,A164,AFF_1:5,25;
end;
then consider d4 such that
A185: d4 in K and
A186: d1,d3 // d1,d4;
A187: not c in C & not b in C & not d in C & not d3 in C
proof
A188: now
assume b in C;
then o,a // o,b by A85,A86,A87,AFF_1:39,41;
then LIN o,a,b by AFF_1:def 1;
then b in Y by A25,A28,A31,A37,AFF_1:25;
then
A189: o,b // Y by A25,A37,AFF_1:52;
o,b // Z by A26,A33,A38,AFF_1:52;
hence contradiction by A25,A26,A29,A40,A189,AFF_1:45,53;
end;
A190: now
A191: d1<>d3
proof
A192: d<>d1
proof
o,a // o,a1 by A25,A31,A32,A37,AFF_1:39,41;
then LIN o,a,a1 by AFF_1:def 1;
then
A193: a1 in C by A28,A85,A86,A87,AFF_1:25;
assume d=d1;
then a,a1 // a,d by A85,A87,A109,A193,AFF_1:39,41;
hence contradiction by A46,AFF_1:def 1;
end;
assume
A194: d1=d3;
A195: o,c // o,c1 by A27,A35,A36,A39,AFF_1:39,41;
A196: d,d1 // c,c1 by A110,AFF_1:4;
d in A by A44,A117,A113,A114,A115,AFF_1:25;
then c1 in A by A113,A115,A157,A194,A192,A196,AFF_1:48;
then
A197: c,c1 // c,b by A113,A114,A115,AFF_1:39,41;
A198: o,b // o,b1 by A26,A33,A34,A38,AFF_1:39,41;
c,o // c,c1 by A27,A35,A36,A39,AFF_1:39,41;
then c,o // c,b by A48,A197,AFF_1:5;
then
A199: LIN c,o,b by AFF_1:def 1;
then LIN o,b,c by AFF_1:6;
then o,b // o,c by AFF_1:def 1;
then o,b1 // o,c by A29,A198,AFF_1:5;
then o,b1 // o,c1 by A30,A195,AFF_1:5;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:6;
then b1,c1 // b1,o by AFF_1:def 1;
then b1,c1 // o,b1 by AFF_1:4;
then
A200: o,b // b1,c1 by A74,A198,AFF_1:5;
LIN b,c,o by A199,AFF_1:6;
then b,c // b,o by AFF_1:def 1;
then b,c // o,b by AFF_1:4;
hence contradiction by A29,A47,A200,AFF_1:5;
end;
assume
A201: d3 in C;
d1,d3 // o,b by A158,AFF_1:4;
hence contradiction by A85,A86,A109,A188,A201,A191,AFF_1:48;
end;
A202: now
assume c in C;
then o,a // o,c by A85,A86,A87,AFF_1:39,41;
then LIN o,a,c by AFF_1:def 1;
then c in Y by A25,A28,A31,A37,AFF_1:25;
then
A203: o,c // Y by A25,A37,AFF_1:52;
o,c // M by A27,A35,A39,AFF_1:52;
hence contradiction by A25,A27,A30,A41,A203,AFF_1:45,53;
end;
A204: now
assume d in C;
then
A205: o,a // a,d by A85,A86,A87,AFF_1:39,41;
o,a // a,a1 by A25,A31,A32,A37,AFF_1:39,41;
then a,a1 // a,d by A28,A205,AFF_1:5;
hence contradiction by A46,AFF_1:def 1;
end;
assume not thesis;
hence contradiction by A202,A188,A204,A190;
end;
A206: d4<>d3
proof
assume
A207: d4=d3;
d=d3
proof
d in A by A44,A117,A113,A114,A115,AFF_1:25;
then
A208: b,c // d,d3 by A113,A114,A115,A157,AFF_1:39,41;
d in K by A45,A159,A153,A154,A155,AFF_1:25;
then
A209: b1,c1 // d,d3 by A153,A154,A155,A185,A207,AFF_1:39,41;
assume d<>d3;
hence contradiction by A47,A209,A208,AFF_1:5;
end;
then
A210: o,b // d,d1 by A158,AFF_1:4;
o,c // c,c1 by A27,A35,A36,A39,AFF_1:39,41;
then o,c // d,d1 by A48,A110,AFF_1:5;
then
A211: o,b // o,c by A109,A187,A210,AFF_1:5;
A212: o,c // o,c1 by A27,A35,A36,A39,AFF_1:39,41;
A213: o,b // o,b1 by A26,A33,A34,A38,AFF_1:39,41;
then o,b1 // o,c by A29,A211,AFF_1:5;
then o,b1 // o,c1 by A30,A212,AFF_1:5;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:6;
then b1,c1 // b1,o by AFF_1:def 1;
then b1,c1 // o,b1 by AFF_1:4;
then
A214: o,b // b1,c1 by A74,A213,AFF_1:5;
LIN o,b,c by A211,AFF_1:def 1;
then LIN b,c,o by AFF_1:6;
then b,c // b,o by AFF_1:def 1;
then b,c // o,b by AFF_1:4;
hence contradiction by A29,A47,A214,AFF_1:5;
end;
A215: a<>b & a<>c
proof
A216: now
assume a=c;
then
A217: o,a // M by A27,A35,A39,AFF_1:52;
o,a // Y by A25,A31,A37,AFF_1:52;
hence contradiction by A25,A27,A28,A41,A217,AFF_1:45,53;
end;
A218: now
assume a=b;
then
A219: o,a // Z by A26,A33,A38,AFF_1:52;
o,a // Y by A25,A31,A37,AFF_1:52;
hence contradiction by A25,A26,A28,A40,A219,AFF_1:45,53;
end;
assume not thesis;
hence contradiction by A218,A216;
end;
A220: not o in K & not a1 in K & not d1 in K & not d2 in K
proof
A221: now
A222: o<>c1
proof
A223: a1<>o
proof
A224: not LIN a,b,o
proof
assume LIN a,b,o;
then LIN o,a,b by AFF_1:6;
then b in Y by A25,A28,A31,A37,AFF_1:25;
then
A225: o,b // Y by A25,A37,AFF_1:52;
o,b // Z by A26,A33,A38,AFF_1:52;
hence contradiction by A25,A26,A29,A40,A225,AFF_1:45,53
;
end;
A226: o,b // o,b1 by A26,A33,A34,A38,AFF_1:39,41;
assume a1=o;
then a,b // o,b by A42,A74,A226,AFF_1:5;
then b,a // b,o by AFF_1:4;
then LIN b,a,o by AFF_1:def 1;
then LIN o,a,b by AFF_1:6;
then o,a // o,b by AFF_1:def 1;
then o,a // o,b1 by A29,A226,AFF_1:5;
then LIN o,a,b1 by AFF_1:def 1;
then
A227: LIN a,o,b1 by AFF_1:6;
b,o // b,b1 by A26,A33,A34,A38,AFF_1:39,41;
hence contradiction by A74,A224,A227,AFF_1:14;
end;
A228: not LIN c,a,o
proof
assume LIN c,a,o;
then LIN o,a,c by AFF_1:6;
then c in Y by A25,A28,A31,A37,AFF_1:25;
then
A229: o,c // Y by A25,A37,AFF_1:52;
o,c // M by A27,A35,A39,AFF_1:52;
hence contradiction by A25,A27,A30,A41,A229,AFF_1:45,53;
end;
A230: a1,o // o,a by A25,A31,A32,A37,AFF_1:39,41;
assume o=c1;
then a,c // o,a by A43,A223,A230,AFF_1:5;
then a,c // a,o by AFF_1:4;
then LIN a,c,o by AFF_1:def 1;
then LIN o,c,a by AFF_1:6;
then o,c // o,a by AFF_1:def 1;
then o,c // a1,o by A28,A230,AFF_1:5;
then o,c // o,a1 by AFF_1:4;
then LIN o,c,a1 by AFF_1:def 1;
then
A231: LIN c,o,a1 by AFF_1:6;
a,o // a,a1 by A25,A31,A32,A37,AFF_1:39,41;
hence contradiction by A223,A228,A231,AFF_1:14;
end;
A232: o,c // o,c1 by A27,A35,A36,A39,AFF_1:39,41;
assume o in K;
then
A233: o,b1 // o,c1 by A153,A154,A155,AFF_1:39,41;
A234: o,b1 // o,b by A26,A33,A34,A38,AFF_1:39,41;
then o,b // o,c1 by A74,A233,AFF_1:5;
then o,b // o,c by A222,A232,AFF_1:5;
then LIN o,b,c by AFF_1:def 1;
then LIN b,c,o by AFF_1:6;
then b,c // b,o by AFF_1:def 1;
then b,c // o,b by AFF_1:4;
then b,c // o,b1 by A29,A234,AFF_1:5;
then
A235: b,c // b1,o by AFF_1:4;
LIN o,b1,c1 by A233,AFF_1:def 1;
then LIN b1,c1,o by AFF_1:6;
then b1,c1 // b1,o by AFF_1:def 1;
hence contradiction by A47,A74,A235,AFF_1:5;
end;
A236: now
A237: d<>d1
proof
assume d=d1;
then
A238: o,a // a,d by A85,A86,A87,A109,AFF_1:39,41;
o,a // a,a1 by A25,A31,A32,A37,AFF_1:39,41;
then a,a1 // a,d by A28,A238,AFF_1:5;
hence contradiction by A46,AFF_1:def 1;
end;
assume
A239: d1 in K;
c,c1 // c,o by A27,A35,A36,A39,AFF_1:39,41;
then
A240: LIN c,c1,o by AFF_1:def 1;
A241: d,d1 // c1,c by A110,AFF_1:4;
d in K by A45,A159,A153,A154,A155,AFF_1:25;
then c in K by A153,A155,A239,A237,A241,AFF_1:48;
hence contradiction by A48,A153,A155,A221,A240,AFF_1:25;
end;
A242: now
assume a1 in K;
then
A243: a1,b1 // a1,c1 by A153,A154,A155,AFF_1:39,41;
then a,b // a1,c1 by A42,A75,AFF_1:5;
then a,b // a,c by A43,A75,AFF_1:5;
then LIN a,b,c by AFF_1:def 1;
then LIN b,c,a by AFF_1:6;
then b,c // b,a by AFF_1:def 1;
then b,c // a,b by AFF_1:4;
then
A244: b,c // a1,b1 by A42,A215,AFF_1:5;
LIN a1,b1,c1 by A243,AFF_1:def 1;
then LIN b1,c1,a1 by AFF_1:6;
then b1,c1 // b1,a1 by AFF_1:def 1;
then b1,c1 // a1,b1 by AFF_1:4;
hence contradiction by A47,A75,A244,AFF_1:5;
end;
A245: now
A246: d<>d2
proof
assume d=d2;
then
A247: o,a // a,d by A85,A86,A87,A107,AFF_1:39,41;
o,a // a,a1 by A25,A31,A32,A37,AFF_1:39,41;
then a,a1 // a,d by A28,A247,AFF_1:5;
hence contradiction by A46,AFF_1:def 1;
end;
assume
A248: d2 in K;
d,d2 // a1,c1 by A43,A215,A108,AFF_1:5;
then
A249: d,d2 // c1,a1 by AFF_1:4;
d in K by A45,A159,A153,A154,A155,AFF_1:25;
hence contradiction by A153,A155,A242,A248,A246,A249,AFF_1:48
;
end;
assume not thesis;
hence contradiction by A221,A242,A236,A245;
end;
A250: not c1 in C & not b1 in C & not d in C & not d4 in C
proof
A251: now
assume
A252: c1 in C;
o,c1 // c1,c by A27,A35,A36,A39,AFF_1:39,41;
hence contradiction by A155,A85,A86,A187,A220,A252,AFF_1:48;
end;
A253: now
assume
A254: d4 in C;
d1,d4 // d1,d3 by A186,AFF_1:4;
hence contradiction by A85,A109,A185,A187,A220,A254,AFF_1:48;
end;
A255: now
assume
A256: b1 in C;
o,b1 // o,b by A26,A33,A34,A38,AFF_1:39,41;
hence contradiction by A74,A85,A86,A187,A256,AFF_1:48;
end;
assume not thesis;
hence contradiction by A187,A251,A255,A253;
end;
a<>c
proof
assume a=c;
then
A257: o,a // M by A27,A35,A39,AFF_1:52;
o,a // Y by A25,A31,A37,AFF_1:52;
hence contradiction by A25,A27,A28,A41,A257,AFF_1:45,53;
end;
then a1,c1 // d,d2 by A43,A108,AFF_1:5;
then
A258: a1,c1 // d2,d by AFF_1:4;
c1,o // c,c1 by A27,A35,A36,A39,AFF_1:39,41;
then
A259: c1,o // d,d1 by A48,A110,AFF_1:5;
A260: d1<>d2
proof
assume d1=d2;
then a,c // c,c1 by A109,A110,A108,A187,AFF_1:5;
then c,c1 // c,a by AFF_1:4;
then LIN c,c1,a by AFF_1:def 1;
then a in M by A35,A36,A39,A48,AFF_1:25;
then
A261: o,a // M by A27,A39,AFF_1:52;
o,a // Y by A25,A31,A37,AFF_1:52;
hence contradiction by A25,A27,A28,A41,A261,AFF_1:45,53;
end;
A262: not LIN d4,d2,d1
proof
assume LIN d4,d2,d1;
then LIN d1,d2,d4 by AFF_1:6;
hence contradiction by A85,A109,A107,A250,A260,AFF_1:25;
end;
A263: o,b // o,b1 by A26,A33,A34,A38,AFF_1:51;
a,c // d2,d by A108,AFF_1:4;
then a,b // d2,d3 by A24,A113,A114,A115,A85,A86,A87,A109,A107
,A157,A158,A116,A129,A187,A111;
then
A264: d2,d3 // a1,b1 by A42,A215,AFF_1:5;
o,b // d1,d4 by A109,A158,A186,A187,AFF_1:5;
then o,b1 // d1,d4 by A29,A263,AFF_1:5;
then a1,b1 // d2,d4 by A24,A153,A154,A155,A85,A86,A109,A107,A185
,A112,A156,A220,A250,A258,A259;
then d2,d3 // d2,d4 by A75,A264,AFF_1:5;
then LIN d2,d3,d4 by AFF_1:def 1;
then LIN d4,d3,d2 by AFF_1:6;
then
A265: d4,d3 // d4,d2 by AFF_1:def 1;
LIN d1,d3,d4 by A186,AFF_1:def 1;
then LIN d4,d3,d1 by AFF_1:6;
then d4,d3 // d4,d1 by AFF_1:def 1;
then d4,d2 // d4,d1 by A206,A265,AFF_1:5;
hence contradiction by A262,AFF_1:def 1;
end;
now
assume
A266: b1=o;
A267: o=a1
proof
A268: not LIN b,a,o
proof
assume LIN b,a,o;
then LIN o,a,b by AFF_1:6;
then b in Y by A25,A28,A31,A37,AFF_1:25;
then
A269: o,b // Y by A25,A37,AFF_1:52;
o,b // Z by A26,A33,A38,AFF_1:52;
hence contradiction by A25,A26,A29,A40,A269,AFF_1:45,53;
end;
A270: a1<>a
proof
assume a1=a;
then LIN a,b,o by A42,A266,AFF_1:def 1;
then LIN o,a,b by AFF_1:6;
then b in Y by A25,A28,A31,A37,AFF_1:25;
then
A271: o,b // Y by A25,A37,AFF_1:52;
o,b // Z by A26,A33,A38,AFF_1:52;
hence contradiction by A25,A26,A29,A40,A271,AFF_1:45,53;
end;
assume
A272: o<>a1;
a1,o // a,a1 by A25,A31,A32,A37,AFF_1:51;
then a,b // a,a1 by A42,A266,A272,AFF_1:5;
then LIN a,b,a1 by AFF_1:def 1;
then LIN a1,b,a by AFF_1:6;
then
A273: a1,b // a1,a by AFF_1:def 1;
a1,a // a1,o by A25,A31,A32,A37,AFF_1:51;
then a1,b // a1,o by A273,A270,AFF_1:5;
then LIN a1,b,o by AFF_1:def 1;
then LIN b,o,a1 by AFF_1:6;
hence contradiction by A25,A31,A32,A37,A272,A268,AFF_1:14,51;
end;
o=c1
proof
A274: not LIN a,c,o
proof
assume LIN a,c,o;
then LIN o,a,c by AFF_1:6;
then c in Y by A25,A28,A31,A37,AFF_1:25;
then
A275: o,c // Y by A25,A37,AFF_1:52;
o,c // M by A27,A35,A39,AFF_1:52;
hence contradiction by A25,A27,A30,A41,A275,AFF_1:45,53;
end;
assume
A276: o<>c1;
A277: o,c1 // o,c by A27,A35,A36,A39,AFF_1:51;
then o,c // a,c by A43,A267,A276,AFF_1:5;
then c,o // c,a by AFF_1:4;
then LIN c,o,a by AFF_1:def 1;
then LIN o,a,c by AFF_1:6;
then o,a // o,c by AFF_1:def 1;
then o,a // o,c1 by A30,A277,AFF_1:5;
then LIN o,a,c1 by AFF_1:def 1;
then LIN a,o,c1 by AFF_1:6;
hence contradiction by A27,A35,A36,A39,A276,A274,AFF_1:14,51;
end;
hence contradiction by A47,A266,AFF_1:3;
end;
hence contradiction by A73;
end;
hence contradiction by A47,AFF_1:3;
end;
hence LIN a,a1,d or b,c // b1,c1;
end;
A278: now
A279: M // M by A17,AFF_1:41;
consider d such that
A280: LIN b,c,d and
A281: LIN b1,c1,d by A22,AFF_1:60;
A282: LIN a,a1,d by A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,A15,A16,A17
,A18,A19,A20,A21,A22,A23,A280,A281;
A283: not a in Z & not a in M
proof
A284: now
assume a in M;
then
A285: o,a // M by A5,A17,AFF_1:52;
o,a // Y by A3,A9,A15,AFF_1:52;
hence contradiction by A3,A5,A6,A19,A285,AFF_1:45,53;
end;
A286: now
assume a in Z;
then
A287: o,a // Z by A4,A16,AFF_1:52;
o,a // Y by A3,A9,A15,AFF_1:52;
hence contradiction by A3,A4,A6,A18,A287,AFF_1:45,53;
end;
assume not thesis;
hence contradiction by A286,A284;
end;
A288: ex d1 st a,b // d,d1 & d1 in Z
proof
consider e1 such that
A289: o,b // o,e1 and
A290: o<>e1 by DIRAF:40;
consider e2 such that
A291: a,b // d,e2 and
A292: d<>e2 by DIRAF:40;
not o,e1 // d,e2
proof
assume o,e1 // d,e2;
then o,b // d,e2 by A289,A290,AFF_1:5;
then o,b // a,b by A291,A292,AFF_1:5;
then b,o // b,a by AFF_1:4;
then LIN b,o,a by AFF_1:def 1;
hence contradiction by A4,A7,A11,A16,A283,AFF_1:25;
end;
then consider d1 such that
A293: LIN o,e1,d1 and
A294: LIN d,e2,d1 by AFF_1:60;
o,e1 // o,d1 by A293,AFF_1:def 1;
then o,b // o,d1 by A289,A290,AFF_1:5;
then
A295: LIN o,b,d1 by AFF_1:def 1;
take d1;
d,e2 // d,d1 by A294,AFF_1:def 1;
hence thesis by A4,A7,A11,A16,A291,A292,A295,AFF_1:5,25;
end;
A296: Z // Z by A16,AFF_1:41;
A297: a<>a1 & b<>b1 & c <>c1
proof
A298: now
A299: not LIN a,o,b
proof
assume LIN a,o,b;
then LIN o,b,a by AFF_1:6;
hence contradiction by A4,A7,A11,A16,A283,AFF_1:25;
end;
A300: not LIN a,o,c
proof
assume LIN a,o,c;
then LIN o,c,a by AFF_1:6;
hence contradiction by A5,A8,A13,A17,A283,AFF_1:25;
end;
assume
A301: a=a1;
then LIN a,c,c1 by A21,AFF_1:def 1;
then
A302: c =c1 by A5,A13,A14,A279,A300,AFF_1:14,39;
LIN a,b,b1 by A20,A301,AFF_1:def 1;
then b=b1 by A4,A11,A12,A296,A299,AFF_1:14,39;
hence contradiction by A22,A302,AFF_1:2;
end;
A303: now
assume b=b1;
then b,a // b,a1 by A20,AFF_1:4;
then
A304: LIN b,a,a1 by AFF_1:def 1;
o,a // o,a1 by A3,A9,A10,A15,AFF_1:39,41;
hence contradiction by A4,A7,A11,A16,A283,A298,A304,AFF_1:14,25;
end;
A305: now
assume c =c1;
then c,a // c,a1 by A21,AFF_1:4;
then
A306: LIN c,a,a1 by AFF_1:def 1;
o,a // o,a1 by A3,A9,A10,A15,AFF_1:39,41;
hence contradiction by A5,A8,A13,A17,A283,A298,A306,AFF_1:14,25;
end;
assume not thesis;
hence contradiction by A298,A303,A305;
end;
A307: a1<>o & b1<>o & c1<>o
proof
A308: now
assume
A309: a1=o;
A310: o=c1
proof
A311: not LIN c,a,o
proof
assume LIN c,a,o;
then LIN o,c,a by AFF_1:6;
hence contradiction by A5,A8,A13,A17,A283,AFF_1:25;
end;
assume
A312: o<>c1;
A313: o,c1 // o,c by A5,A13,A14,A17,AFF_1:39,41;
then a,c // o,c by A21,A309,A312,AFF_1:5;
then c,o // c,a by AFF_1:4;
then LIN c,o,a by AFF_1:def 1;
then LIN o,c,a by AFF_1:6;
then o,c // o,a by AFF_1:def 1;
then o,c1 // o,a by A8,A313,AFF_1:5;
then LIN o,c1,a by AFF_1:def 1;
then LIN a,o,c1 by AFF_1:6;
then
A314: a,o // a,c1 by AFF_1:def 1;
c,o // c,c1 by A5,A13,A14,A17,AFF_1:39,41;
then LIN c,o,c1 by AFF_1:def 1;
hence contradiction by A312,A311,A314,AFF_1:14;
end;
o=b1
proof
A315: not LIN b,a,o
proof
assume LIN b,a,o;
then LIN o,b,a by AFF_1:6;
hence contradiction by A4,A7,A11,A16,A283,AFF_1:25;
end;
assume
A316: o<>b1;
A317: o,b1 // o,b by A4,A11,A12,A16,AFF_1:39,41;
then a,b // o,b by A20,A309,A316,AFF_1:5;
then b,a // b,o by AFF_1:4;
then LIN b,a,o by AFF_1:def 1;
then LIN o,a,b by AFF_1:6;
then o,a // o,b by AFF_1:def 1;
then o,a // o,b1 by A7,A317,AFF_1:5;
then LIN o,a,b1 by AFF_1:def 1;
then LIN a,o,b1 by AFF_1:6;
then
A318: a,o // a,b1 by AFF_1:def 1;
b,o // b,b1 by A4,A11,A12,A16,AFF_1:39,41;
then LIN b,o,b1 by AFF_1:def 1;
hence contradiction by A316,A315,A318,AFF_1:14;
end;
hence contradiction by A22,A310,AFF_1:3;
end;
A319: now
A320: not LIN a,b,o
proof
assume LIN a,b,o;
then LIN o,b,a by AFF_1:6;
hence contradiction by A4,A7,A11,A16,A283,AFF_1:25;
end;
A321: a1,o // a,a1 by A3,A9,A10,A15,AFF_1:39,41;
assume b1=o;
then a,b // a, a1 by A20,A308,A321,AFF_1:5;
then LIN a,b,a1 by AFF_1:def 1;
then LIN a1,b,a by AFF_1:6;
then a1,b // a1,a by AFF_1:def 1;
then a1,b // a,a1 by AFF_1:4;
then a1,b // a1,o by A297,A321,AFF_1:5;
then LIN a1,b,o by AFF_1:def 1;
then LIN b,o,a1 by AFF_1:6;
then
A322: b,o // b,a1 by AFF_1:def 1;
a,o // a,a1 by A3,A9,A10,A15,AFF_1:39,41;
then LIN a,o,a1 by AFF_1:def 1;
hence contradiction by A308,A320,A322,AFF_1:14;
end;
A323: now
A324: not LIN a,c,o
proof
assume LIN a,c,o;
then LIN o,c,a by AFF_1:6;
hence contradiction by A5,A8,A13,A17,A283,AFF_1:25;
end;
A325: a1,o // a,a1 by A3,A9,A10,A15,AFF_1:39,41;
assume c1=o;
then a,c // a, a1 by A21,A308,A325,AFF_1:5;
then LIN a,c,a1 by AFF_1:def 1;
then LIN a1,a,c by AFF_1:6;
then a1,a // a1,c by AFF_1:def 1;
then a,a1 // a1,c by AFF_1:4;
then a1,o // a1,c by A297,A325,AFF_1:5;
then LIN a1,o,c by AFF_1:def 1;
then LIN c,o,a1 by AFF_1:6;
then
A326: c,o // c,a1 by AFF_1:def 1;
a,o // a,a1 by A3,A9,A10,A15,AFF_1:39,41;
then LIN a,o,a1 by AFF_1:def 1;
hence contradiction by A308,A324,A326,AFF_1:14;
end;
assume not thesis;
hence contradiction by A308,A319,A323;
end;
ex d2 st a,c // d,d2 & d2 in M
proof
consider e1 such that
A327: o,c // o,e1 and
A328: o<>e1 by DIRAF:40;
consider e2 such that
A329: a,c // d,e2 and
A330: d<>e2 by DIRAF:40;
not o,e1 // d,e2
proof
assume o,e1 // d,e2;
then o,c // d,e2 by A327,A328,AFF_1:5;
then o,c // a,c by A329,A330,AFF_1:5;
then c,o // c,a by AFF_1:4;
then LIN c,o,a by AFF_1:def 1;
hence contradiction by A5,A8,A13,A17,A283,AFF_1:25;
end;
then consider d2 such that
A331: LIN o,e1,d2 and
A332: LIN d,e2,d2 by AFF_1:60;
o,e1 // o,d2 by A331,AFF_1:def 1;
then o,c // o,d2 by A327,A328,AFF_1:5;
then
A333: LIN o,c,d2 by AFF_1:def 1;
take d2;
d,e2 // d,d2 by A332,AFF_1:def 1;
hence thesis by A5,A8,A13,A17,A329,A330,A333,AFF_1:5,25;
end;
then consider d2 such that
A334: a,c // d,d2 and
A335: d2 in M;
consider d1 such that
A336: a,b // d,d1 and
A337: d1 in Z by A288;
assume
A338: not Z // M;
A339: d1<>d2
proof
A340: o<>d1
proof
A341: o<>d
proof
assume o=d;
then LIN o,b,c by A280,AFF_1:6;
then c in Z by A4,A7,A11,A16,AFF_1:25;
then
A342: o,c // Z by A4,A16,AFF_1:52;
o,c // M by A5,A13,A17,AFF_1:52;
hence contradiction by A8,A338,A342,AFF_1:53;
end;
A343: a,a1 // a,d by A282,AFF_1:def 1;
a,o // a,a1 by A3,A9,A10,A15,AFF_1:39,41;
then a,o // a,d by A297,A343,AFF_1:5;
then LIN a,o,d by AFF_1:def 1;
then LIN o,a,d by AFF_1:6;
then o,a // o,d by AFF_1:def 1;
then
A344: a,o // d,o by AFF_1:4;
assume o=d1;
then a,b // a,o by A336,A341,A344,AFF_1:5;
then LIN a,b,o by AFF_1:def 1;
then LIN o,b,a by AFF_1:6;
hence contradiction by A4,A7,A11,A16,A283,AFF_1:25;
end;
assume d1=d2;
then
A345: o,d1 // M by A5,A17,A335,AFF_1:52;
o,d1 // Z by A4,A16,A337,AFF_1:52;
hence contradiction by A338,A345,A340,AFF_1:53;
end;
A346: now
assume
A347: b1,c1 // d1,d2;
ex d5 st LIN b,c,d5 & LIN d1,d2,d5
proof
consider e1 such that
A348: b,c // b,e1 and
A349: b<>e1 by DIRAF:40;
consider e2 such that
A350: d1,d2 // d1,e2 and
A351: d1<>e2 by DIRAF:40;
not b,e1 // d1,e2
proof
assume b,e1 // d1,e2;
then b,e1 // d1,d2 by A350,A351,AFF_1:5;
then b,c // d1,d2 by A348,A349,AFF_1:5;
hence contradiction by A22,A339,A347,AFF_1:5;
end;
then consider d5 such that
A352: LIN b,e1,d5 and
A353: LIN d1,e2,d5 by AFF_1:60;
b,e1 // b,d5 by A352,AFF_1:def 1;
then
A354: b,c // b,d5 by A348,A349,AFF_1:5;
take d5;
d1,e2 // d1,d5 by A353,AFF_1:def 1;
then d1,d2 // d1,d5 by A350,A351,AFF_1:5;
hence thesis by A354,AFF_1:def 1;
end;
then consider d5 such that
A355: LIN b,c,d5 and
A356: LIN d1,d2,d5;
A357: d in Y by A9,A10,A15,A297,A282,AFF_1:25;
A358: now
A359: not LIN a,b,d
proof
A360: a<>d
proof
A361: a1<>b1
proof
o,a1 // o,a by A3,A9,A10,A15,AFF_1:39,41;
then
A362: LIN o,a1,a by AFF_1:def 1;
assume a1=b1;
hence contradiction by A4,A12,A16,A283,A307,A362,AFF_1:25;
end;
assume
A363: a=d;
then LIN a,b,c by A280,AFF_1:6;
then a,b // a,c by AFF_1:def 1;
then a1,b1 // a,c by A11,A20,A283,AFF_1:5;
then a1,b1 // a1,c1 by A13,A21,A283,AFF_1:5;
then LIN a1,b1,c1 by AFF_1:def 1;
then LIN b1,c1,a1 by AFF_1:6;
then b1,c1 // b1,a1 by AFF_1:def 1;
then
A364: b1,c1 // a1,b1 by AFF_1:4;
b,c // b,a by A280,A363,AFF_1:def 1;
then b,c // a,b by AFF_1:4;
then b,c // a1,b1 by A11,A20,A283,AFF_1:5;
hence contradiction by A22,A364,A361,AFF_1:5;
end;
assume LIN a,b,d;
then LIN a,d,b by AFF_1:6;
then b in Y by A9,A15,A357,A360,AFF_1:25;
then
A365: o,b // Y by A3,A15,AFF_1:52;
o,b // Z by A4,A11,A16,AFF_1:52;
hence contradiction by A3,A4,A7,A18,A365,AFF_1:45,53;
end;
assume
A366: LIN a,d,d5;
A367: o<>d
proof
A368: o,b // o,b1 by A4,A11,A12,A16,AFF_1:39,41;
assume
A369: o=d;
then LIN o,b,c by A280,AFF_1:6;
then o,b // o,c by AFF_1:def 1;
then
A370: o,b1 // o,c by A7,A368,AFF_1:5;
o,c // o,c1 by A5,A13,A14,A17,AFF_1:39,41;
then o,b1 // o,c1 by A8,A370,AFF_1:5;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:6;
then b1,c1 // b1,o by AFF_1:def 1;
then
A371: b1,c1 // o,b1 by AFF_1:4;
b,c // b,o by A280,A369,AFF_1:def 1;
then b,c // o,b by AFF_1:4;
then b,c // o,b1 by A7,A368,AFF_1:5;
hence contradiction by A22,A307,A371,AFF_1:5;
end;
A372: d<>d1
proof
assume d=d1;
then
A373: o,d // Z by A4,A16,A337,AFF_1:52;
o,d // Y by A3,A15,A357,AFF_1:52;
hence contradiction by A3,A4,A18,A367,A373,AFF_1:45,53;
end;
A374: d<>d2
proof
assume d=d2;
then
A375: o,d // M by A5,A17,A335,AFF_1:52;
o,d // Y by A3,A15,A357,AFF_1:52;
hence contradiction by A3,A5,A19,A367,A375,AFF_1:45,53;
end;
A376: b,c // b,d5 by A355,AFF_1:def 1;
A377: b,c // b,d by A280,AFF_1:def 1;
b<>c by A22,AFF_1:3;
then b,d // b,d5 by A377,A376,AFF_1:5;
then LIN d1,d2,d by A356,A366,A359,AFF_1:14;
then LIN d,d1,d2 by AFF_1:6;
then d,d1 // d,d2 by AFF_1:def 1;
then a,b // d,d2 by A336,A372,AFF_1:5;
then
A378: a,b // a,c by A334,A374,AFF_1:5;
then LIN a,b,c by AFF_1:def 1;
then LIN b,c,a by AFF_1:6;
then b,c // b, a by AFF_1:def 1;
then b,c // a,b by AFF_1:4;
then
A379: b,c // a1,b1 by A11,A20,A283,AFF_1:5;
a1,b1 // a,c by A11,A20,A283,A378,AFF_1:5;
then a1,b1 // a1,c1 by A13,A21,A283,AFF_1:5;
then LIN a1,b1,c1 by AFF_1:def 1;
then LIN b1,c1,a1 by AFF_1:6;
then b1,c1 // b1,a1 by AFF_1:def 1;
then
A380: b1,c1 // a1,b1 by AFF_1:4;
a1<>b1
proof
o,a1 // o,a by A3,A9,A10,A15,AFF_1:39,41;
then
A381: LIN o,a1,a by AFF_1:def 1;
assume a1=b1;
hence contradiction by A4,A12,A16,A283,A307,A381,AFF_1:25;
end;
hence contradiction by A22,A380,A379,AFF_1:5;
end;
not b,c // d1,d2 by A22,A339,A347,AFF_1:5;
hence
contradiction by A2,A3,A4,A5,A6,A7,A8,A9,A11,A13,A15,A16,A17,A18,A19
,A23,A336,A337,A334,A335,A355,A356,A357,A358;
end;
now
A382: d in Y by A9,A10,A15,A297,A282,AFF_1:25;
A383: not LIN a1,b1,d
proof
A384: a1<>d
proof
A385: a1<>b1 & a1<>c1
proof
o,a1 // o,a by A3,A9,A10,A15,AFF_1:39,41;
then
A386: LIN o,a1,a by AFF_1:def 1;
assume not thesis;
hence contradiction by A4,A5,A12,A14,A16,A17,A283,A307,A386,
AFF_1:25;
end;
assume
A387: a1=d;
then LIN a1,b1,c1 by A281,AFF_1:6;
then a1,b1 // a1,c1 by AFF_1:def 1;
then a,b // a1,c1 by A20,A385,AFF_1:5;
then a,b // a,c by A21,A385,AFF_1:5;
then LIN a,b,c by AFF_1:def 1;
then LIN b,c,a by AFF_1:6;
then b,c // b,a by AFF_1:def 1;
then
A388: b,c // a,b by AFF_1:4;
b1,c1 // b1,a1 by A281,A387,AFF_1:def 1;
then b1,c1 // a1,b1 by AFF_1:4;
then b1,c1 // a,b by A20,A385,AFF_1:5;
hence contradiction by A11,A22,A283,A388,AFF_1:5;
end;
assume LIN a1,b1,d;
then LIN a1,d,b1 by AFF_1:6;
then b1 in Y by A10,A15,A382,A384,AFF_1:25;
then o,b1 // o,a by A3,A9,A15,AFF_1:39,41;
then LIN o,b1,a by AFF_1:def 1;
hence contradiction by A4,A12,A16,A283,A307,AFF_1:25;
end;
A389: d<>o
proof
A390: o,b // o,b1 by A4,A11,A12,A16,AFF_1:39,41;
assume
A391: d=o;
then LIN o,b,c by A280,AFF_1:6;
then o,b // o,c by AFF_1:def 1;
then
A392: o,b1 // o,c by A7,A390,AFF_1:5;
o,c // o,c1 by A5,A13,A14,A17,AFF_1:39,41;
then o,b1 // o,c1 by A8,A392,AFF_1:5;
then LIN o,b1,c1 by AFF_1:def 1;
then LIN b1,c1,o by AFF_1:6;
then b1,c1 // b1,o by AFF_1:def 1;
then
A393: b1,c1 // o,b1 by AFF_1:4;
b,c // b,o by A280,A391,AFF_1:def 1;
then b,c // o,b by AFF_1:4;
then b,c // o,b1 by A7,A390,AFF_1:5;
hence contradiction by A22,A307,A393,AFF_1:5;
end;
A394: d<>d1
proof
o,d // o,a by A3,A9,A15,A382,AFF_1:39,41;
then
A395: LIN o,d,a by AFF_1:def 1;
assume d=d1;
hence contradiction by A4,A16,A283,A337,A389,A395,AFF_1:25;
end;
A396: d<>d2
proof
o,d // o,a by A3,A9,A15,A382,AFF_1:39,41;
then
A397: LIN o,d,a by AFF_1:def 1;
assume d=d2;
hence contradiction by A5,A17,A283,A335,A389,A397,AFF_1:25;
end;
A398: a1,c1 // d,d2 by A13,A21,A283,A334,AFF_1:5;
A399: b1<>c1 by A22,AFF_1:3;
A400: b1,c1 // b1,d by A281,AFF_1:def 1;
assume
A401: not b1,c1 // d1,d2;
then consider d5 such that
A402: LIN b1,c1,d5 and
A403: LIN d1,d2,d5 by AFF_1:60;
b1,c1 // b1,d5 by A402,AFF_1:def 1;
then
A404: b1,d // b1,d5 by A399,A400,AFF_1:5;
a1,b1 // d,d1 by A11,A20,A283,A336,AFF_1:5;
then LIN a1,d,d5 by A2,A3,A4,A5,A10,A12,A14,A15,A16,A17,A18,A19,A23
,A307,A337,A335,A401,A402,A403,A382,A398;
then d=d5 by A383,A404,AFF_1:14;
then LIN d,d1,d2 by A403,AFF_1:6;
then d,d1 // d,d2 by AFF_1:def 1;
then a,b // d,d2 by A336,A394,AFF_1:5;
then
A405: a,b // a,c by A334,A396,AFF_1:5;
then LIN a,b,c by AFF_1:def 1;
then LIN b,c,a by AFF_1:6;
then b,c // b, a by AFF_1:def 1;
then b,c // a,b by AFF_1:4;
then
A406: b,c // a1,b1 by A11,A20,A283,AFF_1:5;
a1,b1 // a,c by A11,A20,A283,A405,AFF_1:5;
then a1,b1 // a1,c1 by A13,A21,A283,AFF_1:5;
then LIN a1,b1,c1 by AFF_1:def 1;
then LIN b1,c1,a1 by AFF_1:6;
then b1,c1 // b1,a1 by AFF_1:def 1;
then
A407: b1,c1 // a1,b1 by AFF_1:4;
a1<>b1
proof
o,a1 // o,a by A3,A9,A10,A15,AFF_1:39,41;
then
A408: LIN o,a1,a by AFF_1:def 1;
assume a1=b1;
hence contradiction by A4,A12,A16,A283,A307,A408,AFF_1:25;
end;
hence contradiction by A22,A407,A406,AFF_1:5;
end;
hence contradiction by A346;
end;
now
assume
A409: Z // M;
then
A410: b1 in M by A4,A5,A12,AFF_1:45;
b in M by A4,A5,A11,A409,AFF_1:45;
hence contradiction by A13,A14,A17,A22,A410,AFF_1:39,41;
end;
hence contradiction by A278;
end;
hence thesis by AFF_2:def 4;
end;
X is Desarguesian implies X is satisfying_Scherungssatz
proof
assume
A411: X is Desarguesian;
then X is satisfying_TDES_1 by AFF_2:3,12;
then X is satisfying_des_1 by AFF_2:13;
then X is translational by AFF_2:7;
then
A412: X is satisfying_minor_Scherungssatz by Th6;
X is satisfying_major_Scherungssatz by A411,Th7;
hence thesis by A412,Th2;
end;
hence thesis by A1;
end;
theorem Th9:
X is satisfying_pap iff X is satisfying_minor_indirect_Scherungssatz
proof
A1: X is satisfying_minor_indirect_Scherungssatz implies X is satisfying_pap
proof
assume
A2: X is satisfying_minor_indirect_Scherungssatz;
now
let M,N,a,b,c,a1,b1,c1;
assume that
M is being_line and
N is being_line and
A3: a in M and
A4: b in M and
A5: c in M and
A6: M // N and
A7: M<>N and
A8: a1 in N and
A9: b1 in N and
A10: c1 in N and
A11: a,b1 // b,a1 and
A12: b,c1 // c,b1;
A13: not b in N by A4,A6,A7,AFF_1:45;
A14: not c1 in M by A6,A7,A10,AFF_1:45;
A15: not c in N by A5,A6,A7,AFF_1:45;
A16: b1,b // b,b1 by AFF_1:2;
A17: not b1 in M by A6,A7,A9,AFF_1:45;
A18: b,c1 // b1,c by A12,AFF_1:4;
A19: not a1 in M by A6,A7,A8,AFF_1:45;
A20: a,b1 // a1,b by A11,AFF_1:4;
not a in N by A3,A6,A7,AFF_1:45;
then a,c1 // a1,c by A2,A3,A4,A5,A6,A8,A9,A10,A13,A15,A19,A17,A14,A20,A18
,A16;
hence a,c1 // c,a1 by AFF_1:4;
end;
hence thesis by AFF_2:def 13;
end;
X is satisfying_pap implies X is satisfying_minor_indirect_Scherungssatz
proof
assume
A21: X is satisfying_pap;
now
let a1,a2,a3,a4,b1,b2,b3,b4,M,N;
assume that
A22: M // N and
A23: a1 in M and
A24: a3 in M and
A25: b2 in M and
A26: b4 in M and
A27: a2 in N and
A28: a4 in N and
A29: b1 in N and
A30: b3 in N and
A31: not a4 in M and
not a2 in M and
not b1 in M and
not b3 in M and
not a1 in N and
not a3 in N and
not b2 in N and
not b4 in N and
A32: a3,a2 // b3,b2 and
A33: a2,a1 // b2,b1 and
A34: a1,a4 // b1,b4;
A35: M is being_line by A22,AFF_1:36;
A36: b2,b3 // a3,a2 by A32,AFF_1:4;
A37: N is being_line by A22,AFF_1:36;
A38: a4,a1 // b1,b4 by A34,AFF_1:4;
a1,a2 // b2,b1 by A33,AFF_1:4;
then a1,b3 // a3,b1 by A21,A22,A23,A24,A25,A27,A28,A29,A30,A31,A35,A37
,A36,AFF_2:def 13;
then b1,a3 // b3,a1 by AFF_1:4;
then a4,a3 // b3,b4 by A21,A22,A23,A24,A26,A28,A29,A30,A31,A35,A37,A38,
AFF_2:def 13;
hence a3,a4 // b3,b4 by AFF_1:4;
end;
hence thesis;
end;
hence thesis by A1;
end;
theorem Th10:
X is Pappian iff X is satisfying_major_indirect_Scherungssatz
proof
A1: X is Pappian implies X is satisfying_major_indirect_Scherungssatz
proof
assume
A2: X is Pappian;
then
A3: X is Desarguesian by AFF_2:11;
now
let o,a1,a2,a3,a4,b1,b2,b3,b4,M,N;
assume that
A4: M is being_line and
A5: N is being_line and
A6: o in M and
A7: o in N and
A8: a1 in M and
A9: a3 in M and
A10: b2 in M and
A11: b4 in M and
A12: a2 in N and
A13: a4 in N and
A14: b1 in N and
A15: b3 in N and
A16: not a4 in M and
A17: not a2 in M and
A18: not b1 in M and
A19: not b3 in M and
A20: not a1 in N and
A21: not a3 in N and
A22: not b2 in N and
A23: not b4 in N and
A24: a3,a2 // b3,b2 and
A25: a2,a1 // b2,b1 and
A26: a1,a4 // b1,b4;
A27: now
assume that
A28: a1<>a3 and
A29: a2<>a4;
ex x,y,z st LIN x,y,z & x<>y & x<>z & y<>z
proof
o,a1 // o,a3 by A4,A6,A8,A9,AFF_1:39,41;
then
A30: LIN o,a1,a3 by AFF_1:def 1;
assume not thesis;
hence contradiction by A7,A20,A21,A28,A30;
end;
then consider d such that
A31: LIN a2,a1,d and
A32: a2<>d and
A33: a1<>d by TRANSLAC:1;
A34: a2,a1 // a2,d by A31,AFF_1:def 1;
A35: ex c2 st c2 in M & a2,a3 // b1,c2
proof
consider e2 such that
A36: a1,a3 // a1,e2 and
A37: a1<>e2 by DIRAF:40;
consider e1 such that
A38: a2,a3 // b1,e1 and
A39: b1<>e1 by DIRAF:40;
not b1,e1 // a1,e2
proof
assume b1,e1 // a1,e2;
then a2,a3 // a1,e2 by A38,A39,AFF_1:5;
then a2,a3 // a1,a3 by A36,A37,AFF_1:5;
then a3,a1 // a3,a2 by AFF_1:4;
then LIN a3,a1,a2 by AFF_1:def 1;
hence contradiction by A4,A8,A9,A17,A28,AFF_1:25;
end;
then consider c2 such that
A40: LIN b1,e1,c2 and
A41: LIN a1,e2,c2 by AFF_1:60;
a1,e2 // a1,c2 by A41,AFF_1:def 1;
then a1,a3 // a1,c2 by A36,A37,AFF_1:5;
then
A42: LIN a1,a3,c2 by AFF_1:def 1;
take c2;
b1,e1 // b1,c2 by A40,AFF_1:def 1;
hence thesis by A4,A8,A9,A28,A38,A39,A42,AFF_1:5,25;
end;
A43: ex c1 st c1 in N & a1,a4 // b2,c1
proof
consider e2 such that
A44: a2,a4 // a2,e2 and
A45: a2<>e2 by DIRAF:40;
consider e1 such that
A46: a1,a4 // b2,e1 and
A47: b2<>e1 by DIRAF:40;
not b2,e1 // a2,e2
proof
assume b2,e1 // a2,e2;
then a1,a4 // a2,e2 by A46,A47,AFF_1:5;
then a1,a4 // a2,a4 by A44,A45,AFF_1:5;
then a4,a2 // a4,a1 by AFF_1:4;
then LIN a4,a2,a1 by AFF_1:def 1;
hence contradiction by A5,A12,A13,A20,A29,AFF_1:25;
end;
then consider c1 such that
A48: LIN b2,e1,c1 and
A49: LIN a2,e2,c1 by AFF_1:60;
a2,e2 // a2,c1 by A49,AFF_1:def 1;
then a2,a4 // a2,c1 by A44,A45,AFF_1:5;
then
A50: LIN a2,a4,c1 by AFF_1:def 1;
take c1;
b2,e1 // b2,c1 by A48,AFF_1:def 1;
hence thesis by A5,A12,A13,A29,A46,A47,A50,AFF_1:5,25;
end;
consider c2 such that
A51: c2 in M and
A52: a2,a3 // b1,c2 by A35;
consider c1 such that
A53: c1 in N and
A54: a1,a4 // b2,c1 by A43;
b1,b4 // b2,c1 by A8,A16,A26,A54,AFF_1:5;
then
A55: b4,b1 // b2,c1 by AFF_1:4;
A56: o<>c1 & o<>c2
proof
A57: now
assume o=c2;
then
A58: o,b1 // a2,a3 by A52,AFF_1:4;
o,b1 // a2, a4 by A5,A7,A12,A13,A14,AFF_1:39,41;
then a2,a4 // a2,a3 by A6,A18,A58,AFF_1:5;
then LIN a2,a4,a3 by AFF_1:def 1;
hence contradiction by A5,A12,A13,A21,A29,AFF_1:25;
end;
A59: now
assume o=c1;
then
A60: o,b2 // a1,a4 by A54,AFF_1:4;
o,b2 // a1,a3 by A4,A6,A8,A9,A10,AFF_1:39,41;
then a1,a3 // a1,a4 by A7,A22,A60,AFF_1:5;
then LIN a1,a3,a4 by AFF_1:def 1;
hence contradiction by A4,A8,A9,A16,A28,AFF_1:25;
end;
assume not thesis;
hence contradiction by A59,A57;
end;
a3,a2 // c2,b1 by A52,AFF_1:4;
then b3,b2 // c2,b1 by A9,A17,A24,AFF_1:5;
then b2,b3 // c2,b1 by AFF_1:4;
then
A61: b4,b3 // c2,c1 by A2,A4,A5,A6,A7,A10,A11,A14,A15,A18,A19,A22,A23,A53
,A51,A56,A55,AFF_2:def 2;
LIN a1,a2,d by A31,AFF_1:6;
then a1,a2 // a1,d by AFF_1:def 1;
then a2,a1 // a1, d by AFF_1:4;
then
A62: b2,b1 // a1,d by A8,A17,A25,AFF_1:5;
A63: b1<>b3
proof
assume b1=b3;
then b2,b1 // a2,a3 by A24,AFF_1:4;
then
A64: a2,a1 // a2,a3 by A10,A18,A25,AFF_1:5;
o,a1 // o,a3 by A4,A6,A8,A9,AFF_1:39,41;
then LIN o,a1,a3 by AFF_1:def 1;
hence contradiction by A5,A6,A7,A12,A17,A20,A28,A64,AFF_1:14,25;
end;
A65: c1<>c2
proof
A66: b1<>c1
proof
assume b1=c1;
then a1,a4 // a2,a1 by A10,A18,A25,A54,AFF_1:5;
then a1,a4 // a1,a2 by AFF_1:4;
then LIN a1,a4,a2 by AFF_1:def 1;
then LIN a2,a4,a1 by AFF_1:6;
hence contradiction by A5,A12,A13,A20,A29,AFF_1:25;
end;
assume c1=c2;
then a3,a2 // b1,c1 by A52,AFF_1:4;
then
A67: b3,b2 // b1,c1 by A9,A17,A24,AFF_1:5;
b1,c1 // b3,b1 by A5,A14,A15,A53,AFF_1:39,41;
then b3,b1 // b3,b2 by A67,A66,AFF_1:5;
then LIN b3,b1,b2 by AFF_1:def 1;
hence contradiction by A5,A14,A15,A22,A63,AFF_1:25;
end;
LIN o,d,d by AFF_1:7;
then consider Y such that
A68: Y is being_line and
A69: o in Y and
A70: d in Y and
d in Y by AFF_1:21;
A71: M<>N & M<>Y & N<>Y
proof
A72: now
assume
A73: N=Y;
LIN a2,d,a1 by A31,AFF_1:6;
hence contradiction by A5,A12,A20,A32,A70,A73,AFF_1:25;
end;
A74: now
assume
A75: M=Y;
LIN a1,d,a2 by A31,AFF_1:6;
hence contradiction by A4,A8,A17,A33,A70,A75,AFF_1:25;
end;
assume not thesis;
hence contradiction by A13,A16,A74,A72;
end;
A76: o<>d
proof
assume o=d;
then LIN o,a1,a2 by A31,AFF_1:6;
hence contradiction by A4,A6,A7,A8,A17,A20,AFF_1:25;
end;
ex d1 st LIN b1,b2,d1 & d1 in Y
proof
consider e2 such that
A77: o,d // o,e2 and
A78: o<>e2 by DIRAF:40;
consider e1 such that
A79: b1,b2 // b1,e1 and
A80: b1<>e1 by DIRAF:40;
not b1,e1 // o,e2
proof
assume b1,e1 // o,e2;
then b1,b2 // o,e2 by A79,A80,AFF_1:5;
then b1,b2 // o,d by A77,A78,AFF_1:5;
then b2,b1 // o,d by AFF_1:4;
then
A81: a2,a1 // o,d by A10,A18,A25,AFF_1:5;
a2,a1 // a2,d by A31,AFF_1:def 1;
then a2,d // o,d by A8,A17,A81,AFF_1:5;
then d,o // d,a2 by AFF_1:4;
then LIN d,o,a2 by AFF_1:def 1;
then
A82: LIN o,a2,d by AFF_1:6;
LIN a1,a2,d by A31,AFF_1:6;
then a1,a2 // a1,d by AFF_1:def 1;
hence contradiction by A4,A6,A7,A8,A17,A20,A32,A82,AFF_1:14,25;
end;
then consider d1 such that
A83: LIN b1,e1,d1 and
A84: LIN o,e2,d1 by AFF_1:60;
o,e2 // o,d1 by A84,AFF_1:def 1;
then o,d // o,d1 by A77,A78,AFF_1:5;
then
A85: LIN o,d,d1 by AFF_1:def 1;
take d1;
b1,e1 // b1,d1 by A83,AFF_1:def 1;
then b1,b2 // b1,d1 by A79,A80,AFF_1:5;
hence thesis by A76,A68,A69,A70,A85,AFF_1:25,def 1;
end;
then consider d1 such that
A86: LIN b1,b2,d1 and
A87: d1 in Y;
LIN b2,b1,d1 by A86,AFF_1:6;
then b2,b1 // b2,d1 by AFF_1:def 1;
then a1,d // b2,d1 by A10,A18,A62,AFF_1:5;
then
A88: d,a4 // d1,c1 by A3,A4,A5,A6,A7,A8,A10,A13,A16,A20,A76,A68,A69,A70,A87
,A53,A54,A71,AFF_2:def 4;
b1,b2 // b1,d1 by A86,AFF_1:def 1;
then b2,b1 // b1,d1 by AFF_1:4;
then a2,a1 // b1,d1 by A10,A18,A25,AFF_1:5;
then a2,d // b1,d1 by A8,A17,A34,AFF_1:5;
then d,a3 // d1,c2 by A3,A4,A5,A6,A7,A9,A12,A14,A17,A21,A76,A68,A69,A70
,A87,A51,A52,A71,AFF_2:def 4;
then a3,a4 // c2,c1 by A3,A4,A5,A6,A7,A9,A13,A16,A21,A76,A68,A69,A70
,A87,A53,A51,A71,A88,AFF_2:def 4;
then b4,b3 // a3,a4 by A65,A61,AFF_1:5;
hence a3,a4 // b3,b4 by AFF_1:4;
end;
now
A89: now
o,b2 // o,b4 by A4,A6,A10,A11,AFF_1:39,41;
then
A90: LIN o,b2,b4 by AFF_1:def 1;
assume
A91: a2=a4;
then a1,a4 // b1,b2 by A25,AFF_1:4;
then b1,b2 // b1,b4 by A8,A16,A26,AFF_1:5;
hence a3,a4 // b3,b4 by A5,A6,A7,A14,A18,A22,A24,A91,A90,AFF_1:14,25;
end;
A92: now
o,b1 // o,b3 by A5,A7,A14,A15,AFF_1:39,41;
then
A93: LIN o,b1,b3 by AFF_1:def 1;
assume
A94: a1=a3;
then a2,a1 // b2,b3 by A24,AFF_1:4;
then b2,b1 // b2,b3 by A8,A17,A25,AFF_1:5;
hence a3,a4 // b3,b4 by A4,A6,A7,A10,A18,A22,A26,A94,A93,AFF_1:14,25;
end;
assume a1=a3 or a2=a4;
hence a3,a4 // b3,b4 by A92,A89;
end;
hence a3,a4 // b3,b4 by A27;
end;
hence thesis;
end;
X is satisfying_major_indirect_Scherungssatz implies X is Pappian
proof
assume
A95: X is satisfying_major_indirect_Scherungssatz;
now
let M,N,o,a,b,c,a1,b1,c1;
assume that
A96: M is being_line and
A97: N is being_line and
A98: M<>N and
A99: o in M and
A100: o in N and
A101: o<>a and
A102: o<>a1 and
A103: o<>b and
A104: o<>b1 and
A105: o<>c and
A106: o<>c1 and
A107: a in M and
A108: b in M and
A109: c in M and
A110: a1 in N and
A111: b1 in N and
A112: c1 in N and
A113: a,b1 // b,a1 and
A114: b,c1 // c,b1;
A115: 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
A116: o,c1 // o,c1 by AFF_1:2;
A117: o,b1 // o,b1 by AFF_1:2;
A118: o,a1 // o,a1 by AFF_1:2;
A119: o,c // o,c by AFF_1:2;
A120: o,b // o,b by AFF_1:2;
A121: o,a // o,a by AFF_1:2;
assume not thesis;
then M // N by A96,A97,A99,A100,A101,A102,A103,A104,A105,A106,A107,A108
,A109,A110,A111,A112,A121,A120,A119,A118,A117,A116,AFF_1:38;
hence contradiction by A98,A99,A100,AFF_1:45;
end;
A122: b,c1 // b1,c by A114,AFF_1:4;
A123: b1,b // b,b1 by AFF_1:2;
a,b1 // a1,b by A113,AFF_1:4;
then a,c1 // a1,c by A95,A96,A97,A99,A100,A107,A108,A109,A110,A111,A112
,A115,A122,A123;
hence a,c1 // c,a1 by AFF_1:4;
end;
hence thesis by AFF_2:def 2;
end;
hence thesis by A1;
end;
theorem
X is satisfying_PPAP iff X is satisfying_indirect_Scherungssatz
proof
A1: X is satisfying_PPAP implies X is satisfying_indirect_Scherungssatz
proof
assume
A2: X is satisfying_PPAP;
then X is satisfying_pap by AFF_2:10;
then
A3: X is satisfying_minor_indirect_Scherungssatz by Th9;
X is Pappian by A2,AFF_2:10;
then X is satisfying_major_indirect_Scherungssatz by Th10;
hence thesis by A3,Th1;
end;
X is satisfying_indirect_Scherungssatz implies X is satisfying_PPAP
proof
assume
A4: X is satisfying_indirect_Scherungssatz;
then X is satisfying_major_indirect_Scherungssatz;
then
A5: X is Pappian by Th10;
X is satisfying_minor_indirect_Scherungssatz by A4,Th1;
then X is satisfying_pap by Th9;
hence thesis by A5,AFF_2:10;
end;
hence thesis by A1;
end;
theorem
X is satisfying_major_indirect_Scherungssatz implies X is
satisfying_minor_indirect_Scherungssatz
proof
assume X is satisfying_major_indirect_Scherungssatz;
then X is Pappian by Th10;
then X is satisfying_pap by AFF_2:9;
hence thesis by Th9;
end;
reserve X for OrtAfPl;
reserve o9,a9,a19,a29,a39,a49,b9,b19,b29,b39,b49,c9,c19 for Element of X;
reserve o,a,a1,a2,a3,a4,b,b1,b2,b3,b4,c,c1 for Element of the AffinStruct of X;
reserve M9,N9 for Subset of X;
reserve A,M,N for Subset of the AffinStruct of X;
theorem
the AffinStruct of X is satisfying_Scherungssatz iff X is satisfying_SCH
proof
A1: X is satisfying_SCH implies
the AffinStruct of X is satisfying_Scherungssatz
proof
assume
A2: X is satisfying_SCH;
now
let a1,a2,a3,a4,b1,b2,b3,b4,M,N;
assume that
A3: M is being_line and
A4: N is being_line and
A5: a1 in M and
A6: a3 in M and
A7: b1 in M and
A8: b3 in M and
A9: a2 in N and
A10: a4 in N and
A11: b2 in N and
A12: b4 in N and
A13: not a4 in M and
A14: not a2 in M and
A15: not b2 in M and
A16: not b4 in M and
A17: not a1 in N and
A18: not a3 in N and
A19: not b1 in N and
A20: not b3 in N and
A21: a3,a2 // b3,b2 and
A22: a2,a1 // b2,b1 and
A23: a1,a4 // b1,b4;
reconsider a19=a1,a29=a2,a39=a3,a49=a4,b19=b1,b29=b2,b39=b3,b49=b4 as
Element of X;
A24: a39,a29 // b39,b29 by A21,ANALMETR:36;
A25: a19,a49 // b19,b49 by A23,ANALMETR:36;
A26: a29,a19 // b29,b19 by A22,ANALMETR:36;
reconsider M9=M,N9=N as Subset of X;
A27: N9 is being_line by A4,ANALMETR:43;
M9 is being_line by A3,ANALMETR:43;
then
a39,a49 // b39,b49 by A2,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,A15,A16,A17
,A18,A19,A20,A27,A24,A26,A25,CONMETR:def 6;
hence a3,a4 // b3,b4 by ANALMETR:36;
end;
hence thesis;
end;
the AffinStruct of X is satisfying_Scherungssatz implies X is satisfying_SCH
proof
assume
A28: the AffinStruct of X is satisfying_Scherungssatz;
now
let a19,a29,a39,a49,b19,b29,b39,b49,M9,N9;
assume that
A29: M9 is being_line and
A30: N9 is being_line and
A31: a19 in M9 and
A32: a39 in M9 and
A33: b19 in M9 and
A34: b39 in M9 and
A35: a29 in N9 and
A36: a49 in N9 and
A37: b29 in N9 and
A38: b49 in N9 and
A39: not a49 in M9 and
A40: not a29 in M9 and
A41: not b29 in M9 and
A42: not b49 in M9 and
A43: not a19 in N9 and
A44: not a39 in N9 and
A45: not b19 in N9 and
A46: not b39 in N9 and
A47: a39,a29 // b39,b29 and
A48: a29,a19 // b29,b19 and
A49: a19,a49 // b19,b49;
reconsider a1=a19,a2=a29,a3=a39,a4=a49,b1=b19,b2=b29,b3=b39,b4=b49 as
Element of the AffinStruct of X;
A50: a3,a2 // b3,b2 by A47,ANALMETR:36;
A51: a1,a4 // b1,b4 by A49,ANALMETR:36;
A52: a2,a1 // b2,b1 by A48,ANALMETR:36;
reconsider M=M9,N=N9 as Subset of the AffinStruct of X;
A53: N is being_line by A30,ANALMETR:43;
M is being_line by A29,ANALMETR:43;
then a3,a4 // b3,b4 by A28,A31,A32,A33,A34,A35,A36,A37,A38,A39,A40,A41
,A42,A43,A44,A45,A46,A53,A50,A52,A51;
hence a39,a49 // b39,b49 by ANALMETR:36;
end;
hence thesis by CONMETR:def 6;
end;
hence thesis by A1;
end;
theorem
X is satisfying_TDES iff the AffinStruct of X is Moufangian
proof
the AffinStruct of X is Moufangian implies X is satisfying_TDES
proof
assume
A1: the AffinStruct of X is Moufangian;
now
let o9,a9,a19,b9,b19,c9,c19;
assume that
o9<>a9 and
o9<>a19 and
A2: o9<>b9 and
o9<>b19 and
A3: o9<>c9 and
o9<>c19 and
A4: not LIN b9,b19,a9 and
A5: not LIN b9,b19,c9 and
A6: LIN o9,a9,a19 and
A7: LIN o9,b9,b19 and
A8: LIN o9,c9,c19 and
A9: a9,b9 // a19,b19 and
A10: a9,b9 // o9,c9 and
A11: b9,c9 // b19,c19;
reconsider o=o9,a=a9,a1=a19,b=b9,b1=b19,c =c9,c1=c19 as Element
of the AffinStruct of X;
A12: LIN o,b,b1 by A7,ANALMETR:40;
LIN o,c,c1 by A8,ANALMETR:40;
then consider M such that
A13: M is being_line and
A14: o in M and
A15: c in M and
A16: c1 in M by AFF_1:21;
A17: not LIN b,b1,c by A5,ANALMETR:40;
A18: not b in M
proof
LIN b,b1,o by A12,AFF_1:6;
then b,b1 // b,o by AFF_1:def 1;
then
A19: b,b1 // o,b by AFF_1:4;
assume b in M;
then o,b // b,c by A13,A14,A15,AFF_1:39,41;
then b,b1 // b,c by A2,A19,AFF_1:5;
hence contradiction by A17,AFF_1:def 1;
end;
a,b // a1,b1 by A9,ANALMETR:36;
then
A20: b,a // b1,a1 by AFF_1:4;
not LIN b,b1,a by A4,ANALMETR:40;
then
A21: b<>a by AFF_1:7;
A22: b,c // b1,c1 by A11,ANALMETR:36;
A23: LIN o,a,a1 by A6,ANALMETR:40;
a,b // o,c by A10,ANALMETR:36;
then b,a // o,c by AFF_1:4;
then b,a // M by A3,A13,A14,A15,AFF_1:27;
then a,c // a1,c1 by A1,A3,A23,A12,A13,A14,A15,A16,A18,A21,A20,A22,
AFF_2:def 7;
hence a9,c9 // a19,c19 by ANALMETR:36;
end;
hence thesis by CONMETR:def 5;
end;
hence thesis by CONMETR:7;
end;
theorem
the AffinStruct of X is translational iff X is satisfying_des
proof
X is satisfying_des implies the AffinStruct of X is translational
proof
assume
A1: X is satisfying_des;
now
let A,M,N,a,b,c,a1,b1,c1;
assume that
A2: A // M and
A3: A // N and
A4: a in A and
A5: a1 in A and
A6: b in M and
A7: b1 in M and
A8: c in N and
A9: c1 in N and
A10: A is being_line and
A11: M is being_line and
A12: N is being_line and
A13: A<>M and
A14: A<>N and
A15: a,b // a1,b1 and
A16: a,c // a1,c1;
reconsider a9=a,a19=a1,b9=b,b19=b1,c9=c,c19=c1 as Element of X;
b,c // b1,c1
proof
assume
A17: not b,c // b1,c1;
A18: a<>a1
proof
assume
A19: a=a1;
A20: c =c1
proof
LIN a,c,c1 by A16,A19,AFF_1:def 1;
then
A21: LIN c,c1,a by AFF_1:6;
assume c <>c1;
then a in N by A8,A9,A12,A21,AFF_1:25;
hence contradiction by A3,A4,A14,AFF_1:45;
end;
b=b1
proof
LIN a,b,b1 by A15,A19,AFF_1:def 1;
then
A22: LIN b,b1,a by AFF_1:6;
assume b<>b1;
then a in M by A6,A7,A11,A22,AFF_1:25;
hence contradiction by A2,A4,A13,AFF_1:45;
end;
hence contradiction by A17,A20,AFF_1:2;
end;
A23: not LIN a9,a19,b9 & not LIN a9,a19,c9
proof
assume LIN a9,a19,b9 or LIN a9,a19,c9;
then LIN a,a1,b or LIN a,a1,c by ANALMETR:40;
then b in A or c in A by A4,A5,A10,A18,AFF_1:25;
hence contradiction by A2,A3,A6,A8,A13,A14,AFF_1:45;
end;
a,a1 // c,c1 by A3,A4,A5,A8,A9,AFF_1:39;
then
A24: a9,a19 // c9,c19 by ANALMETR:36;
a,a1 // b,b1 by A2,A4,A5,A6,A7,AFF_1:39;
then
A25: a9,a19 // b9,b19 by ANALMETR:36;
A26: a9,c9 // a19,c19 by A16,ANALMETR:36;
a9,b9 // a19,b19 by A15,ANALMETR:36;
then b9,c9 // b19,c19 by A1,A23,A25,A24,A26,CONMETR:def 8;
hence contradiction by A17,ANALMETR:36;
end;
hence b,c // b1,c1;
end;
hence thesis by AFF_2:def 11;
end;
hence thesis by CONMETR:8;
end;
theorem
X is satisfying_PAP iff the AffinStruct of X is Pappian
proof
A1: X is satisfying_PAP implies the AffinStruct of X is Pappian
proof
assume
A2: X is satisfying_PAP;
now
let M,N,o,a,b,c,a1,b1,c1;
assume that
A3: M is being_line and
A4: N is being_line and
A5: M<>N and
A6: o in M and
A7: o in N and
A8: o<>a and
A9: o<>a1 and
A10: o<>b and
A11: o<>b1 and
A12: o<>c and
A13: o<>c1 and
A14: a in M and
A15: b in M and
A16: c in M and
A17: a1 in N and
A18: b1 in N and
A19: c1 in N and
A20: a,b1 // b,a1 and
A21: b,c1 // c,b1;
reconsider a9=a,b9=b,c9=c,a19=a1,b19=b1,c19=c1 as Element of X;
reconsider M9=M,N9=N as Subset of X;
A22: N9 is being_line by A4,ANALMETR:43;
A23: not c19 in M9 & not b9 in N9
proof
assume c19 in M9 or b9 in N9;
then
A24: o,c1 // M or o,b // N by A3,A4,A6,A7,AFF_1:52;
A25: o,b // M by A3,A6,A15,AFF_1:52;
o,c1 // N by A4,A7,A19,AFF_1:52;
hence contradiction by A5,A6,A7,A10,A13,A24,A25,AFF_1:45,53;
end;
b,a1 // a,b1 by A20,AFF_1:4;
then
A26: b9,a19 // a9,b19 by ANALMETR:36;
A27: b9,c19 // c9,b19 by A21,ANALMETR:36;
M9 is being_line by A3,ANALMETR:43;
then
a9,c19 // c9,a19 by A2,A6,A7,A8,A9,A11,A12,A14,A15,A16,A17,A18,A19,A22
,A26,A27,A23,CONMETR:def 2;
hence a,c1 // c,a1 by ANALMETR:36;
end;
hence thesis by AFF_2:def 2;
end;
the AffinStruct of X is Pappian implies X is satisfying_PAP
proof
assume
A28: the AffinStruct of X is Pappian;
now
let o9,a19,a29,a39,b19,b29,b39,M9,N9;
assume that
A29: M9 is being_line and
A30: N9 is being_line and
A31: o9 in M9 and
A32: a19 in M9 and
A33: a29 in M9 and
A34: a39 in M9 and
A35: o9 in N9 and
A36: b19 in N9 and
A37: b29 in N9 and
A38: b39 in N9 and
A39: not b29 in M9 and
A40: not a39 in N9 and
A41: o9<>a19 and
A42: o9<>a29 and
o9<>a39 and
A43: o9<>b19 and
o9<>b29 and
A44: o9<>b39 and
A45: a39,b29 // a29,b19 and
A46: a39,b39 // a19,b19;
reconsider a1=a19,a2=a29,a3=a39,b1=b19,b2=b29,b3=b39
as Element of the AffinStruct of X;
reconsider M=M9,N=N9 as Subset of the AffinStruct of X;
A47: N is being_line by A30,ANALMETR:43;
A48: M is being_line by A29,ANALMETR:43;
now
assume M<>N;
a3,b3 // a1,b1 by A46,ANALMETR:36;
then
A49: a1,b1 // a3,b3 by AFF_1:4;
a3,b2 // a2,b1 by A45,ANALMETR:36;
then
a1,b2 // a2,b3 by A28,A31,A32,A33,A34,A35,A36,A37,A38,A39,A40,A41,A42
,A43,A44,A48,A47,A49,AFF_2:def 2;
hence a19,b29 // a29,b39 by ANALMETR:36;
end;
hence a19,b29 // a29,b39 by A37,A39;
end;
hence thesis by CONMETR:def 2;
end;
hence thesis by A1;
end;
theorem
X is satisfying_DES iff the AffinStruct of X is Desarguesian
proof
A1: X is satisfying_DES implies the AffinStruct of X is Desarguesian
proof
assume
A2: X is satisfying_DES;
now
let A,M,N,o,a,b,c,a1,b1,c1;
assume that
A3: o in A and
A4: o in M and
A5: o in N and
A6: o<>a and
A7: o<>b and
A8: o<>c and
A9: a in A and
A10: a1 in A and
A11: b in M and
A12: b1 in M and
A13: c in N and
A14: c1 in N and
A15: A is being_line and
A16: M is being_line and
A17: N is being_line and
A18: A<>M and
A19: A<>N and
A20: a,b // a1,b1 and
A21: a,c // a1,c1;
reconsider o9=o,a9=a,a19=a1,b9=b,b19=b1,c9=c,c19=c1 as Element of X;
o,b // o,b1 by A4,A11,A12,A16,AFF_1:39,41;
then
A22: LIN o,b,b1 by AFF_1:def 1;
then
A23: LIN o9,b9,b19 by ANALMETR:40;
o,a // o,a1 by A3,A9,A10,A15,AFF_1:39,41;
then
A24: LIN o,a, a1 by AFF_1:def 1;
o,c // o,c1 by A5,A13,A14,A17,AFF_1:39,41;
then
A25: LIN o,c,c1 by AFF_1:def 1;
then
A26: LIN o9,c9,c19 by ANALMETR:40;
assume
A27: not b,c // b1,c1;
A28: not LIN b9,b19,a9 & not LIN a9,a19,c9
proof
A29: a<>a1
proof
assume
A30: a=a1;
A31: c =c1
proof
A32: not LIN o,a,c
proof
assume LIN o,a,c;
then c in A by A3,A6,A9,A15,AFF_1:25;
then
A33: o,c // A by A3,A15,AFF_1:52;
o,c // N by A5,A13,A17,AFF_1:52;
hence contradiction by A3,A5,A8,A19,A33,AFF_1:45,53;
end;
assume c <>c1;
hence contradiction by A21,A25,A30,A32,AFF_1:14;
end;
b=b1
proof
A34: not LIN o,a,b
proof
assume LIN o,a,b;
then b in A by A3,A6,A9,A15,AFF_1:25;
then
A35: o,b // A by A3,A15,AFF_1:52;
o,b // M by A4,A11,A16,AFF_1:52;
hence contradiction by A3,A4,A7,A18,A35,AFF_1:45,53;
end;
assume b<>b1;
hence contradiction by A20,A22,A30,A34,AFF_1:14;
end;
hence contradiction by A27,A31,AFF_1:2;
end;
A36: b<>b1
proof
A37: not LIN o,b,a
proof
assume LIN o,b,a;
then a in M by A4,A7,A11,A16,AFF_1:25;
then
A38: o,a // M by A4,A16,AFF_1:52;
o,a // A by A3,A9,A15,AFF_1:52;
hence contradiction by A3,A4,A6,A18,A38,AFF_1:45,53;
end;
assume b=b1;
then b,a // b,a1 by A20,AFF_1:4;
hence contradiction by A24,A29,A37,AFF_1:14;
end;
assume LIN b9,b19,a9 or LIN a9,a19,c9;
then LIN b,b1,a or LIN a,a1,c by ANALMETR:40;
then a in M or c in A by A9,A10,A11,A12,A15,A16,A29,A36,AFF_1:25;
then
A39: o,a // M or o,c // A by A3,A4,A15,A16,AFF_1:52;
A40: o,c // N by A5,A13,A17,AFF_1:52;
o,a // A by A3,A9,A15,AFF_1:52;
hence contradiction by A3,A4,A5,A6,A8,A18,A19,A39,A40,AFF_1:45,53;
end;
A41: a9,c9 // a19,c19 by A21,ANALMETR:36;
A42: a9,b9 // a19,b19 by A20,ANALMETR:36;
A43: o9<>a19 & o9<>b19 & o9<>c19
proof
A44: now
assume
A45: o9=a19;
A46: o=c1
proof
A47: not LIN c,a,o
proof
assume LIN c,a,o;
then LIN o,a,c by AFF_1:6;
then c in A by A3,A6,A9,A15,AFF_1:25;
then
A48: o,c // A by A3,A15,AFF_1:52;
o,c // N by A5,A13,A17,AFF_1:52;
hence contradiction by A3,A5,A8,A19,A48,AFF_1:45,53;
end;
assume
A49: o<>c1;
A50: o,c // o,c1 by A5,A13,A14,A17,AFF_1:39,41;
then a,c // o,c by A21,A45,A49,AFF_1:5;
then c,a // c,o by AFF_1:4;
then LIN c,a,o by AFF_1:def 1;
then LIN o,a,c by AFF_1:6;
then o,a // o,c by AFF_1:def 1;
then o,a // o,c1 by A8,A50,AFF_1:5;
then LIN o,a,c1 by AFF_1:def 1;
then LIN a,o,c1 by AFF_1:6;
then
A51: a,o // a,c1 by AFF_1:def 1;
LIN c,o,c1 by A25,AFF_1:6;
hence contradiction by A49,A47,A51,AFF_1:14;
end;
o=b1
proof
A52: not LIN b,a,o
proof
assume LIN b,a,o;
then LIN o,a,b by AFF_1:6;
then b in A by A3,A6,A9,A15,AFF_1:25;
then
A53: o,b // A by A3,A15,AFF_1:52;
o,b // M by A4,A11,A16,AFF_1:52;
hence contradiction by A3,A4,A7,A18,A53,AFF_1:45,53;
end;
assume
A54: o<>b1;
A55: o,b1 // o,b by A4,A11,A12,A16,AFF_1:39,41;
then a,b // o,b by A20,A45,A54,AFF_1:5;
then b,a // b,o by AFF_1:4;
then LIN b,a,o by AFF_1:def 1;
then LIN o,a,b by AFF_1:6;
then o,a // o,b by AFF_1:def 1;
then o,a // o,b1 by A7,A55,AFF_1:5;
then LIN o,a,b1 by AFF_1:def 1;
then LIN a,o,b1 by AFF_1:6;
then
A56: a,o // a,b1 by AFF_1:def 1;
LIN b,o,b1 by A22,AFF_1:6;
hence contradiction by A54,A52,A56,AFF_1:14;
end;
hence contradiction by A27,A46,AFF_1:3;
end;
A57: now
A58: not LIN a,b,o
proof
assume LIN a,b,o;
then LIN o,a,b by AFF_1:6;
then b in A by A3,A6,A9,A15,AFF_1:25;
then
A59: o,b // A by A3,A15,AFF_1:52;
o,b // M by A4,A11,A16,AFF_1:52;
hence contradiction by A3,A4,A7,A18,A59,AFF_1:45,53;
end;
A60: a1,o // a,o by A3,A9,A10,A15,AFF_1:39,41;
assume o9=b19;
then a,b // a,o by A20,A44,A60,AFF_1:5;
then LIN a,b,o by AFF_1:def 1;
then LIN o,b,a by AFF_1:6;
then o,b // o,a by AFF_1:def 1;
then o,b // a,o by AFF_1:4;
then o,b // a1,o by A6,A60,AFF_1:5;
then o,b // o,a1 by AFF_1:4;
then LIN o,b,a1 by AFF_1:def 1;
then LIN b,o,a1 by AFF_1:6;
then
A61: b,o // b,a1 by AFF_1:def 1;
LIN a,o,a1 by A24,AFF_1:6;
hence contradiction by A44,A58,A61,AFF_1:14;
end;
A62: now
A63: not LIN a,c,o
proof
assume LIN a,c,o;
then LIN o,a,c by AFF_1:6;
then c in A by A3,A6,A9,A15,AFF_1:25;
then
A64: o,c // A by A3,A15,AFF_1:52;
o,c // N by A5,A13,A17,AFF_1:52;
hence contradiction by A3,A5,A8,A19,A64,AFF_1:45,53;
end;
A65: a1,o // a,o by A3,A9,A10,A15,AFF_1:39,41;
assume o9=c19;
then a,c // a,o by A21,A44,A65,AFF_1:5;
then LIN a,c,o by AFF_1:def 1;
then LIN o,c,a by AFF_1:6;
then o,c // o,a by AFF_1:def 1;
then o,c // a,o by AFF_1:4;
then o,c // a1,o by A6,A65,AFF_1:5;
then o,c // o,a1 by AFF_1:4;
then LIN o,c,a1 by AFF_1:def 1;
then LIN c,o,a1 by AFF_1:6;
then
A66: c,o // c,a1 by AFF_1:def 1;
LIN a,o,a1 by A24,AFF_1:6;
hence contradiction by A44,A63,A66,AFF_1:14;
end;
assume not thesis;
hence contradiction by A44,A57,A62;
end;
LIN o9,a9,a19 by A24,ANALMETR:40;
then b9,c9 // b19,c19 by A2,A6,A7,A8,A23,A26,A43,A28,A42,A41,
CONAFFM:def 1;
hence contradiction by A27,ANALMETR:36;
end;
hence thesis by AFF_2:def 4;
end;
the AffinStruct of X is Desarguesian implies X is satisfying_DES
proof
assume
A67: the AffinStruct of X is Desarguesian;
now
let o9,a9,a19,b9,b19,c9,c19;
assume that
A68: o9<>a9 and
o9<>a19 and
A69: o9<>b9 and
o9<>b19 and
A70: o9<>c9 and
o9<>c19 and
A71: not LIN b9,b19,a9 and
A72: not LIN a9,a19,c9 and
A73: LIN o9,a9,a19 and
A74: LIN o9,b9,b19 and
A75: LIN o9,c9,c19 and
A76: a9,b9 // a19,b19 and
A77: a9,c9 // a19,c19;
reconsider o=o9,a=a9,a1=a19,b=b9,b1=b19,c =c9,c1=c19
as Element of the AffinStruct of X;
A78: not LIN a,a1,c by A72,ANALMETR:40;
A79: a,c // a1,c1 by A77,ANALMETR:36;
A80: a,b // a1,b1 by A76,ANALMETR:36;
LIN o,b,b1 by A74,ANALMETR:40;
then consider M such that
A81: M is being_line and
A82: o in M and
A83: b in M and
A84: b1 in M by AFF_1:21;
LIN o,c,c1 by A75,ANALMETR:40;
then consider N such that
A85: N is being_line and
A86: o in N and
A87: c in N and
A88: c1 in N by AFF_1:21;
LIN o,a,a1 by A73,ANALMETR:40;
then consider A such that
A89: A is being_line and
A90: o in A and
A91: a in A and
A92: a1 in A by AFF_1:21;
A93: not LIN b,b1,a by A71,ANALMETR:40;
A<>M & A<>N
proof
assume not thesis;
then
b,b1 // b,a or a,a1 // a,c by A89,A91,A92,A83,A84,A87,AFF_1:39,41;
hence contradiction by A93,A78,AFF_1:def 1;
end;
then b,c // b1,c1 by A67,A68,A69,A70,A89,A90,A91,A92,A81,A82,A83,A84,A85
,A86,A87,A88,A80,A79,AFF_2:def 4;
hence b9,c9 // b19,c19 by ANALMETR:36;
end;
hence thesis by CONAFFM:def 1;
end;
hence thesis by A1;
end;