:: Metric-Affine Configurations in Metric Affine Planes - Part II
:: by Jolanta \'Swierzy\'nska and Bogdan \'Swierzy\'nski
::
:: Received October 31, 1990
:: Copyright (c) 1990-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 ANALMETR, SUBSET_1, SYMSP_1, ANALOAF, AFF_1, DIRAF, INCSP_1,
AFF_2, CONAFFM, STRUCT_0, CONMETR;
notations SUBSET_1, STRUCT_0, ANALOAF, AFF_1, ANALMETR, AFF_2, CONAFFM;
constructors AFF_1, AFF_2, CONAFFM;
registrations ANALMETR;
requirements SUBSET;
definitions AFF_2;
expansions AFF_2;
theorems AFF_1, AFF_2, ANALMETR, TRANSLAC, CONAFFM, DIRAF;
begin
reserve X for OrtAfPl;
reserve o,a,a1,a2,a3,a4,b,b1,b2,b3,b4,c,c1,c2,c3,d,d1,d2,d3,d4,e1,e2 for
Element of X;
reserve a29,a39,b29,x9 for Element of the AffinStruct of X;
reserve A,K,M,N for Subset of X;
reserve A9,K9 for Subset of the AffinStruct of X;
definition
let X;
attr X is satisfying_OPAP means
for o,a1,a2,a3,b1,b2,b3,M,N st o in M
& a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2
in M & not a3 in N & M _|_ N & o<>a1 & o<>a2 & o<>a3 & o<>b1 & o<>b2 & o<>b3 &
a3,b2 // a2,b1 & a3,b3 // a1,b1 holds a1,b2 // a2,b3;
attr X is satisfying_PAP means
for o,a1,a2,a3,b1,b2,b3,M,N st M is
being_line & N is being_line & o in M & a1 in M & a2 in M & a3 in M & o in N &
b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & o<>a1 & o<>a2 & o<>a3
& o<>b1 & o<>b2 & o<>b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds a1,b2 // a2,b3;
attr X is satisfying_MH1 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 a2 in M & not a4 in M & a1,a2 _|_ b1,b2 & a2,a3 _|_ b2,b3 & a3,a4
_|_ b3,b4 holds a1,a4 _|_ b1,b4;
attr X is satisfying_MH2 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 a2 in M & not a4 in M & a1,a2 _|_ b1,b2 & a2,a3 _|_ b2,b3 & a3,a4
_|_ b3,b4 holds a1,a4 _|_ b1,b4;
attr X is satisfying_TDES means
for o,a,a1,b,b1,c,c1 st o<>a & o<>a1
& o<>b & o<>b1 & o<>c & o<>c1 & not LIN b,b1,a & not LIN b,b1,c & LIN o,a,a1 &
LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,b // o,c & b,c // b1,c1 holds a,c //
a1,c1;
attr X is satisfying_SCH 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;
attr X is satisfying_OSCH 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;
attr X is satisfying_des means
for a,a1,b,b1,c,c1 st not LIN a,a1,b &
not LIN a,a1,c & a,a1 // b,b1 & a,a1 // c,c1 & a,b // a1,b1 & a,c // a1,c1
holds b,c // b1,c1;
end;
theorem Th1:
ex a,b,c st LIN a,b,c & a<>b & b<>c & c <>a
proof
consider a,p being Element of X such that
A1: a<>p by ANALMETR:39;
consider b such that
A2: a,p _|_ p,b and
A3: p<>b by ANALMETR:39;
reconsider a9=a,b9=b,p9=p as Element of the AffinStruct of X;
consider c such that
A4: p,c _|_ a,b and
A5: LIN a,b,c by ANALMETR:69;
take a,b,c;
thus LIN a,b,c by A5;
thus a<>b
proof
assume not thesis;
then a,p _|_ a,p by A2,ANALMETR:61;
hence contradiction by A1,ANALMETR:39;
end;
thus b<>c
proof
assume not thesis;
then a,p // a,b by A2,A3,A4,ANALMETR:63;
then LIN a,p,b by ANALMETR:def 10;
then LIN a9,p9,b9 by ANALMETR:40;
then LIN p9,a9,b9 by AFF_1:6;
then LIN p,a,b by ANALMETR:40;
then p,a // p,b by ANALMETR:def 10;
then a,p _|_ p,a by A2,A3,ANALMETR:62;
then a,p _|_ a,p by ANALMETR:61;
hence contradiction by A1,ANALMETR:39;
end;
assume not thesis;
then a,p _|_ a,b by A4,ANALMETR:61;
then p,b // a,b by A1,A2,ANALMETR:63;
then b,p // b,a by ANALMETR:59;
then LIN b,p,a by ANALMETR:def 10;
then LIN b9,p9,a9 by ANALMETR:40;
then LIN p9,a9,b9 by AFF_1:6;
then LIN p,a,b by ANALMETR:40;
then p,a // p,b by ANALMETR:def 10;
then a,p _|_ p,a by A2,A3,ANALMETR:62;
then a,p _|_ a,p by ANALMETR:61;
hence contradiction by A1,ANALMETR:39;
end;
theorem Th2:
for a,b ex c st LIN a,b,c & a<>c & b<>c
proof
let a,b;
consider p,q,r being Element of X such that
A1: LIN p,q,r and
A2: p<>q and
A3: q<>r and
A4: r<>p by Th1;
reconsider a9=a,b9=b,p9=p,q9=q,r9=r as Element of the AffinStruct of X;
LIN p9,q9,r9 by A1,ANALMETR:40;
then consider c9 being Element of the AffinStruct of X such that
A5: LIN a9,b9,c9 and
A6: a9<>c9 and
A7: b9<>c9 by A2,A3,A4,TRANSLAC:1;
reconsider c =c9 as Element of X;
LIN a,b,c by A5,ANALMETR:40;
hence thesis by A6,A7;
end;
theorem Th3:
for A,a st A is being_line ex K st a in K & A _|_ K
proof
let A,a;
assume A is being_line;
then consider b,c such that
A1: b<>c and
A2: A = Line(b,c) by ANALMETR:def 12;
consider d such that
A3: b,c _|_ a,d and
A4: a<>d by ANALMETR:39;
reconsider a9=a,d9=d as Element of the AffinStruct of X;
take K = Line(a,d);
K = Line(a9,d9) by ANALMETR:41;
hence a in K by AFF_1:15;
thus thesis by A1,A2,A3,A4,ANALMETR:45;
end;
theorem Th4:
A is being_line & a in A & b in A & c in A implies LIN a,b,c
proof
assume that
A1: A is being_line and
A2: a in A and
A3: b in A and
A4: c in A;
reconsider a9=a,b9=b,c9=c as Element of the AffinStruct of X;
reconsider A9=A as Subset of the AffinStruct of X;
A9 is being_line by A1,ANALMETR:43;
then LIN a9,b9,c9 by A2,A3,A4,AFF_1:21;
hence thesis by ANALMETR:40;
end;
theorem Th5:
A is being_line & M is being_line & a in A & b in A & a in M & b
in M implies a=b or A=M
proof
assume that
A1: A is being_line and
A2: M is being_line and
A3: a in A and
A4: b in A and
A5: a in M and
A6: b in M;
reconsider A9=A,M9=M as Subset of the AffinStruct of X;
A7: M9 is being_line by A2,ANALMETR:43;
assume
A8: a<>b;
A9 is being_line by A1,ANALMETR:43;
hence thesis by A3,A4,A5,A6,A8,A7,AFF_1:18;
end;
theorem Th6:
for a,b,c,d,M holds for M9 being Subset of the AffinStruct of X, c9,d9 being
Element of the AffinStruct of X
st c =c9 & d=d9 & M=M9 & a in M & b in M & c9,d9 // M9 holds c,d // a,b
proof
let a,b,c,d,M;
let M9 be Subset of the AffinStruct of X,
c9,d9 be Element of the AffinStruct of X such that
A1: c =c9 and
A2: d=d9 and
A3: M=M9 and
A4: a in M and
A5: b in M and
A6: c9,d9 // M9;
reconsider a9=a,b9=b as Element of the AffinStruct of X;
A7: M9 is being_line by A6,AFF_1:26;
then a9,b9 // M9 by A3,A4,A5,AFF_1:52;
then c9,d9 // a9,b9 by A7,A6,AFF_1:31;
hence thesis by A1,A2,ANALMETR:36;
end;
theorem Th7:
X is satisfying_TDES implies the AffinStruct of X is Moufangian
proof
assume
A1: X is satisfying_TDES;
let K9 be Subset of the AffinStruct of X;
let o9,a9,b9,c9,a19,b19,c19 be Element of the AffinStruct of X;
assume that
A2: K9 is being_line and
A3: o9 in K9 and
A4: c9 in K9 and
A5: c19 in K9 and
A6: not a9 in K9 and
A7: o9<>c9 and
A8: a9<>b9 and
A9: LIN o9,a9,a19 and
A10: LIN o9,b9,b19 and
A11: a9,b9 // a19,b19 and
A12: a9,c9 // a19,c19 and
A13: a9,b9 // K9;
reconsider K=K9 as Subset of X;
reconsider o=o9,a=a9,a1=a19,b=b9,b1=b19,c =c9,c1=c19 as Element
of X;
A14: a,c // a1,c1 by A12,ANALMETR:36;
A15: a,b // a1,b1 by A11,ANALMETR:36;
now
A16: now
assume
A17: o<>a1;
A18: o<>a & o<>b & o<>c & o<>c1 & o<>b1
proof
A19: now
o9,c9 // K9 by A2,A3,A4,AFF_1:23;
then
A20: a9,b9 // o9,c9 by A2,A13,AFF_1:31;
assume o=b1;
then a19,o9 // o9,c9 by A8,A11,A20,DIRAF:40;
then o9,c9 // o9,a19 by AFF_1:4;
then LIN o9,c9,a19 by AFF_1:def 1;
then
A21: a19 in K9 by A2,A3,A4,A7,AFF_1:25;
LIN o9,a19,a9 by A9,AFF_1:6;
hence contradiction by A2,A3,A6,A17,A21,AFF_1:25;
end;
A22: now
o9,a9 // o9,a19 by A9,AFF_1:def 1;
then
A23: o9,a19 // a9, o9 by AFF_1:4;
assume o=c1;
then o9,a19 // a9,c9 by A12,AFF_1:4;
then a9,c9 // a9,o9 by A17,A23,DIRAF:40;
then LIN a9,c9,o9 by AFF_1:def 1;
then LIN o9,c9,a9 by AFF_1:6;
hence contradiction by A2,A3,A4,A6,A7,AFF_1:25;
end;
assume o=a or o=b or o=c or o=c1 or o=b1;
hence contradiction by A3,A6,A7,A13,A22,A19,AFF_1:35;
end;
A24: now
assume
A25: a<>a19;
A26: not LIN a,a1,b & not LIN a,a1,c
proof
A27: now
LIN a9,a19,o9 by A9,AFF_1:6;
then a9,a19 // a9,o9 by AFF_1:def 1;
then
A28: a,a1 // a,o by ANALMETR:36;
assume LIN a,a1,b;
then a,a1 // a,b by ANALMETR:def 10;
then a,b // a,o by A25,A28,ANALMETR:60;
then
A29: a,b // o,a by ANALMETR:59;
a9,b9 // o9,c9 by A2,A3,A4,A7,A13,AFF_1:27;
then a,b // o,c by ANALMETR:36;
then o,c // o,a by A8,A29,ANALMETR:60;
then LIN o,c,a by ANALMETR:def 10;
then LIN o9,c9,a9 by ANALMETR:40;
hence contradiction by A2,A3,A4,A6,A7,AFF_1:25;
end;
A30: now
LIN a9,a19,o9 by A9,AFF_1:6;
then a9,a19 // a9,o9 by AFF_1:def 1;
then
A31: a,a1 // a,o by ANALMETR:36;
assume LIN a,a1,c;
then a,a1 // a,c by ANALMETR:def 10;
then a,c // a,o by A25,A31,ANALMETR:60;
then LIN a,c,o by ANALMETR:def 10;
then LIN a9,c9,o9 by ANALMETR:40;
then LIN c9,o9,a9 by AFF_1:6;
hence contradiction by A2,A3,A4,A6,A7,AFF_1:25;
end;
assume LIN a,a1,b or LIN a,a1,c;
hence contradiction by A27,A30;
end;
A32: LIN o,b,b1 by A10,ANALMETR:40;
o9,c9 // o9,c19 by A2,A3,A4,A5,AFF_1:39,41;
then o,c // o,c1 by ANALMETR:36;
then
A33: LIN o,c,c1 by ANALMETR:def 10;
o9,c9 // K9 by A2,A3,A4,AFF_1:40,41;
then a9,b9 // o9,c9 by A2,A13,AFF_1:31;
then b9,a9 // o9,c9 by AFF_1:4;
then
A34: b,a // o,c by ANALMETR:36;
A35: b,a // b1,a1 by A15,ANALMETR:59;
LIN o,a,a1 by A9,ANALMETR:40;
then b,c // b1,c1 by A1,A14,A17,A18,A26,A32,A33,A35,A34;
hence thesis by ANALMETR:36;
end;
now
A36: not LIN o9,a9,c9
proof
assume LIN o9,a9,c9;
then LIN o9,c9,a9 by AFF_1:6;
hence contradiction by A2,A3,A4,A6,A7,AFF_1:25;
end;
assume
A37: a=a1;
o9,c9 // o9,c19 by A2,A3,A4,A5,AFF_1:39,41;
then LIN o9,c9,c19 by AFF_1:def 1;
then
A38: c9=c19 by A12,A37,A36,AFF_1:14;
not LIN o9,a9,b9
proof
assume LIN o9,a9,b9;
then LIN a9,b9,o9 by AFF_1:6;
then
A39: a9,b9 // a9,o9 by AFF_1:def 1;
o9,c9 // K9 by A2,A3,A4,AFF_1:23;
then a9,b9 // o9,c9 by A2,A13,AFF_1:31;
then a9,o9 // o9,c9 by A8,A39,DIRAF:40;
then o9,c9 // o9,a9 by AFF_1:4;
then LIN o9,c9,a9 by AFF_1:def 1;
hence contradiction by A2,A3,A4,A6,A7,AFF_1:25;
end;
then b9=b19 by A10,A11,A37,AFF_1:14;
hence thesis by A38,AFF_1:2;
end;
hence thesis by A24;
end;
assume
A40: not b in K;
A41: o=a1 implies o=b1 & o=c1
proof
assume that
A42: o=a1 and
A43: o<>b1 or o<>c1;
A44: now
A45: o9,c19 // a9,c9 by A12,A42,AFF_1:4;
assume
A46: o<>c1;
o9,c19 // o9,c9 by A2,A3,A4,A5,AFF_1:39,41;
then a9,c9 // o9,c9 by A46,A45,DIRAF:40;
then c9,a9 // c9,o9 by AFF_1:4;
then LIN c9,a9,o9 by AFF_1:def 1;
then LIN o9,c9,a9 by AFF_1:6;
hence contradiction by A2,A3,A4,A6,A7,AFF_1:25;
end;
now
o9,c9 // K9 by A2,A3,A4,AFF_1:23;
then a9,b9 // o9,c9 by A2,A13,AFF_1:31;
then o9,c9 // o9,b19 by A8,A11,A42,DIRAF:40;
then LIN o9,c9,b19 by AFF_1:def 1;
then
A47: b19 in K9 by A2,A3,A4,A7,AFF_1:25;
assume
A48: o<>b1;
LIN o9,b19,b9 by A10,AFF_1:6;
hence contradiction by A2,A3,A40,A48,A47,AFF_1:25;
end;
hence contradiction by A43,A44;
end;
now
assume o=a1;
then b,c // b1,c1 by A41,ANALMETR:39;
hence thesis by ANALMETR:36;
end;
hence thesis by A16;
end;
hence thesis by A6,A13,AFF_1:35;
end;
theorem Th8:
the AffinStruct of X is translational implies X is satisfying_des
proof
assume
A1: the AffinStruct of X is translational;
let a,a1,b,b1,c,c1;
assume that
A2: not LIN a,a1,b and
A3: not LIN a,a1,c and
A4: a,a1 // b,b1 and
A5: a,a1 // c,c1 and
A6: a,b // a1,b1 and
A7: a,c // a1,c1;
reconsider a9=a,a19=a1,b9=b,b19=b1,c9=c,c19=c1
as Element of the AffinStruct of X;
LIN a9,a19,a19 by AFF_1:7;
then consider A9 be Subset of the AffinStruct of X such that
A8: A9 is being_line and
A9: a9 in A9 and
A10: a19 in A9 and
a19 in A9 by AFF_1:21;
A11: a9,b9 // a19,b19 by A6,ANALMETR:36;
b,b1 // a,a1 by A4,ANALMETR:59;
then
A12: b9,b19 // a9,a19 by ANALMETR:36;
A13: a9<>a19
proof
assume a9=a19;
then LIN a9,a19,b9 by AFF_1:7;
hence contradiction by A2,ANALMETR:40;
end;
then for x9 holds x9 in A9 iff LIN a9,a19,x9 by A8,A9,A10,AFF_1:21,25;
then A9=Line(a9,a19) by AFF_1:def 2;
then
A14: b9,b19 // A9 by A13,A12,AFF_1:def 4;
A15: a9,c9 // a19,c19 by A7,ANALMETR:36;
c,c1 // a,a1 by A5,ANALMETR:59;
then
A16: c9,c19 // a9,a19 by ANALMETR:36;
A17: a9<>a19
proof
assume a9=a19;
then LIN a9,a19,b9 by AFF_1:7;
hence contradiction by A2,ANALMETR:40;
end;
then for x9 holds x9 in A9 iff LIN a9,a19,x9 by A8,A9,A10,AFF_1:21,25;
then A9=Line(a9,a19) by AFF_1:def 2;
then
A18: c9,c19 // A9 by A17,A16,AFF_1:def 4;
LIN c9,c19,c19 by AFF_1:7;
then consider N9 be Subset of the AffinStruct of X such that
A19: N9 is being_line and
A20: c9 in N9 and
A21: c19 in N9 and
c19 in N9 by AFF_1:21;
LIN b9,b19,b19 by AFF_1:7;
then consider M9 be Subset of the AffinStruct of X such that
A22: M9 is being_line and
A23: b9 in M9 and
A24: b19 in M9 and
b19 in M9 by AFF_1:21;
A25: A9<>M9 & A9<>N9
proof
assume A9=M9 or A9=N9;
then LIN a9,a19,b9 or LIN a9,a19,c9 by A8,A9,A10,A23,A20,AFF_1:21;
hence contradiction by A2,A3,ANALMETR:40;
end;
A26: c9<>c19
proof
assume c9=c19;
then c,a // c,a1 by A7,ANALMETR:59;
then LIN c,a,a1 by ANALMETR:def 10;
then LIN c9,a9,a19 by ANALMETR:40;
then LIN a9,a19,c9 by AFF_1:6;
hence contradiction by A3,ANALMETR:40;
end;
then for x9 holds x9 in N9 iff LIN c9,c19,x9 by A19,A20,A21,AFF_1:21,25;
then N9=Line(c9,c19) by AFF_1:def 2;
then
A27: A9 // N9 by A18,A26,AFF_1:def 5;
A28: b9<>b19
proof
assume b9=b19;
then b,a // b,a1 by A6,ANALMETR:59;
then LIN b,a,a1 by ANALMETR:def 10;
then LIN b9,a9,a19 by ANALMETR:40;
then LIN a9,a19,b9 by AFF_1:6;
hence contradiction by A2,ANALMETR:40;
end;
then for x9 holds x9 in M9 iff LIN b9,b19,x9 by A22,A23,A24,AFF_1:21,25;
then M9=Line(b9,b19) by AFF_1:def 2;
then A9 // M9 by A14,A28,AFF_1:def 5;
then b9,c9 // b19,c19 by A1,A8,A9,A10,A22,A23,A24,A19,A20,A21,A27,A25,A11,A15
;
hence thesis by ANALMETR:36;
end;
theorem
X is satisfying_MH1 implies X is satisfying_OSCH
proof
assume
A1: X is satisfying_MH1;
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
not b3 in N and
A18: a3,a2 // b3,b2 and
A19: a2,a1 // b2,b1 and
A20: a1,a4 // b1,b4;
reconsider M9=M,N9=N as Subset of the AffinStruct of X;
N is being_line by A2,ANALMETR:44;
then
A21: N9 is being_line by ANALMETR:43;
reconsider b49=b4,b19=b1,b29=b2,b39=b3,a19=a1,a29=a2,a39=a3,a49=a4 as
Element of the AffinStruct of X;
M is being_line by A2,ANALMETR:44;
then
A22: M9 is being_line by ANALMETR:43;
not M9 // N9
proof
assume M9 // N9;
then M // N by ANALMETR:46;
hence contradiction by A2,ANALMETR:52;
end;
then ex o9 be Element of the AffinStruct of X st o9 in M9 & o9 in N9
by A22,A21,AFF_1:58;
then consider o such that
A23: o in M and
A24: o in N;
reconsider o9=o as Element of the AffinStruct of X;
A25: now
assume
A26: b2<>b4;
A27: now
consider e19 be Element of the AffinStruct of X such that
A28: o9<>e19 and
A29: e19 in M9 by A22,AFF_1:20;
reconsider e1=e19 as Element of X;
ex d49 be Element of the AffinStruct of X st o9<>d49 & d49 in N9
by A21,AFF_1:20;
then consider d4 such that
A30: d4 in N and
A31: d4 <> o;
reconsider d49=d4 as Element of the AffinStruct of X;
consider e2 such that
A32: a1,a4 _|_ d4,e2 and
A33: e2<>d4 by ANALMETR:39;
reconsider e29=e2 as Element of the AffinStruct of X;
assume
A34: b1<>b3;
not o9,e19 // d49,e29
proof
A35: a49<>a29
proof
assume a49=a29;
then a2,a1 // b1,b4 by A20,ANALMETR:59;
then b1,b4 // b2,b1 by A3,A12,A19,ANALMETR:60;
then b1,b4 // b1,b2 by ANALMETR:59;
then LIN b1,b4,b2 by ANALMETR:def 10;
then LIN b19,b49,b29 by ANALMETR:40;
then LIN b29,b49,b19 by AFF_1:6;
hence contradiction by A9,A10,A17,A21,A26,AFF_1:25;
end;
A36: a1<>a3
proof
assume a1=a3;
then a3,a2 // b2,b1 by A19,ANALMETR:59;
then b3,b2 // b2,b1 by A4,A12,A18,ANALMETR:60;
then b2,b3 // b2,b1 by ANALMETR:59;
then LIN b2,b3,b1 by ANALMETR:def 10;
then LIN b29,b39,b19 by ANALMETR:40;
then LIN b19,b39,b29 by AFF_1:6;
hence contradiction by A5,A6,A13,A22,A34,AFF_1:25;
end;
assume o9,e19 // d49,e29;
then o,e1 // d4,e2 by ANALMETR:36;
then
A37: o,e1 _|_ a1,a4 by A32,A33,ANALMETR:62;
o9,e19 // a19,a39 by A3,A4,A22,A23,A29,AFF_1:39,41;
then o,e1 // a1,a3 by ANALMETR:36;
then
A38: a1,a3 _|_ a1,a4 by A28,A37,ANALMETR:62;
a1,a3 _|_ a2,a4 by A2,A3,A4,A7,A8,ANALMETR:56;
then a1,a4 // a2,a4 by A38,A36,ANALMETR:63;
then a4,a2 // a4,a1 by ANALMETR:59;
then LIN a4,a2,a1 by ANALMETR:def 10;
then LIN a49,a29,a19 by ANALMETR:40;
hence contradiction by A7,A8,A15,A21,A35,AFF_1:25;
end;
then consider d19 be Element of the AffinStruct of X such that
A39: LIN o9,e19,d19 and
A40: LIN d49,e29,d19 by AFF_1:60;
reconsider d1=d19 as Element of X;
consider e19 be Element of the AffinStruct of X such that
A41: o9<>e19 and
A42: e19 in N9 by A21,AFF_1:20;
A43: d1 in M by A22,A23,A28,A29,A39,AFF_1:25;
LIN d4,e2,d1 by A40,ANALMETR:40;
then d4,e2 // d4,d1 by ANALMETR:def 10;
then
A44: d1,d4 // d4,e2 by ANALMETR:59;
then a1,a4 _|_ d1,d4 by A32,A33,ANALMETR:62;
then
A45: b1,b4 _|_ d1,d4 by A3,A11,A20,ANALMETR:62;
reconsider e1=e19 as Element of X;
consider e2 such that
A46: a2,a1 _|_ d1,e2 and
A47: e2<>d1 by ANALMETR:39;
reconsider e29=e2 as Element of the AffinStruct of X;
not o9,e19 // e29,d19
proof
A48: a19<>a39
proof
assume a19=a39;
then a3,a2 // b2,b1 by A19,ANALMETR:59;
then b3,b2 // b2,b1 by A4,A12,A18,ANALMETR:60;
then b2,b3 // b2,b1 by ANALMETR:59;
then LIN b2,b3,b1 by ANALMETR:def 10;
then LIN b29,b39,b19 by ANALMETR:40;
then LIN b19,b39,b29 by AFF_1:6;
hence contradiction by A5,A6,A13,A22,A34,AFF_1:25;
end;
o9,e19 // a29,a49 by A7,A8,A21,A24,A42,AFF_1:39,41;
then
A49: o,e1 // a2,a4 by ANALMETR:36;
A50: a2<>a4
proof
assume a2=a4;
then a2,a1 // b1,b4 by A20,ANALMETR:59;
then b1,b4 // b2,b1 by A3,A12,A19,ANALMETR:60;
then b1,b4 // b1,b2 by ANALMETR:59;
then LIN b1,b4,b2 by ANALMETR:def 10;
then LIN b19,b49,b29 by ANALMETR:40;
then LIN b29,b49,b19 by AFF_1:6;
hence contradiction by A9,A10,A17,A21,A26,AFF_1:25;
end;
assume o9,e19 // e29,d19;
then
A51: o,e1 // e2,d1 by ANALMETR:36;
a2,a1 _|_ e2,d1 by A46,ANALMETR:61;
then o,e1 _|_ a2,a1 by A47,A51,ANALMETR:62;
then
A52: a2,a1 _|_ a2,a4 by A41,A49,ANALMETR:62;
a3,a1 _|_ a2,a4 by A2,A3,A4,A7,A8,ANALMETR:56;
then a3,a1 // a2,a1 by A52,A50,ANALMETR:63;
then a1,a3 // a1,a2 by ANALMETR:59;
then LIN a1,a3,a2 by ANALMETR:def 10;
then LIN a19,a39,a29 by ANALMETR:40;
hence contradiction by A3,A4,A12,A22,A48,AFF_1:25;
end;
then consider d29 be Element of the AffinStruct of X such that
A53: LIN o9,e19,d29 and
A54: LIN e29,d19,d29 by AFF_1:60;
reconsider d2=d29 as Element of X;
A55: d2 in N by A21,A24,A41,A42,A53,AFF_1:25;
LIN d19,d29,e29 by A54,AFF_1:6;
then LIN d1,d2,e2 by ANALMETR:40;
then d1,d2 // d1,e2 by ANALMETR:def 10;
then
A56: d2,d1 // e2,d1 by ANALMETR:59;
A57: a2,a1 _|_ e2,d1 by A46,ANALMETR:61;
then
A58: a2,a1 _|_ d2,d1 by A47,A56,ANALMETR:62;
consider e19 be Element of the AffinStruct of X such that
A59: o9<>e19 and
A60: e19 in M9 by A22,AFF_1:20;
reconsider e1=e19 as Element of X;
consider e2 such that
A61: a3,a2 _|_ d2,e2 and
A62: e2<>d2 by ANALMETR:39;
reconsider e29=e2 as Element of the AffinStruct of X;
not o9,e19 // e29,d29
proof
A63: a29<>a49
proof
assume a29=a49;
then a2,a1 // b1,b4 by A20,ANALMETR:59;
then b1,b4 // b2,b1 by A3,A12,A19,ANALMETR:60;
then b1,b4 // b1,b2 by ANALMETR:59;
then LIN b1,b4,b2 by ANALMETR:def 10;
then LIN b19,b49,b29 by ANALMETR:40;
then LIN b29,b49,b19 by AFF_1:6;
hence contradiction by A9,A10,A17,A21,A26,AFF_1:25;
end;
assume o9,e19 // e29,d29;
then o,e1 // e2,d2 by ANALMETR:36;
then o,e1 // d2,e2 by ANALMETR:59;
then
A64: a3,a2 _|_ o,e1 by A61,A62,ANALMETR:62;
o,e1 _|_ a2,a4 by A2,A7,A8,A23,A60,ANALMETR:56;
then a3,a2 // a2,a4 by A59,A64,ANALMETR:63;
then a2,a4 // a2,a3 by ANALMETR:59;
then LIN a2,a4,a3 by ANALMETR:def 10;
then LIN a29,a49,a39 by ANALMETR:40;
hence contradiction by A7,A8,A16,A21,A63,AFF_1:25;
end;
then consider d39 be Element of the AffinStruct of X such that
A65: LIN o9,e19,d39 and
A66: LIN e29,d29,d39 by AFF_1:60;
reconsider d3=d39 as Element of X;
A67: d3 in M by A22,A23,A59,A60,A65,AFF_1:25;
then
A68: d3<>d4 by A2,A22,A21,A23,A24,A30,A31,AFF_1:18;
a2,a1 _|_ d2,d1 by A47,A56,A57,ANALMETR:62;
then
A69: b2,b1 _|_ d2,d1 by A3,A12,A19,ANALMETR:62;
LIN d29,d39,e29 by A66,AFF_1:6;
then LIN d2,d3,e2 by ANALMETR:40;
then d2,d3 // d2,e2 by ANALMETR:def 10;
then d3,d2 // d2,e2 by ANALMETR:59;
then
A70: a3,a2 _|_ d3,d2 by A61,A62,ANALMETR:62;
then b3,b2 _|_ d3,d2 by A4,A12,A18,ANALMETR:62;
then
A71: b3,b4 _|_ d3,d4 by A1,A2,A5,A6,A9,A10,A13,A14,A30,A43,A55,A67,A45,A69;
a1,a4 _|_ d1,d4 by A32,A33,A44,ANALMETR:62;
then a3,a4 _|_ d3,d4 by A1,A2,A3,A4,A7,A8,A11,A12,A30,A43,A55,A58,A70,A67
;
hence thesis by A68,A71,ANALMETR:63;
end;
now
A72: not LIN o9,a29,a19 by A7,A12,A15,A21,A23,A24,AFF_1:48,def 1;
A73: LIN o9,a19,a39 by A3,A4,A22,A23,AFF_1:21;
assume
A74: b1=b3;
then a2,a3 // b2,b1 by A18,ANALMETR:59;
then
A75: a29,a39 // b29,b19 by ANALMETR:36;
a29,a19 // b29,b19 by A19,ANALMETR:36;
then a29,a19 // a29,a39 by A5,A13,A75,AFF_1:5;
hence thesis by A20,A74,A72,A73,AFF_1:14;
end;
hence thesis by A27;
end;
now
A76: not LIN o9,a19,a49
proof
assume LIN o9,a19,a49;
then
ex A9 st A9 is being_line & o9 in A9 & a19 in A9 & a49 in A9 by AFF_1:21;
hence contradiction by A3,A11,A15,A22,A23,A24,AFF_1:18;
end;
assume
A77: b2=b4;
b1,b2 // a1,a2 by A19,ANALMETR:59;
then a1,a4 // a1,a2 by A5,A13,A20,A77,ANALMETR:60;
then
A78: a19,a49 // a19,a29 by ANALMETR:36;
LIN o9,a49,a29 by A7,A8,A21,A24,AFF_1:21;
hence thesis by A18,A77,A78,A76,AFF_1:14;
end;
hence thesis by A25;
end;
theorem
X is satisfying_MH2 implies X is satisfying_OSCH
proof
assume
A1: X is satisfying_MH2;
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
not b3 in N and
A18: a3,a2 // b3,b2 and
A19: a2,a1 // b2,b1 and
A20: a1,a4 // b1,b4;
reconsider M9=M,N9=N as Subset of the AffinStruct of X;
N is being_line by A2,ANALMETR:44;
then
A21: N9 is being_line by ANALMETR:43;
reconsider b49=b4,b19=b1,b29=b2,b39=b3,a19=a1,a29=a2,a39=a3,a49=a4 as
Element of the AffinStruct of X;
M is being_line by A2,ANALMETR:44;
then
A22: M9 is being_line by ANALMETR:43;
not M9 // N9
proof
assume M9 // N9;
then M // N by ANALMETR:46;
hence contradiction by A2,ANALMETR:52;
end;
then ex o9 be Element of the AffinStruct of X st o9 in M9 & o9 in N9
by A22,A21,AFF_1:58;
then consider o such that
A23: o in M and
A24: o in N;
reconsider o9=o as Element of the AffinStruct of X;
A25: now
assume
A26: b2<>b4;
A27: now
ex d39 be Element of the AffinStruct of X st o9<>d39 & d39 in N9
by A21,AFF_1:20;
then consider d3 such that
A28: d3 in N and
A29: d3 <>o;
reconsider d39=d3 as Element of the AffinStruct of X;
consider e2 such that
A30: a3,a2 _|_ d3,e2 and
A31: d3<>e2 by ANALMETR:def 9;
consider e1 such that
A32: a3,a1 // a3,e1 and
A33: a3<>e1 by ANALMETR:39;
reconsider e19=e1,e29=e2 as Element of the AffinStruct of X;
assume
A34: b1<>b3;
A35: a1<>a3 & a2<>a4
proof
assume a1=a3 or a2=a4;
then a2,a1 // b3,b2 or a1,a4 // b2,b1 by A18,A19,ANALMETR:59;
then b3,b2 // b2,b1 or b2,b1 // b1,b4 by A3,A11,A12,A19,A20,ANALMETR:60
;
then b2,b3 // b2,b1 or b1,b2 // b1,b4 by ANALMETR:59;
then LIN b2,b3,b1 or LIN b1,b2,b4 by ANALMETR:def 10;
then LIN b29,b39,b19 or LIN b19,b29,b49 by ANALMETR:40;
then LIN b19,b39,b29 or LIN b29,b49,b19 by AFF_1:6;
hence contradiction by A5,A6,A9,A10,A13,A17,A22,A21,A26,A34,AFF_1:25;
end;
not a39,e19 // d39,e29
proof
assume a39,e19 // d39,e29;
then a3,e1 // d3,e2 by ANALMETR:36;
then a3,a1 // d3,e2 by A32,A33,ANALMETR:60;
then
A36: a3,a2 _|_ a3,a1 by A30,A31,ANALMETR:62;
a3,a1 _|_ a2,a4 by A2,A3,A4,A7,A8,ANALMETR:56;
then a3,a2 // a2,a4 by A35,A36,ANALMETR:63;
then a2,a4 // a2,a3 by ANALMETR:59;
then LIN a2,a4,a3 by ANALMETR:def 10;
then LIN a29,a49,a39 by ANALMETR:40;
hence contradiction by A7,A8,A16,A21,A35,AFF_1:25;
end;
then consider d29 be Element of the AffinStruct of X such that
A37: LIN a39,e19,d29 and
A38: LIN d39,e29,d29 by AFF_1:60;
reconsider d2=d29 as Element of X;
LIN d3,e2,d2 by A38,ANALMETR:40;
then d3,e2 // d3,d2 by ANALMETR:def 10;
then
A39: a3,a2 _|_ d3,d2 by A30,A31,ANALMETR:62;
LIN a3,e1,d2 by A37,ANALMETR:40;
then a3,e1 // a3,d2 by ANALMETR:def 10;
then a3,a1 // a3,d2 by A32,A33,ANALMETR:60;
then LIN a3,a1,d2 by ANALMETR:def 10;
then LIN a39,a19,d29 by ANALMETR:40;
then consider d2 such that
A40: d2 in M and
A41: a3,a2 _|_ d3,d2 by A3,A4,A22,A35,A39,AFF_1:25;
reconsider d29=d2 as Element of the AffinStruct of X;
consider e1 such that
A42: a2,a4 // a2,e1 and
A43: a2<>e1 by ANALMETR:39;
consider e2 such that
A44: a2,a1 _|_ d2,e2 and
A45: d2<>e2 by ANALMETR:def 9;
reconsider e19=e1,e29=e2 as Element of the AffinStruct of X;
not a29,e19 // d29,e29
proof
assume a29,e19 // d29,e29;
then a2,e1 // d2,e2 by ANALMETR:36;
then a2,a4 // d2,e2 by A42,A43,ANALMETR:60;
then
A46: a2,a4 _|_ a2,a1 by A44,A45,ANALMETR:62;
a1,a3 _|_ a2,a4 by A2,A3,A4,A7,A8,ANALMETR:56;
then a1,a3 // a2,a1 by A35,A46,ANALMETR:63;
then a1,a3 // a1,a2 by ANALMETR:59;
then LIN a1,a3,a2 by ANALMETR:def 10;
then LIN a19,a39,a29 by ANALMETR:40;
hence contradiction by A3,A4,A12,A22,A35,AFF_1:25;
end;
then consider d19 be Element of the AffinStruct of X such that
A47: LIN a29,e19,d19 and
A48: LIN d29,e29,d19 by AFF_1:60;
reconsider d1=d19 as Element of X;
A49: b3,b2 _|_ d3,d2 by A4,A12,A18,A41,ANALMETR:62;
LIN a2,e1,d1 by A47,ANALMETR:40;
then a2,e1 // a2,d1 by ANALMETR:def 10;
then a2,a4 // a2,d1 by A42,A43,ANALMETR:60;
then LIN a2,a4,d1 by ANALMETR:def 10;
then LIN a29,a49,d19 by ANALMETR:40;
then
A50: d1 in N by A7,A8,A21,A35,AFF_1:25;
LIN d2,e2,d1 by A48,ANALMETR:40;
then d2,e2 // d2,d1 by ANALMETR:def 10;
then
A51: a2,a1 _|_ d2,d1 by A44,A45,ANALMETR:62;
then
A52: b2,b1 _|_ d2,d1 by A3,A12,A19,ANALMETR:62;
consider e2 such that
A53: a1,a4 _|_ d1,e2 and
A54: d1<>e2 by ANALMETR:39;
consider e1 such that
A55: a1,a3 // a1,e1 and
A56: a1<>e1 by ANALMETR:39;
reconsider e19=e1,e29=e2 as Element of the AffinStruct of X;
not a19,e19 // d19,e29
proof
assume a19,e19 // d19,e29;
then a1,e1 // d1,e2 by ANALMETR:36;
then a1,a3 // d1,e2 by A55,A56,ANALMETR:60;
then
A57: a1,a3 _|_ a1,a4 by A53,A54,ANALMETR:62;
a1,a3 _|_ a2,a4 by A2,A3,A4,A7,A8,ANALMETR:56;
then a2,a4 // a1,a4 by A35,A57,ANALMETR:63;
then a4,a2 // a4,a1 by ANALMETR:59;
then LIN a4,a2,a1 by ANALMETR:def 10;
then LIN a49,a29,a19 by ANALMETR:40;
hence contradiction by A7,A8,A15,A21,A35,AFF_1:25;
end;
then consider d49 be Element of the AffinStruct of X such that
A58: LIN a19,e19,d49 and
A59: LIN d19,e29,d49 by AFF_1:60;
reconsider d4=d49 as Element of X;
LIN a1,e1,d4 by A58,ANALMETR:40;
then a1,e1 // a1,d4 by ANALMETR:def 10;
then a1,a3 // a1,d4 by A55,A56,ANALMETR:60;
then LIN a1,a3,d4 by ANALMETR:def 10;
then LIN a19,a39,d49 by ANALMETR:40;
then
A60: d4 in M by A3,A4,A22,A35,AFF_1:25;
then
A61: d3<>d4 by A2,A22,A21,A23,A24,A28,A29,AFF_1:18;
LIN d1,e2,d4 by A59,ANALMETR:40;
then d1,e2 // d1,d4 by ANALMETR:def 10;
then
A62: a1,a4 _|_ d1,d4 by A53,A54,ANALMETR:62;
then b1,b4 _|_ d1,d4 by A3,A11,A20,ANALMETR:62;
then
A63: b3,b4 _|_ d3,d4 by A1,A2,A5,A6,A9,A10,A13,A14,A28,A40,A50,A60,A49,A52;
a3,a4 _|_ d3,d4 by A1,A2,A3,A4,A7,A8,A11,A12,A28,A40,A41,A50,A51,A60,A62;
hence thesis by A63,A61,ANALMETR:63;
end;
now
o9,a19 // o9,a39 by A3,A4,A22,A23,AFF_1:39,41;
then
A64: LIN o9,a19,a39 by AFF_1:def 1;
assume
A65: b1=b3;
then a2,a1 // b3,b2 by A19,ANALMETR:59;
then a2,a1 // a3,a2 by A6,A13,A18,ANALMETR:60;
then a2,a1 // a2,a3 by ANALMETR:59;
then a29,a19 // a29,a39 by ANALMETR:36;
hence thesis by A7,A12,A15,A20,A21,A23,A24,A65,A64,AFF_1:14,25;
end;
hence thesis by A27;
end;
now
o9,a29 // o9,a49 by A7,A8,A21,A24,AFF_1:39,41;
then
A66: LIN o9,a29,a49 by AFF_1:def 1;
assume
A67: b2=b4;
then a1,a4 // b2,b1 by A20,ANALMETR:59;
then a2,a1 // a1,a4 by A5,A13,A19,ANALMETR:60;
then a1,a2 // a1,a4 by ANALMETR:59;
then a19,a29 // a19,a49 by ANALMETR:36;
hence thesis by A3,A12,A15,A18,A22,A23,A24,A67,A66,AFF_1:14,25;
end;
hence thesis by A25;
end;
theorem
X is satisfying_AH implies X is satisfying_TDES
proof
assume
A1: X is satisfying_AH;
let o,a,a1,b,b1,c,c1;
assume that
A2: o<>a and
A3: o<>a1 and
A4: o<>b and
A5: o<>b1 and
A6: o<>c and
A7: o<>c1 and
A8: not LIN b,b1,a and
A9: not LIN b,b1,c and
A10: LIN o,a,a1 and
A11: LIN o,b,b1 and
A12: LIN o,c,c1 and
A13: a,b // a1,b1 and
A14: a,b // o,c and
A15: b,c // b1,c1;
consider e1 such that
A16: o,b _|_ o,e1 and
A17: o<>e1 by ANALMETR:def 9;
consider c2 such that
A18: o,c _|_ o,c2 and
A19: o<>c2 by ANALMETR:def 9;
consider e2 such that
A20: b,c _|_ c2,e2 and
A21: c2<>e2 by ANALMETR:def 9;
reconsider o9=o,a9=a,a19=a1,b9=b,b19=b1,c9 = c,c19= c1,c29= c2,e19=e1, e29=
e2 as Element of the AffinStruct of X;
A22: b1<>a1
proof
assume b1=a1;
then LIN o9,b9,a19 by A11,ANALMETR:40;
then o9,b9 // o9,a19 by AFF_1:def 1;
then o9,a19 // o9,b9 by AFF_1:4;
then
A23: o,a1 // o,b by ANALMETR:36;
o,a // o,a1 by A10,ANALMETR:def 10;
then o9,a9 // o9,a19 by ANALMETR:36;
then o9,a19 // o9,a9 by AFF_1:4;
then o,a1 // o,a by ANALMETR:36;
then o,a // o,b by A3,A23,ANALMETR:60;
then LIN o,a,b by ANALMETR:def 10;
then
A24: LIN o9,a9,b9 by ANALMETR:40;
then LIN b9,o9,a9 by AFF_1:6;
then b9,o9 // b9,a9 by AFF_1:def 1;
then o9,b9 // a9,b9 by AFF_1:4;
then
A25: o,b // a,b by ANALMETR:36;
A26: a9<>b9
proof
assume a9=b9;
then LIN b9,b19,a9 by AFF_1:7;
hence contradiction by A8,ANALMETR:40;
end;
o,b // o,b1 by A11,ANALMETR:def 10;
then a,b // o,b1 by A4,A25,ANALMETR:60;
then
A27: a9,b9 // o9,b19 by ANALMETR:36;
LIN a9,b9,o9 by A24,AFF_1:6;
then LIN a9,b9,b19 by A27,A26,AFF_1:9;
then LIN b9,b19,a9 by AFF_1:6;
hence contradiction by A8,ANALMETR:40;
end;
A28: now
not o9,e19 // c29,e29
proof
assume o9,e19 // c29,e29;
then o,e1 // c2,e2 by ANALMETR:36;
then c2,e2 _|_ o,b by A16,A17,ANALMETR:62;
then c2,e2 _|_ b,o by ANALMETR:61;
then b,c // b,o by A20,A21,ANALMETR:63;
then LIN b,c,o by ANALMETR:def 10;
then LIN b9,c9,o9 by ANALMETR:40;
then LIN b9,o9,c9 by AFF_1:6;
then LIN b,o,c by ANALMETR:40;
then
A29: b,o // b,c by ANALMETR:def 10;
LIN o9,b9,b19 by A11,ANALMETR:40;
then LIN b9,o9,b19 by AFF_1:6;
then LIN b,o,b1 by ANALMETR:40;
then b,o // b,b1 by ANALMETR:def 10;
then b,b1 // b,c by A4,A29,ANALMETR:60;
hence contradiction by A9,ANALMETR:def 10;
end;
then consider b29 such that
A30: LIN o9,e19,b29 and
A31: LIN c29,e29,b29 by AFF_1:60;
reconsider b2=b29 as Element of X;
LIN o,e1,b2 by A30,ANALMETR:40;
then o,e1 // o,b2 by ANALMETR:def 10;
then
A32: o,b _|_ o,b2 by A16,A17,ANALMETR:62;
o,b // o,b1 by A11,ANALMETR:def 10;
then
A33: o,b1 _|_ o,b2 by A4,A32,ANALMETR:62;
assume
A34: not LIN a,b,c;
A35: b<>a
proof
assume b=a;
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A34,ANALMETR:40;
end;
A36: not o,c // o,b
proof
assume o,c // o,b;
then LIN o,c,b by ANALMETR:def 10;
then LIN o9,c9,b9 by ANALMETR:40;
then LIN c9,o9,b9 by AFF_1:6;
then c9,o9 // c9,b9 by AFF_1:def 1;
then o9,c9 // b9,c9 by AFF_1:4;
then
A37: o,c // b,c by ANALMETR:36;
a9,b9 // o9,c9 by A14,ANALMETR:36;
then o9,c9 // b9,a9 by AFF_1:4;
then o,c // b,a by ANALMETR:36;
then b,a // b,c by A6,A37,ANALMETR:60;
then LIN b,a,c by ANALMETR:def 10;
then LIN b9,a9,c9 by ANALMETR:40;
then LIN a9,b9,c9 by AFF_1:6;
hence contradiction by A34,ANALMETR:40;
end;
A38: not o,a // o,c
proof
assume o,a // o,c;
then LIN o,a,c by ANALMETR:def 10;
then LIN o9,a9,c9 by ANALMETR:40;
then LIN c9,o9,a9 by AFF_1:6;
then LIN c,o,a by ANALMETR:40;
then
A39: c,o // c,a by ANALMETR:def 10;
a9,b9 // o9,c9 by A14,ANALMETR:36;
then c9,o9 // a9,b9 by AFF_1:4;
then c,o // a,b by ANALMETR:36;
then a,b // c,a by A6,A39,ANALMETR:60;
then a9,b9 // c9,a9 by ANALMETR:36;
then a9,b9 // a9,c9 by AFF_1:4;
then a,b // a,c by ANALMETR:36;
hence contradiction by A34,ANALMETR:def 10;
end;
LIN c2,e2,b2 by A31,ANALMETR:40;
then c2,e2 // c2,b2 by ANALMETR:def 10;
then
A40: b,c _|_ c2,b2 by A20,A21,ANALMETR:62;
consider e1 such that
A41: o,a _|_ o,e1 and
A42: o<>e1 by ANALMETR:def 9;
consider e2 such that
A43: a,c _|_ c2,e2 and
A44: c2<>e2 by ANALMETR:def 9;
reconsider e19=e1,e29=e2 as Element of the AffinStruct of X;
not o9,e19 // c29,e29
proof
assume o9,e19 // c29,e29;
then o,e1 // c2,e2 by ANALMETR:36;
then c2,e2 _|_ o,a by A41,A42,ANALMETR:62;
then a,c // o,a by A43,A44,ANALMETR:63;
then a9,c9 // o9,a9 by ANALMETR:36;
then a9,c9 // a9,o9 by AFF_1:4;
then LIN a9,c9,o9 by AFF_1:def 1;
then LIN c9,o9,a9 by AFF_1:6;
then LIN c,o,a by ANALMETR:40;
then
A45: c,o // c,a by ANALMETR:def 10;
a9,b9 // o9,c9 by A14,ANALMETR:36;
then c9,o9 // a9,b9 by AFF_1:4;
then c,o // a,b by ANALMETR:36;
then a,b // c,a by A6,A45,ANALMETR:60;
then a9,b9 // c9,a9 by ANALMETR:36;
then a9,b9 // a9,c9 by AFF_1:4;
then a,b // a,c by ANALMETR:36;
hence contradiction by A34,ANALMETR:def 10;
end;
then consider a29 such that
A46: LIN o9,e19,a29 and
A47: LIN c29,e29,a29 by AFF_1:60;
reconsider a2=a29 as Element of X;
LIN o,e1,a2 by A46,ANALMETR:40;
then o,e1 // o,a2 by ANALMETR:def 10;
then
A48: o,a _|_ o,a2 by A41,A42,ANALMETR:62;
A49: c2<>a2
proof
assume c2=a2;
then o,c // o,a by A18,A19,A48,ANALMETR:63;
then LIN o,c,a by ANALMETR:def 10;
then LIN o9,c9,a9 by ANALMETR:40;
then LIN c9,a9,o9 by AFF_1:6;
then c9,a9 // c9,o9 by AFF_1:def 1;
then o9,c9 // a9,c9 by AFF_1:4;
then o,c // a,c by ANALMETR:36;
then a,b // a,c by A6,A14,ANALMETR:60;
hence contradiction by A34,ANALMETR:def 10;
end;
LIN c2,e2,a2 by A47,ANALMETR:40;
then c2,e2 // c2,a2 by ANALMETR:def 10;
then a,c _|_ c2,a2 by A43,A44,ANALMETR:62;
then
A50: c,a _|_ c2,a2 by ANALMETR:61;
A51: not LIN o9,b29,a29
proof
A52: o<>b2
proof
a9,b9 // o9,c9 by A14,ANALMETR:36;
then o9,c9 // b9,a9 by AFF_1:4;
then
A53: o,c // b,a by ANALMETR:36;
assume o=b2;
then o,c2 _|_ b,c by A40,ANALMETR:61;
then o,c // b,c by A18,A19,ANALMETR:63;
then b,a // b,c by A6,A53,ANALMETR:60;
then LIN b,a,c by ANALMETR:def 10;
then LIN b9,a9,c9 by ANALMETR:40;
then LIN a9,b9,c9 by AFF_1:6;
hence contradiction by A34,ANALMETR:40;
end;
A54: o<>a2
proof
assume
A55: o=a2;
c2,o _|_ o,c by A18,ANALMETR:61;
then o,c // c,a by A19,A50,A55,ANALMETR:63;
then a,b // c,a by A6,A14,ANALMETR:60;
then a9,b9 // c9,a9 by ANALMETR:36;
then a9,b9 // a9,c9 by AFF_1:4;
then a,b // a,c by ANALMETR:36;
hence contradiction by A34,ANALMETR:def 10;
end;
assume LIN o9,b29,a29;
then LIN o,b2,a2 by ANALMETR:40;
then o,b2 // o,a2 by ANALMETR:def 10;
then o,a2 _|_ o,b by A32,A52,ANALMETR:62;
then o,a // o,b by A48,A54,ANALMETR:63;
then LIN o,a,b by ANALMETR:def 10;
then LIN o9,a9,b9 by ANALMETR:40;
then
A56: LIN a9,b9,o9 by AFF_1:6;
A57: a9<>b9
proof
assume a9=b9;
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A34,ANALMETR:40;
end;
a9,b9 // o9,c9 by A14,ANALMETR:36;
then LIN a9,b9,c9 by A56,A57,AFF_1:9;
hence contradiction by A34,ANALMETR:40;
end;
consider e1 such that
A58: o,a1 _|_ o,e1 and
A59: o<>e1 by ANALMETR:def 9;
consider e2 such that
A60: a1,c1 _|_ c2,e2 and
A61: c2<>e2 by ANALMETR:def 9;
reconsider e19=e1,e29=e2 as Element of the AffinStruct of X;
not o9,e19 // c29,e29
proof
assume o9,e19 // c29,e29;
then o,e1 // c2,e2 by ANALMETR:36;
then c2,e2 _|_ o,a1 by A58,A59,ANALMETR:62;
then a1,c1 // o,a1 by A60,A61,ANALMETR:63;
then a19,c19 // o9,a19 by ANALMETR:36;
then a19,c19 // a19,o9 by AFF_1:4;
then LIN a19,c19,o9 by AFF_1:def 1;
then LIN o9,c19,a19 by AFF_1:6;
then o9,c19 // o9,a19 by AFF_1:def 1;
then
A62: o,c1 // o,a1 by ANALMETR:36;
LIN o9,a9,a19 by A10,ANALMETR:40;
then o9,a9 // o9,a19 by AFF_1:def 1;
then o9,a19 // o9,a9 by AFF_1:4;
then
A63: o,a1 // o,a by ANALMETR:36;
LIN o9,c9,c19 by A12,ANALMETR:40;
then o9,c9 // o9,c19 by AFF_1:def 1;
then o9,c19 // o9,c9 by AFF_1:4;
then o,c1 // o,c by ANALMETR:36;
then o,a1 // o,c by A7,A62,ANALMETR:60;
then o,a // o,c by A3,A63,ANALMETR:60;
then LIN o,a,c by ANALMETR:def 10;
then LIN o9,a9,c9 by ANALMETR:40;
then LIN c9,o9,a9 by AFF_1:6;
then c9,o9 // c9,a9 by AFF_1:def 1;
then o9,c9 // a9,c9 by AFF_1:4;
then o,c // a,c by ANALMETR:36;
then a,b // a,c by A6,A14,ANALMETR:60;
hence contradiction by A34,ANALMETR:def 10;
end;
then consider a39 such that
A64: LIN o9,e19,a39 and
A65: LIN c29,e29,a39 by AFF_1:60;
reconsider a3=a39 as Element of X;
LIN o,e1,a3 by A64,ANALMETR:40;
then o,e1 // o,a3 by ANALMETR:def 10;
then
A66: o,a1 _|_ o,a3 by A58,A59,ANALMETR:62;
b<>c
proof
assume b= c;
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A34,ANALMETR:40;
end;
then c2,b2 _|_ b1,c1 by A15,A40,ANALMETR:62;
then
A67: c1,b1 _|_ c2,b2 by ANALMETR:61;
A68: not o,a1 // o,c1
proof
o,a // o,a1 by A10,ANALMETR:def 10;
then o9,a9 // o9,a19 by ANALMETR:36;
then o9,a19 // o9,a9 by AFF_1:4;
then
A69: o,a1 // o,a by ANALMETR:36;
assume o,a1 // o,c1;
then o9,a19 // o9,c19 by ANALMETR:36;
then o9,c19 // o9,a19 by AFF_1:4;
then
A70: o,c1 // o,a1 by ANALMETR:36;
o,c // o,c1 by A12,ANALMETR:def 10;
then o9,c9 // o9,c19 by ANALMETR:36;
then o9,c19 // o9,c9 by AFF_1:4;
then o,c1 // o,c by ANALMETR:36;
then o,a1 // o,c by A7,A70,ANALMETR:60;
then o,a // o,c by A3,A69,ANALMETR:60;
then LIN o,a,c by ANALMETR:def 10;
then LIN o9,a9,c9 by ANALMETR:40;
then LIN c9,a9,o9 by AFF_1:6;
then c9,a9 // c9,o9 by AFF_1:def 1;
then o9,c9// a9,c9 by AFF_1:4;
then o,c // a,c by ANALMETR:36;
then a,b // a,c by A6,A14,ANALMETR:60;
hence contradiction by A34,ANALMETR:def 10;
end;
a9,b9 // o9,c9 by A14,ANALMETR:36;
then o9,c9 // b9,a9 by AFF_1:4;
then
A71: o,c // b,a by ANALMETR:36;
A72: not o,c1 // o,b1
proof
o,b // o,b1 by A11,ANALMETR:def 10;
then o9,b9 // o9,b19 by ANALMETR:36;
then o9,b19 // o9,b9 by AFF_1:4;
then
A73: o,b1 // o,b by ANALMETR:36;
o,c // o,c1 by A12,ANALMETR:def 10;
then o9,c9 // o9,c19 by ANALMETR:36;
then o9,c19 // o9,c9 by AFF_1:4;
then
A74: o,c1 // o,c by ANALMETR:36;
assume o,c1 // o,b1;
then o,b1 // o,c by A7,A74,ANALMETR:60;
then o,b // o,c by A5,A73,ANALMETR:60;
then LIN o,b,c by ANALMETR:def 10;
then LIN o9,b9,c9 by ANALMETR:40;
then LIN c9,o9,b9 by AFF_1:6;
then c9,o9 // c9,b9 by AFF_1:def 1;
then o9,c9 // b9,c9 by AFF_1:4;
then
A75: o,c // b,c by ANALMETR:36;
a9,b9 // o9,c9 by A14,ANALMETR:36;
then o9,c9 // b9,a9 by AFF_1:4;
then o,c // b,a by ANALMETR:36;
then b,a // b,c by A6,A75,ANALMETR:60;
then LIN b,a,c by ANALMETR:def 10;
then LIN b9,a9,c9 by ANALMETR:40;
then LIN a9,b9,c9 by AFF_1:6;
hence contradiction by A34,ANALMETR:40;
end;
a<>b
proof
assume a=b;
then LIN b9,b19,a9 by AFF_1:7;
hence contradiction by A8,ANALMETR:40;
end;
then o,c // a1,b1 by A13,A14,ANALMETR:60;
then o9,c9 // a19,b19 by ANALMETR:36;
then o9,c9 // b19,a19 by AFF_1:4;
then
A76: o,c // b1,a1 by ANALMETR:36;
o,c // o,c1 by A12,ANALMETR:def 10;
then
A77: o,c1 // b1,a1 by A6,A76,ANALMETR:60;
o,c // o,c1 by A12,ANALMETR:def 10;
then
A78: o,c1 _|_ o,c2 by A6,A18,ANALMETR:62;
c,b _|_ c2,b2 by A40,ANALMETR:61;
then b,a _|_ b2,a2 by A1,A18,A32,A48,A71,A50,A38,A36,CONAFFM:def 2;
then b2,a2 _|_ a,b by ANALMETR:61;
then b2,a2 _|_ a1,b1 by A13,A35,ANALMETR:62;
then
A79: b1,a1 _|_ b2,a2 by ANALMETR:61;
o,a // o,a1 by A10,ANALMETR:def 10;
then o,a1 _|_ o,a2 by A2,A48,ANALMETR:62;
then o,a2 // o,a3 by A3,A66,ANALMETR:63;
then LIN o,a2,a3 by ANALMETR:def 10;
then
A80: LIN o9,a29,a39 by ANALMETR:40;
LIN c2,e2,a3 by A65,ANALMETR:40;
then c2,e2 // c2,a3 by ANALMETR:def 10;
then
A81: a1,c1 _|_ c2,a3 by A60,A61,ANALMETR:62;
then c1,a1 _|_ c2,a3 by ANALMETR:61;
then b1,a1 _|_ b2,a3 by A1,A66,A78,A33,A67,A77,A68,A72,CONAFFM:def 2;
then b2,a3 // b2,a2 by A22,A79,ANALMETR:63;
then b29,a39 // b29,a29 by ANALMETR:36;
then b29,a29 // b29,a39 by AFF_1:4;
then a29=a39 by A51,A80,AFF_1:14;
then c,a // a1,c1 by A50,A81,A49,ANALMETR:63;
then c9,a9 // a19,c19 by ANALMETR:36;
then a9,c9 // a19,c19 by AFF_1:4;
hence thesis by ANALMETR:36;
end;
now
assume
A82: LIN a,b,c;
then
A83: LIN a9,b9,c9 by ANALMETR:40;
A84: a<>b
proof
assume a=b;
then LIN b9,b19,a9 by AFF_1:7;
hence contradiction by A8,ANALMETR:40;
end;
A85: now
assume a1,c1 // a,b;
then a19,c19 // a9,b9 by ANALMETR:36;
then a9,b9 // a19,c19 by AFF_1:4;
then
A86: a,b // a1,c1 by ANALMETR:36;
a,b // a,c by A82,ANALMETR:def 10;
hence thesis by A84,A86,ANALMETR:60;
end;
A87: b<>c
proof
assume b=c;
then LIN b9,b19,c9 by AFF_1:7;
hence contradiction by A9,ANALMETR:40;
end;
A88: now
LIN c9,b9,a9 by A83,AFF_1:6;
then c9,b9 // c9,a9 by AFF_1:def 1;
then b9,c9 // a9,c9 by AFF_1:4;
then
A89: b,c // a,c by ANALMETR:36;
assume a1=b1;
hence thesis by A15,A87,A89,ANALMETR:60;
end;
LIN b9,a9,c9 by A83,AFF_1:6;
then b9,a9 // b9,c9 by AFF_1:def 1;
then a9,b9 // b9,c9 by AFF_1:4;
then a,b // b,c by ANALMETR:36;
then b,c // a1,b1 by A13,A84,ANALMETR:60;
then b1,c1 // a1,b1 by A15,A87,ANALMETR:60;
then b19,c19 // a19,b19 by ANALMETR:36;
then b19,a19 // b19,c19 by AFF_1:4;
then LIN b19,a19,c19 by AFF_1:def 1;
then LIN a19,b19,c19 by AFF_1:6;
then LIN a1,b1,c1 by ANALMETR:40;
then
A90: a1,b1 // a1,c1 by ANALMETR:def 10;
a9,b9 // a19,b19 by A13,ANALMETR:36;
then a19,b19 // a9,b9 by AFF_1:4;
then a1,b1 // a,b by ANALMETR:36;
hence thesis by A90,A85,A88,ANALMETR:60;
end;
hence thesis by A28;
end;
theorem
X is satisfying_OSCH & X is satisfying_TDES implies X is satisfying_SCH
proof
assume that
A1: X is satisfying_OSCH and
A2: X is satisfying_TDES;
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 the AffinStruct of X;
reconsider M9=M,N9=N as Subset of the AffinStruct of X;
A24: M9 is being_line by A3,ANALMETR:43;
A25: N9 is being_line by A4,ANALMETR:43;
A26: a1<>b1 implies a2<>b2 & a3<>b3 & a4<>b4
proof
assume
A27: a1<>b1;
A28: now
assume a4=b4;
then a4,a1 // a4,b1 by A23,ANALMETR:59;
then LIN a4,a1,b1 by ANALMETR:def 10;
then LIN a49,a19,b19 by ANALMETR:40;
then LIN a19,b19,a49 by AFF_1:6;
hence contradiction by A5,A7,A13,A24,A27,AFF_1:25;
end;
A29: now
assume a2=b2;
then LIN a2,a1,b1 by A22,ANALMETR:def 10;
then LIN a29,a19,b19 by ANALMETR:40;
then LIN a19,b19,a29 by AFF_1:6;
hence contradiction by A5,A7,A14,A24,A27,AFF_1:25;
end;
A30: now
assume a3=b3;
then LIN a3,a2,b2 by A21,ANALMETR:def 10;
then LIN a39,a29,b29 by ANALMETR:40;
then LIN a29,b29,a39 by AFF_1:6;
hence contradiction by A9,A11,A18,A25,A29,AFF_1:25;
end;
assume a2=b2 or a3=b3 or a4=b4;
hence contradiction by A29,A28,A30;
end;
A31: now
assume
A32: a1<>b1;
A33: now
A34: not LIN a29,b19,b29
proof
assume LIN a29,b19,b29;
then LIN a29,b29,b19 by AFF_1:6;
hence contradiction by A9,A11,A19,A25,A26,A32,AFF_1:25;
end;
assume
A35: a2=a4;
then a2,a1 // b1,b4 by A23,ANALMETR:59;
then b2,b1 // b1,b4 by A5,A14,A22,ANALMETR:60;
then b1,b2 // b1,b4 by ANALMETR:59;
then
A36: b19,b29 // b19,b49 by ANALMETR:36;
a29,b29 // a29,b49 by A9,A11,A12,A25,AFF_1:39,41;
then LIN a29,b29,b49 by AFF_1:def 1;
hence thesis by A21,A35,A34,A36,AFF_1:14;
end;
A37: now
assume that
A38: a2<>a4 and
A39: a1<>a3;
A40: now
consider e1 be Element of X such that
A41: b1,b2 // b1,e1 and
A42: b1<>e1 by ANALMETR:39;
consider x be Element of X such that
A43: LIN a1,a2,x and
A44: a1<>x and
A45: a2<>x by Th2;
reconsider x9=x as Element of the AffinStruct of X;
consider e2 be Element of X such that
A46: a1,b1 // x,e2 and
A47: x<>e2 by ANALMETR:39;
reconsider e19=e1,e29=e2 as Element of the AffinStruct of X;
not b19,e19 // x9,e29
proof
assume b19,e19 // x9,e29;
then b1,e1 // x,e2 by ANALMETR:36;
then b1,b2 // x,e2 by A41,A42,ANALMETR:60;
then b1,b2 // a1,b1 by A46,A47,ANALMETR:60;
then b1,a1 // b1,b2 by ANALMETR:59;
then LIN b1,a1,b2 by ANALMETR:def 10;
then LIN b19,a19,b29 by ANALMETR:40;
hence contradiction by A5,A7,A15,A24,A32,AFF_1:25;
end;
then consider y9 be Element of the AffinStruct of X such that
A48: LIN b19,e19,y9 and
A49: LIN x9,e29,y9 by AFF_1:60;
reconsider y=y9 as Element of X;
A50: a1,a2 // a1,x by A43,ANALMETR:def 10;
A51: not LIN a2,b2,x
proof
A52: a2<>b2
proof
assume a2=b2;
then LIN a2,a1,b1 by A22,ANALMETR:def 10;
then LIN a29,a19,b19 by ANALMETR:40;
then LIN a19,b19,a29 by AFF_1:6;
hence contradiction by A5,A7,A14,A24,A32,AFF_1:25;
end;
LIN a19,a29,x9 by A43,ANALMETR:40;
then
A53: LIN a29,x9,a19 by AFF_1:6;
assume LIN a2,b2,x;
then LIN a29,b29,x9 by ANALMETR:40;
then x9 in N9 by A9,A11,A25,A52,AFF_1:25;
hence contradiction by A9,A17,A25,A45,A53,AFF_1:25;
end;
A54: not LIN a1,b1,a4
proof
assume LIN a1,b1,a4;
then LIN a19,b19,a49 by ANALMETR:40;
hence contradiction by A5,A7,A13,A24,A32,AFF_1:25;
end;
A55: not LIN a1,b1,x
proof
assume LIN a1,b1,x;
then LIN a19,b19,x9 by ANALMETR:40;
then
A56: x9 in M9 by A5,A7,A24,A32,AFF_1:25;
LIN a19,a29,x9 by A43,ANALMETR:40;
then LIN a19,x9,a29 by AFF_1:6;
hence contradiction by A5,A14,A24,A44,A56,AFF_1:25;
end;
assume
A57: M // N;
then M9 // N9 by ANALMETR:46;
then a39,b39 // a29, b29 by A6,A8,A9,A11,AFF_1:39;
then a3,b3 // a2,b2 by ANALMETR:36;
then
A58: a2,b2 // a3,b3 by ANALMETR:59;
LIN x,e2,y by A49,ANALMETR:40;
then x,e2 // x,y by ANALMETR:def 10;
then
A59: a1,b1 // x,y by A46,A47,ANALMETR:60;
A60: b1 <> y
proof
assume b1=y;
then b1,a1 // b1,x by A59,ANALMETR:59;
then LIN b1,a1,x by ANALMETR:def 10;
then LIN b19,a19,x9 by ANALMETR:40;
then
A61: x9 in M9 by A5,A7,A24,A32,AFF_1:25;
LIN a19,a29,x9 by A43,ANALMETR:40;
then LIN a19,x9,a29 by AFF_1:6;
hence contradiction by A5,A14,A24,A44,A61,AFF_1:25;
end;
LIN b1,e1,y by A48,ANALMETR:40;
then b1,e1 // b1,y by ANALMETR:def 10;
then
A62: b1,b2 // b1,y by A41,A42,ANALMETR:60;
then LIN b1,b2,y by ANALMETR:def 10;
then LIN b19,b29,y9 by ANALMETR:40;
then LIN y9,b19,b29 by AFF_1:6;
then LIN y,b1,b2 by ANALMETR:40;
then y,b1 // y,b2 by ANALMETR:def 10;
then
A63: b1,y // b2,y by ANALMETR:59;
a1,a2 // b1, b2 by A22,ANALMETR:59;
then a1,a2 // b1,y by A7,A15,A62,ANALMETR:60;
then
A64: a1,x // b1,y by A5,A14,A50,ANALMETR:60;
A65: not LIN x,y,a3
proof
A66: x<>y
proof
assume x=y;
then x,a1 // x,b1 by A64,ANALMETR:59;
then LIN x,a1,b1 by ANALMETR:def 10;
then LIN x9,a19,b19 by ANALMETR:40;
then LIN a19,b19,x9 by AFF_1:6;
then
A67: x9 in M9 by A5,A7,A24,A32,AFF_1:25;
LIN a19,a29,x9 by A43,ANALMETR:40;
then LIN x9,a19, a29 by AFF_1:6;
hence contradiction by A5,A14,A24,A44,A67,AFF_1:25;
end;
a19,a39 // a19,b19 by A5,A6,A7,A24,AFF_1:39,41;
then a1,a3 // a1,b1 by ANALMETR:36;
then
A68: x,y // a1,a3 by A32,A59,ANALMETR:60;
assume LIN x,y,a3;
then x,y // x,a3 by ANALMETR:def 10;
then x,a3 // a1,a3 by A66,A68,ANALMETR:60;
then a3,a1 // a3,x by ANALMETR:59;
then LIN a3,a1,x by ANALMETR:def 10;
then LIN a39,a19,x9 by ANALMETR:40;
then
A69: x9 in M9 by A5,A6,A24,A39,AFF_1:25;
LIN a19,a29,x9 by A43,ANALMETR:40;
then LIN a19,x9, a29 by AFF_1:6;
hence contradiction by A5,A14,A24,A44,A69,AFF_1:25;
end;
A70: not LIN x,y,a4
proof
A71: x<>y
proof
assume x=y;
then x,a1 // x,b1 by A64,ANALMETR:59;
then LIN x,a1,b1 by ANALMETR:def 10;
then LIN x9,a19,b19 by ANALMETR:40;
then LIN a19,b19,x9 by AFF_1:6;
then
A72: x9 in M9 by A5,A7,A24,A32,AFF_1:25;
LIN a19,a29,x9 by A43,ANALMETR:40;
then LIN x9,a19, a29 by AFF_1:6;
hence contradiction by A5,A14,A24,A44,A72,AFF_1:25;
end;
M9 // N9 by A57,ANALMETR:46;
then a19,b19 // a29,a49 by A5,A7,A9,A10,AFF_1:39;
then a1,b1 // a2,a4 by ANALMETR:36;
then
A73: a2,a4 // x,y by A32,A59,ANALMETR:60;
assume LIN x,y,a4;
then x,y // x,a4 by ANALMETR:def 10;
then a2,a4 // x,a4 by A71,A73,ANALMETR:60;
then a4,a2 // a4,x by ANALMETR:59;
then LIN a4,a2,x by ANALMETR:def 10;
then LIN a49,a29,x9 by ANALMETR:40;
then
A74: x9 in N9 by A9,A10,A25,A38,AFF_1:25;
LIN a19,a29,x9 by A43,ANALMETR:40;
then LIN a29,x9, a19 by AFF_1:6;
hence contradiction by A9,A17,A25,A45,A74,AFF_1:25;
end;
A75: not LIN a2,b2,a3
proof
A76: a2<>b2
proof
assume a2=b2;
then LIN a2,a1,b1 by A22,ANALMETR:def 10;
then LIN a29,a19,b19 by ANALMETR:40;
then LIN a19,b19,a29 by AFF_1:6;
hence contradiction by A5,A7,A14,A24,A32,AFF_1:25;
end;
assume LIN a2,b2,a3;
then LIN a29,b29,a39 by ANALMETR:40;
hence contradiction by A9,A11,A18,A25,A76,AFF_1:25;
end;
A77: X is satisfying_TDES implies X is satisfying_des
proof
assume X is satisfying_TDES;
then the AffinStruct of X is Moufangian by Th7;
then the AffinStruct of X is translational by AFF_2:14;
hence thesis by Th8;
end;
LIN a19,a29,x9 by A43,ANALMETR:40;
then LIN x9,a19, a29 by AFF_1:6;
then LIN x,a1,a2 by ANALMETR:40;
then x,a1 // x,a2 by ANALMETR:def 10;
then a1,x // a2,x by ANALMETR:59;
then a2,x // b1,y by A44,A64,ANALMETR:60;
then
A78: a2,x // b2,y by A60,A63,ANALMETR:60;
a19,b19 // a39,b39 by A5,A6,A7,A8,A24,AFF_1:39,41;
then a1,b1 // a3,b3 by ANALMETR:36;
then
A79: x,y // a3,b3 by A32,A59,ANALMETR:60;
M9 // N9 by A57,ANALMETR:46;
then a19,b19 // a49,b49 by A5,A7,A10,A12,AFF_1:39;
then a1,b1 // a4,b4 by ANALMETR:36;
then
A80: x,y // a4,b4 by A32,A59,ANALMETR:60;
M9 // N9 by A57,ANALMETR:46;
then a19,b19 // a29,b29 by A5,A7,A9,A11,AFF_1:39;
then a1,b1 // a2,b2 by ANALMETR:36;
then
A81: a2,b2 // x,y by A32,A59,ANALMETR:60;
a2,a3 // b2,b3 by A21,ANALMETR:59;
then
A82: x,a3 // y,b3 by A2,A77,A51,A75,A81,A58,A78;
M9 // N9 by A57,ANALMETR:46;
then a19,b19 // a49, b49 by A5,A7,A10,A12,AFF_1:39;
then a1,b1 // a4,b4 by ANALMETR:36;
then x,a4 // y,b4 by A2,A23,A59,A77,A55,A54,A64;
hence thesis by A2,A77,A82,A65,A70,A79,A80;
end;
now
assume not M // N;
then not M9 // N9 by ANALMETR:46;
then consider o9 being Element of the AffinStruct of X such that
A83: o9 in M9 and
A84: o9 in N9 by A24,A25,AFF_1:58;
reconsider o=o9 as Element of X;
consider K such that
A85: o in K and
A86: N _|_ K by A4,Th3;
reconsider K9=K as Subset of the AffinStruct of X;
A87: K is being_line by A86,ANALMETR:44;
then
A88: K9 is being_line by ANALMETR:43;
now
A89: not a2 in K & not a4 in K & not b2 in K & not b4 in K
proof
A90: now
let x be Element of X;
assume that
A91: x in N and
A92: o<>x;
assume x in K;
then o,x _|_ o,x by A84,A85,A86,A91,ANALMETR:56;
hence contradiction by A92,ANALMETR:39;
end;
assume not thesis;
hence contradiction by A9,A10,A11,A12,A13,A14,A15,A16,A83,A90;
end;
A93: LIN o,a2,b2 by A4,A9,A11,A84,Th4;
A94: now
assume LIN a1,b1,a4;
then LIN a19,b19,a49 by ANALMETR:40;
hence contradiction by A5,A7,A13,A24,A32,AFF_1:25;
end;
A95: LIN o,a3,b3 by A3,A6,A8,A83,Th4;
A96: now
assume LIN a3,b3,a2;
then LIN a39,b39,a29 by ANALMETR:40;
hence contradiction by A6,A8,A14,A24,A26,A32,AFF_1:25;
end;
A97: LIN o,a1,b1 by A3,A5,A7,A83,Th4;
A98: now
let x9 be Element of the AffinStruct of X;
consider D9 being Subset of the AffinStruct of X such that
A99: x9 in D9 and
A100: N9 // D9 by A25,AFF_1:49;
reconsider D=D9 as Subset of the carrier of X;
N // D by A100,ANALMETR:46;
then K _|_ D by A86,ANALMETR:52;
then consider y being Element of X such that
A101: y in K and
A102: y in D by ANALMETR:66;
reconsider y9=y as Element of the AffinStruct of X;
take y9;
thus y9 in K9 & x9,y9 // N9 by A99,A100,A101,A102,AFF_1:40;
end;
then consider d19 be Element of the AffinStruct of X such that
A103: d19 in K9 and
A104: a19,d19 // N9;
consider e19 be Element of the AffinStruct of X such that
A105: e19 in K9 and
A106: b19,e19 // N9 by A98;
consider d39 be Element of the AffinStruct of X such that
A107: d39 in K9 and
A108: a39,d39 // N9 by A98;
consider e39 be Element of the AffinStruct of X such that
A109: e39 in K9 and
A110: b39,e39 // N9 by A98;
reconsider d1=d19,d3=d39,e1=e19,e3=e39 as Element of X;
A111: LIN o,d1,e1 by A85,A87,A103,A105,Th4;
A112: o<>e1 & o<>e3 & o<>d1 & o<>d3
proof
A113: now
let x,y be Element of X,
x9,y9 be Element of the AffinStruct of X;
assume that
A114: x9,y9 // N9 and
A115: x=x9 and
A116: y=y9 and
x in M and
y in K and
A117: not x in N;
assume o=y;
then o9,x9 // N9 by A114,A116,AFF_1:34;
hence contradiction by A25,A84,A115,A117,AFF_1:23;
end;
assume not thesis;
hence
contradiction by A5,A6,A7,A8,A17,A18,A19,A20,A103,A104,A107,A108
,A109,A110,A105,A106,A113;
end;
a1,d1 // o,a2 by A9,A84,A104,Th6;
then
A118: d1,a1 // o,a2 by ANALMETR:59;
A119: not e1 in N by A19,A106,AFF_1:35;
A120: not d3 in N by A18,A108,AFF_1:35;
a19,d19 // b19,e19 by A25,A104,A106,AFF_1:31;
then a1,d1 // b1,e1 by ANALMETR:36;
then
A121: d1,a1 // e1,b1 by ANALMETR:59;
assume
A122: K<>M;
A123: now
assume LIN a3,b3,d3;
then LIN a39,b39,d39 by ANALMETR:40;
then d3 in M by A6,A8,A24,A26,A32,AFF_1:25;
hence contradiction by A3,A83,A85,A87,A122,A107,A112,Th5;
end;
A124: now
assume LIN a1,b1,d1;
then LIN a19,b19,d19 by ANALMETR:40;
then d1 in M by A5,A7,A24,A32,AFF_1:25;
hence contradiction by A3,A83,A85,A87,A122,A103,A112,Th5;
end;
a39,d39 // b39,e39 by A25,A108,A110,AFF_1:31;
then
A125: a3,d3 // b3,e3 by ANALMETR:36;
then
A126: d3,a3 // e3,b3 by ANALMETR:59;
A127: not LIN d3,e3,a3 & not LIN d3,e3,a4
proof
A128: d3<>e3
proof
assume not thesis;
then LIN e3,a3,b3 by A126,ANALMETR:def 10;
then LIN e39,a39,b39 by ANALMETR:40;
then LIN a39,b39,e39 by AFF_1:6;
then e39 in M9 by A6,A8,A24,A26,A32,AFF_1:25;
hence contradiction by A24,A83,A85,A88,A122,A109,A112,AFF_1:18;
end;
assume not thesis;
then LIN d39,e39,a39 or LIN d39,e39,a49 by ANALMETR:40;
then a39 in K9 or a49 in K9 by A88,A107,A109,A128,AFF_1:25;
hence
contradiction by A6,A10,A13,A18,A24,A25,A83,A84,A85,A86,A88,A122,
AFF_1:18;
end;
A129: now
assume LIN a1,b1,a2;
then LIN a19,b19,a29 by ANALMETR:40;
hence contradiction by A5,A7,A14,A24,A32,AFF_1:25;
end;
A130: LIN o,a4,b4 by A4,A10,A12,A84,Th4;
a1,a2 // b1,b2 by A22,ANALMETR:59;
then d1,a2 // e1,b2 by A2,A14,A15,A17,A19,A83,A84,A112,A93,A97,A111
,A124,A129,A121,A118;
then
A131: a2,d1 // b2,e1 by ANALMETR:59;
A132: not e3 in N by A20,A110,AFF_1:35;
A133: LIN o,d3,e3 by A85,A87,A107,A109,Th4;
a1,d1 // o,a4 by A10,A84,A104,Th6;
then d1,a1 // o,a4 by ANALMETR:59;
then
A134: d1,a4 // e1,b4 by A2,A13,A16,A17,A19,A23,A83,A84,A112,A97,A130,A111
,A124,A94,A121;
A135: a3,d3 // o,a4 by A10,A84,A108,Th6;
A136: not d1 in N by A17,A104,AFF_1:35;
a3,d3 // o,a2 by A9,A84,A108,Th6;
then d3,a3 // o,a2 by ANALMETR:59;
then d3,a2 // e3,b2 by A2,A14,A15,A18,A20,A21,A83,A84,A112,A93,A95
,A133,A123,A96,A126;
then d3,a4 // e3,b4 by A1,A9,A10,A11,A12,A86,A103,A107,A109,A105,A131
,A134,A136,A120,A119,A132,A89;
hence
thesis by A2,A13,A16,A18,A20,A83,A84,A112,A130,A95,A133,A125,A127
,A135;
end;
hence
thesis by A1,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,A15,A16,A17,A18,A19,A20
,A21,A22,A23,A86;
end;
hence thesis by A40;
end;
now
A137: not LIN a19,b29,b19
proof
assume LIN a19,b29,b19;
then LIN a19,b19,b29 by AFF_1:6;
hence contradiction by A5,A7,A15,A24,A32,AFF_1:25;
end;
a19,b19 // a19,b39 by A5,A7,A8,A24,AFF_1:39,41;
then
A138: LIN a19,b19,b39 by AFF_1:def 1;
assume
A139: a1=a3;
then a2,a1 // b2,b3 by A21,ANALMETR:59;
then b2,b1 // b2,b3 by A5,A14,A22,ANALMETR:60;
then b29,b19 // b29,b39 by ANALMETR:36;
hence thesis by A23,A139,A137,A138,AFF_1:14;
end;
hence thesis by A33,A37;
end;
A140: a1=b1 implies a2=b2 & a3=b3 & a4=b4
proof
assume
A141: a1=b1;
A142: now
LIN a1,a4,b4 by A23,A141,ANALMETR:def 10;
then LIN a19,a49,b49 by ANALMETR:40;
then
A143: LIN a49,b49,a19 by AFF_1:6;
assume a4<>b4;
hence contradiction by A10,A12,A17,A25,A143,AFF_1:25;
end;
A144: now
a1,a2 // a1,b2 by A22,A141,ANALMETR:59;
then LIN a1,a2,b2 by ANALMETR:def 10;
then LIN a19,a29,b29 by ANALMETR:40;
then
A145: LIN a29,b29,a19 by AFF_1:6;
assume a2<>b2;
hence contradiction by A9,A11,A17,A25,A145,AFF_1:25;
end;
A146: now
a2,a3 // a2,b3 by A21,A144,ANALMETR:59;
then LIN a2,a3,b3 by ANALMETR:def 10;
then LIN a29,a39,b39 by ANALMETR:40;
then
A147: LIN a39,b39,a29 by AFF_1:6;
assume a3<>b3;
hence contradiction by A6,A8,A14,A24,A147,AFF_1:25;
end;
assume a2<>b2 or a3<>b3 or a4<>b4;
hence contradiction by A144,A142,A146;
end;
now
assume a1=b1;
then a39,a49 // b39,b49 by A140,AFF_1:2;
hence thesis by ANALMETR:36;
end;
hence thesis by A31;
end;
theorem
X is satisfying_OPAP & X is satisfying_DES implies X is satisfying_PAP
proof
assume that
A1: X is satisfying_OPAP and
A2: X is satisfying_DES;
let o,a1,a2,a3,b1,b2,b3,M,N;
assume that
A3: M is being_line and
A4: N is being_line and
A5: o in M and
A6: a1 in M and
A7: a2 in M and
A8: a3 in M and
A9: o in N and
A10: b1 in N and
A11: b2 in N and
A12: b3 in N and
A13: not b2 in M and
A14: not a3 in N and
A15: o<>a1 and
A16: o<>a2 and
o<>a3 and
A17: o<>b1 and
o<>b2 and
A18: o<>b3 and
A19: a3,b2 // a2,b1 and
A20: a3,b3 // a1,b1;
reconsider o9=o,a19=a1,a29=a2,a39=a3,b19=b1,b29=b2,b39=b3
as Element of the AffinStruct of X;
reconsider M9=M,N9=N as Subset of the AffinStruct of X;
A21: M9 is being_line by A3,ANALMETR:43;
A22: N9 is being_line by A4,ANALMETR:43;
now
assume
A23: not M _|_ N;
A24: now
assume that
A25: a1<>a2 and
A26: a2<>a3 and
A27: a1<>a3;
A28: b1<>b2 & b2<>b3 & b1<>b3
proof
A29: now
A30: not LIN o9,b19,a19
proof
o9,a19 // o9,a39 by A5,A6,A8,A21,AFF_1:39,41;
then
A31: LIN o9,a19,a39 by AFF_1:def 1;
assume LIN o9,b19,a19;
then a19 in N9 by A9,A10,A17,A22,AFF_1:25;
hence contradiction by A9,A14,A15,A22,A31,AFF_1:25;
end;
assume b1=b3;
then b1,a1 // b1,a3 by A20,ANALMETR:59;
then
A32: b19,a19 // b19,a39 by ANALMETR:36;
o9,a19 // o9,a39 by A5,A6,A8,A21,AFF_1:39,41;
then LIN o9,a19,a39 by AFF_1:def 1;
hence contradiction by A27,A30,A32,AFF_1:14;
end;
A33: now
A34: not LIN o9,b19,a19
proof
o9,a19 // o9,a39 by A5,A6,A8,A21,AFF_1:39,41;
then
A35: LIN o9,a19,a39 by AFF_1:def 1;
assume LIN o9,b19,a19;
then a19 in N9 by A9,A10,A17,A22,AFF_1:25;
hence contradiction by A9,A14,A15,A22,A35,AFF_1:25;
end;
assume b2=b3;
then a1,b1 // a2,b1 by A8,A13,A19,A20,ANALMETR:60;
then b1,a1 // b1,a2 by ANALMETR:59;
then
A36: b19,a19 // b19,a29 by ANALMETR:36;
o9,a19 // o9,a29 by A5,A6,A7,A21,AFF_1:39,41;
then LIN o9,a19,a29 by AFF_1:def 1;
hence contradiction by A25,A34,A36,AFF_1:14;
end;
A37: now
A38: not LIN o9,b29,a29
proof
assume LIN o9,b29,a29;
then LIN o9,a29,b29 by AFF_1:6;
hence contradiction by A5,A7,A13,A16,A21,AFF_1:25;
end;
assume b1=b2;
then b2,a2 // b2,a3 by A19,ANALMETR:59;
then
A39: b29,a29 // b29,a39 by ANALMETR:36;
o9,a29 // o9,a39 by A5,A7,A8,A21,AFF_1:39,41;
then LIN o9,a29,a39 by AFF_1:def 1;
hence contradiction by A26,A38,A39,AFF_1:14;
end;
assume b1=b2 or b2=b3 or b1=b3;
hence contradiction by A37,A33,A29;
end;
A40: now
A41: not LIN b3,b1,a3
proof
assume LIN b3,b1,a3;
then LIN b39,b19,a39 by ANALMETR:40;
hence contradiction by A10,A12,A14,A22,A28,AFF_1:25;
end;
o9,b29 // o9,b39 by A9,A11,A12,A22,AFF_1:39,41;
then LIN o9,b29,b39 by AFF_1:def 1;
then
A42: LIN o,b2,b3 by ANALMETR:40;
A43: not LIN b2,b1,a3
proof
assume LIN b2,b1,a3;
then LIN b29,b19,a39 by ANALMETR:40;
hence contradiction by A10,A11,A14,A22,A28,AFF_1:25;
end;
o9,a39 // o9,a19 by A5,A6,A8,A21,AFF_1:39,41;
then LIN o9,a39,a19 by AFF_1:def 1;
then
A44: LIN o,a3,a1 by ANALMETR:40;
consider x be Element of X such that
A45: o,b2 _|_ o,x and
A46: o<>x by ANALMETR:39;
A47: o,x _|_ N by A4,A5,A9,A11,A13,A45,ANALMETR:55;
consider e19 be Element of the AffinStruct of X such that
A48: a39,b39 // b29,e19 and
A49: b29<> e19 by DIRAF:40;
reconsider x9=x as Element of the AffinStruct of X;
LIN o9,x9,x9 by AFF_1:7;
then consider A9 be Subset of the AffinStruct of X such that
A50: A9 is being_line and
A51: o9 in A9 and
A52: x9 in A9 and
x9 in A9 by AFF_1:21;
reconsider A=A9 as Subset of X;
A53: for e1 holds e1 in A implies LIN o,x,e1
proof
let e1 such that
A54: e1 in A;
reconsider e19=e1 as Element of the AffinStruct of X;
o9,x9 // o9,e19 by A50,A51,A52,A54,AFF_1:39,41;
then LIN o9,x9,e19 by AFF_1:def 1;
hence thesis by ANALMETR:40;
end;
for e1 holds LIN o,x,e1 implies e1 in A
proof
let e1 such that
A55: LIN o,x,e1;
reconsider e19=e1 as Element of the AffinStruct of X;
LIN o9,x9,e19 by A55,ANALMETR:40;
hence thesis by A46,A50,A51,A52,AFF_1:25;
end;
then A=Line(o,x) by A53,ANALMETR:def 11;
then
A56: A _|_ N by A46,A47,ANALMETR:def 14;
A57: not b2 in A
proof
A58: o9,b29 // o9,b29 by AFF_1:2;
assume b2 in A;
then A9 // N9 by A5,A9,A11,A13,A22,A50,A51,A58,AFF_1:38;
then A // N by ANALMETR:46;
hence contradiction by A56,ANALMETR:52;
end;
assume
A59: not a3,b3 _|_ o,b2;
not b29,e19 // A9
proof
assume
A60: b29,e19 // A9;
consider d19,d29 be Element of the AffinStruct of X such that
A61: d19<>d29 and
A62: A9=Line(d19,d29) by A50,AFF_1:def 3;
A63: d29 in A9 by A62,AFF_1:15;
reconsider d1=d19,d2=d29 as Element of X;
d19,d29 // d19,d29 by AFF_1:2;
then d19,d29 // A9 by A61,A62,AFF_1:def 4;
then b29,e19 // d19,d29 by A50,A60,AFF_1:31;
then a39,b39 // d19,d29 by A48,A49,AFF_1:5;
then
A64: a3,b3 // d1,d2 by ANALMETR:36;
d19 in A9 by A62,AFF_1:15;
then d1,d2 _|_ o,b2 by A9,A11,A56,A63,ANALMETR:56;
hence contradiction by A59,A61,A64,ANALMETR:62;
end;
then consider c39 be Element of the AffinStruct of X such that
A65: c39 in A9 and
A66: LIN b29,e19,c39 by A50,AFF_1:59;
b29,e19 // b29,c39 by A66,AFF_1:def 1;
then
A67: a39,b39 // b29,c39 by A48,A49,AFF_1:5;
consider e19 be Element of the AffinStruct of X such that
A68: c39,a39 // a19,e19 and
A69: a19<> e19 by DIRAF:40;
not a19,e19 // A9
proof
A70: c39<>o9
proof
assume c39=o9;
then
A71: a3,b3 // b2,o by A67,ANALMETR:36;
b29,o9 // b29,b39 by A9,A11,A12,A22,AFF_1:39,41;
then b2,o // b2,b3 by ANALMETR:36;
then a3,b3 // b2,b3 by A5,A13,A71,ANALMETR:60;
then b3,b2 // b3,a3 by ANALMETR:59;
then LIN b3,b2,a3 by ANALMETR:def 10;
then LIN b39,b29,a39 by ANALMETR:40;
hence contradiction by A11,A12,A14,A22,A28,AFF_1:25;
end;
assume
A72: a19,e19 // A9;
A73: o9,a39 // o9,a39 by AFF_1:2;
o9,c39 // A9 by A50,A51,A65,AFF_1:40,41;
then a19,e19 // o9,c39 by A50,A72,AFF_1:31;
then c39,a39 // o9,c39 by A68,A69,AFF_1:5;
then c39,o9 // c39,a39 by AFF_1:4;
then LIN c39,o9,a39 by AFF_1:def 1;
then a39 in A9 by A50,A51,A65,A70,AFF_1:25;
then A9 // M9 by A5,A8,A9,A14,A21,A50,A51,A73,AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23,A56,ANALMETR:52;
end;
then consider c19 be Element of the AffinStruct of X such that
A74: c19 in A9 and
A75: LIN a19,e19,c19 by A50,AFF_1:59;
reconsider c1=c19 as Element of X;
reconsider c3=c39 as Element of X;
a19,e19 // a19,c19 by A75,AFF_1:def 1;
then
A76: c39,a39 // a19,c19 by A68,A69,AFF_1:5;
then
A77: c3,a3 // a1,c1 by ANALMETR:36;
consider e19 be Element of the AffinStruct of X such that
A78: c39,a39 // a29,e19 and
A79: a29<> e19 by DIRAF:40;
not a29,e19 // A9
proof
A80: c39<>o9
proof
assume c39=o9;
then
A81: a3,b3 // b2,o by A67,ANALMETR:36;
b29,o9 // b29,b39 by A9,A11,A12,A22,AFF_1:39,41;
then b2,o // b2,b3 by ANALMETR:36;
then a3,b3 // b2,b3 by A5,A13,A81,ANALMETR:60;
then b3,b2 // b3,a3 by ANALMETR:59;
then LIN b3,b2,a3 by ANALMETR:def 10;
then LIN b39,b29,a39 by ANALMETR:40;
hence contradiction by A11,A12,A14,A22,A28,AFF_1:25;
end;
assume
A82: a29,e19 // A9;
A83: o9,a39 // o9,a39 by AFF_1:2;
o9,c39 // A9 by A50,A51,A65,AFF_1:40,41;
then a29,e19 // o9,c39 by A50,A82,AFF_1:31;
then c39,a39 // o9,c39 by A78,A79,AFF_1:5;
then c39,o9 // c39,a39 by AFF_1:4;
then LIN c39,o9,a39 by AFF_1:def 1;
then a39 in A9 by A50,A51,A65,A80,AFF_1:25;
then A9 // M9 by A5,A8,A9,A14,A21,A50,A51,A83,AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23,A56,ANALMETR:52;
end;
then consider c29 be Element of the AffinStruct of X such that
A84: c29 in A9 and
A85: LIN a29,e19,c29 by A50,AFF_1:59;
reconsider c2=c29 as Element of X;
a29,e19 // a29,c29 by A85,AFF_1:def 1;
then
A86: c39,a39 // a29,c29 by A78,A79,AFF_1:5;
then
A87: c3,a3 // a2,c2 by ANALMETR:36;
A88: o<>c3 & o<>c2 & o<>c1
proof
A89: now
assume
A90: o=c3;
b29,o9 // b39,b29 by A9,A11,A12,A22,AFF_1:39,41;
then a39,b39 // b39,b29 by A5,A13,A67,A90,AFF_1:5;
then b39,b29 // b39,a39 by AFF_1:4;
then LIN b39,b29,a39 by AFF_1:def 1;
hence contradiction by A11,A12,A14,A22,A28,AFF_1:25;
end;
A91: now
a19,o9 // a19,a39 by A5,A6,A8,A21,AFF_1:39,41;
then
A92: a1,o // a1,a3 by ANALMETR:36;
assume o=c2 or o=c1;
then
A93: c3,a3 // a1,o or c3,a3 // a2,o by A76,A86,ANALMETR:36;
a29,o9 // a19,a39 by A5,A6,A7,A8,A21,AFF_1:39,41;
then a2,o // a1,a3 by ANALMETR:36;
then c3,a3 // a1,a3 by A15,A16,A93,A92,ANALMETR:60;
then a3,a1 // a3,c3 by ANALMETR:59;
then LIN a3,a1,c3 by ANALMETR:def 10;
then LIN a39,a19,c39 by ANALMETR:40;
then
A94: c39 in M9 by A6,A8,A21,A27,AFF_1:25;
o9,c39 // o9,c39 by AFF_1:2;
then A9 // M9 by A5,A21,A50,A51,A65,A89,A94,AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23,A56,ANALMETR:52;
end;
assume o=c3 or o=c2 or o=c1;
hence contradiction by A89,A91;
end;
A95: not c3 in N
proof
A96: o9,c39 // o9,c39 by AFF_1:2;
assume c3 in N;
then A9 // N9 by A9,A22,A50,A51,A65,A88,A96,AFF_1:38;
then A // N by ANALMETR:46;
hence contradiction by A56,ANALMETR:52;
end;
A97: not LIN a3,a2,c3
proof
assume LIN a3,a2,c3;
then LIN a39,a29,c39 by ANALMETR:40;
then
A98: c39 in M9 by A7,A8,A21,A26,AFF_1:25;
o9,c39 // o9,c39 by AFF_1:2;
then A9 // M9 by A5,A21,A50,A51,A65,A88,A98,AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23,A56,ANALMETR:52;
end;
A99: not LIN a3,a1,c3
proof
assume LIN a3,a1,c3;
then LIN a39,a19,c39 by ANALMETR:40;
then
A100: c39 in M9 by A6,A8,A21,A27,AFF_1:25;
o9,c39 // o9,c39 by AFF_1:2;
then A9 // M9 by A5,A21,A50,A51,A65,A88,A100,AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23,A56,ANALMETR:52;
end;
A101: not LIN a1,a2,c1
proof
assume LIN a1,a2,c1;
then LIN a19,a29,c19 by ANALMETR:40;
then
A102: c19 in M9 by A6,A7,A21,A25,AFF_1:25;
o9,c19 // o9,c19 by AFF_1:2;
then M9 // A9 by A5,A21,A50,A51,A74,A88,A102,AFF_1:38;
then M // A by ANALMETR:46;
hence contradiction by A23,A56,ANALMETR:52;
end;
o9,a19 // o9,a29 by A5,A6,A7,A21,AFF_1:39,41;
then LIN o9,a19,a29 by AFF_1:def 1;
then
A103: LIN o,a1,a2 by ANALMETR:40;
o9,b29 // o9,b19 by A9,A10,A11,A22,AFF_1:39,41;
then LIN o9,b29,b19 by AFF_1:def 1;
then
A104: LIN o,b2,b1 by ANALMETR:40;
o9,c19 // o9,c29 by A50,A51,A74,A84,AFF_1:39,41;
then LIN o9,c19,c29 by AFF_1:def 1;
then
A105: LIN o,c1,c2 by ANALMETR:40;
o9,c39 // o9,c29 by A50,A51,A65,A84,AFF_1:39,41;
then LIN o9,c39,c29 by AFF_1:def 1;
then
A106: LIN o,c3,c2 by ANALMETR:40;
o9,c39 // o9,c19 by A50,A51,A65,A74,AFF_1:39,41;
then LIN o9,c39,c19 by AFF_1:def 1;
then
A107: LIN o,c3,c1 by ANALMETR:40;
c3<>a3
proof
A108: o9,a39 // o9,a39 by AFF_1:2;
assume c3=a3;
then A9 // M9 by A5,A8,A9,A14,A21,A50,A51,A65,A108,AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23,A56,ANALMETR:52;
end;
then a1,c1 // a2,c2 by A77,A87,ANALMETR:60;
then
A109: c1,a1 // c2,a2 by ANALMETR:59;
A110: not LIN c1,c2,b2
proof
A111: c19<>c29
proof
A112: c3<>a3
proof
A113: o9,c39 // o9,c39 by AFF_1:2;
assume c3=a3;
then A9 // M9 by A5,A8,A9,A14,A21,A50,A51,A65,A113,AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23,A56,ANALMETR:52;
end;
assume c19=c29;
then a1,c1 // a2,c1 by A77,A87,A112,ANALMETR:60;
then c1,a2 // c1,a1 by ANALMETR:59;
then LIN c1,a2,a1 by ANALMETR:def 10;
then LIN c19,a29,a19 by ANALMETR:40;
then LIN a19,a29,c19 by AFF_1:6;
then
A114: c19 in M9 by A6,A7,A21,A25,AFF_1:25;
o9,c19 // o9,c19 by AFF_1:2;
then A9 // M9 by A5,A21,A50,A51,A74,A88,A114,AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23,A56,ANALMETR:52;
end;
assume LIN c1,c2,b2;
then LIN c19,c29,b29 by ANALMETR:40;
then b29 in A9 by A50,A74,A84,A111,AFF_1:25;
then A9=N9 by A5,A9,A11,A13,A22,A50,A51,AFF_1:18;
then A9 // N9 by A22,AFF_1:41;
then A // N by ANALMETR:46;
hence contradiction by A56,ANALMETR:52;
end;
o9,a39 // o9,a29 by A5,A7,A8,A21,AFF_1:39,41;
then LIN o9,a39,a29 by AFF_1:def 1;
then
A115: LIN o,a3,a2 by ANALMETR:40;
o9,b39 // o9,b19 by A9,A10,A12,A22,AFF_1:39,41;
then LIN o9,b39,b19 by AFF_1:def 1;
then
A116: LIN o,b3,b1 by ANALMETR:40;
a3,c3 // a1,c1 by A77,ANALMETR:59;
then b3,c3 // b1,c1 by A2,A9,A14,A15,A17,A18,A20,A88,A99,A41,A44,A116
,A107,CONAFFM:def 1;
then
A117: c3,b3 // c1,b1 by ANALMETR:59;
a3,c3 // a2,c2 by A87,ANALMETR:59;
then b2,c3 // b1,c2 by A2,A5,A9,A13,A14,A16,A17,A19,A88,A115,A104,A106
,A43,A97,CONAFFM:def 1;
then c3,b2 // c2,b1 by ANALMETR:59;
then c1,b2 // c2,b3 by A1,A9,A10,A11,A12,A17,A18,A51,A56,A65,A74,A84
,A88,A117,A57,A95;
hence thesis by A2,A5,A13,A15,A16,A18,A88,A103,A42,A105,A101,A110,A109,
CONAFFM:def 1;
end;
now
o9,a19 // o9,a29 by A5,A6,A7,A21,AFF_1:39,41;
then LIN o9,a19,a29 by AFF_1:def 1;
then
A118: LIN o,a1,a2 by ANALMETR:40;
o9,b29 // o9,b19 by A9,A10,A11,A22,AFF_1:39,41;
then LIN o9,b29,b19 by AFF_1:def 1;
then
A119: LIN o,b2,b1 by ANALMETR:40;
o9,b29 // o9,b39 by A9,A11,A12,A22,AFF_1:39,41;
then LIN o9,b29,b39 by AFF_1:def 1;
then
A120: LIN o,b2,b3 by ANALMETR:40;
A121: not LIN b3,b1,a3 & not LIN b2,b1,a3
proof
assume LIN b3,b1,a3 or LIN b2,b1,a3;
then LIN b39,b19,a39 or LIN b29,b19,a39 by ANALMETR:40;
hence contradiction by A10,A11,A12,A14,A22,A28,AFF_1:25;
end;
o9,a39 // o9,a29 by A5,A7,A8,A21,AFF_1:39,41;
then LIN o9,a39,a29 by AFF_1:def 1;
then
A122: LIN o,a3,a2 by ANALMETR:40;
o9,b39 // o9,b19 by A9,A10,A12,A22,AFF_1:39,41;
then LIN o9,b39,b19 by AFF_1:def 1;
then
A123: LIN o,b3,b1 by ANALMETR:40;
o9,a39 // o9,a19 by A5,A6,A8,A21,AFF_1:39,41;
then LIN o9,a39,a19 by AFF_1:def 1;
then
A124: LIN o,a3,a1 by ANALMETR:40;
consider x be Element of X such that
A125: o,b2 _|_ o,x and
A126: o<>x by ANALMETR:39;
A127: o,x _|_ N by A4,A5,A9,A11,A13,A125,ANALMETR:55;
consider e19 be Element of the AffinStruct of X such that
A128: a39,b29 // b39,e19 and
A129: b39<> e19 by DIRAF:40;
reconsider x9=x as Element of the AffinStruct of X;
LIN o9,x9,x9 by AFF_1:7;
then consider A9 be Subset of the AffinStruct of X such that
A130: A9 is being_line and
A131: o9 in A9 and
A132: x9 in A9 and
x9 in A9 by AFF_1:21;
reconsider A=A9 as Subset of X;
A133: for e1 holds e1 in A implies LIN o,x,e1
proof
let e1 such that
A134: e1 in A;
reconsider e19=e1 as Element of the AffinStruct of X;
o9,x9 // o9,e19 by A130,A131,A132,A134,AFF_1:39,41;
then LIN o9,x9,e19 by AFF_1:def 1;
hence thesis by ANALMETR:40;
end;
for e1 holds LIN o,x,e1 implies e1 in A
proof
let e1 such that
A135: LIN o,x,e1;
reconsider e19=e1 as Element of the AffinStruct of X;
LIN o9,x9,e19 by A135,ANALMETR:40;
hence thesis by A126,A130,A131,A132,AFF_1:25;
end;
then A=Line(o,x) by A133,ANALMETR:def 11;
then
A136: A _|_ N by A126,A127,ANALMETR:def 14;
assume
A137: a3,b3 _|_ o,b2;
not b39,e19 // A9
proof
assume
A138: b39,e19 // A9;
consider d19,d29 be Element of the AffinStruct of X such that
A139: d19<>d29 and
A140: A9=Line(d19,d29) by A130,AFF_1:def 3;
A141: d29 in A9 by A140,AFF_1:15;
reconsider d1=d19,d2=d29 as Element of X;
d19,d29 // d19,d29 by AFF_1:2;
then d19,d29 // A9 by A139,A140,AFF_1:def 4;
then b39,e19 // d19,d29 by A130,A138,AFF_1:31;
then a39,b29 // d19,d29 by A128,A129,AFF_1:5;
then
A142: a3,b2 // d1,d2 by ANALMETR:36;
d19 in A9 by A140,AFF_1:15;
then d1,d2 _|_ o,b2 by A9,A11,A136,A141,ANALMETR:56;
then a3,b2 _|_ o,b2 by A139,A142,ANALMETR:62;
then a3,b2 // a3,b3 by A5,A13,A137,ANALMETR:63;
then LIN a3,b2,b3 by ANALMETR:def 10;
then LIN a39,b29,b39 by ANALMETR:40;
then LIN b29,b39,a39 by AFF_1:6;
hence contradiction by A11,A12,A14,A22,A28,AFF_1:25;
end;
then consider c39 be Element of the AffinStruct of X such that
A143: c39 in A9 and
A144: LIN b39,e19,c39 by A130,AFF_1:59;
A145: b39,e19 // b39,c39 by A144,AFF_1:def 1;
consider e19 be Element of the AffinStruct of X such that
A146: c39,a39 // a29,e19 and
A147: a29<> e19 by DIRAF:40;
not a29,e19 // A9
proof
A148: c39<>o9
proof
assume c39=o9;
then
A149: a39,b29 // b39,o9 by A128,A129,A145,AFF_1:5;
b39,o9 // b39,b29 by A9,A11,A12,A22,AFF_1:39,41;
then a39,b29 // b39,b29 by A18,A149,AFF_1:5;
then b29,b39 // b29,a39 by AFF_1:4;
then LIN b29,b39,a39 by AFF_1:def 1;
hence contradiction by A11,A12,A14,A22,A28,AFF_1:25;
end;
assume
A150: a29,e19 // A9;
A151: o9,a39 // o9,a39 by AFF_1:2;
o9,c39 // A9 by A130,A131,A143,AFF_1:40,41;
then a29,e19 // o9,c39 by A130,A150,AFF_1:31;
then c39,a39 // o9,c39 by A146,A147,AFF_1:5;
then c39,o9 // c39,a39 by AFF_1:4;
then LIN c39,o9,a39 by AFF_1:def 1;
then a39 in A9 by A130,A131,A143,A148,AFF_1:25;
then A9 // M9 by A5,A8,A9,A14,A21,A130,A131,A151,AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23,A136,ANALMETR:52;
end;
then consider c29 be Element of the AffinStruct of X such that
A152: c29 in A9 and
A153: LIN a29,e19,c29 by A130,AFF_1:59;
reconsider c3=c39 as Element of X;
reconsider c2=c29 as Element of X;
a29,e19 // a29,c29 by A153,AFF_1:def 1;
then c39,a39 // a29,c29 by A146,A147,AFF_1:5;
then
A154: c3,a3 // a2,c2 by ANALMETR:36;
then
A155: a3,c3 // a2,c2 by ANALMETR:59;
consider e19 be Element of the AffinStruct of X such that
A156: c39,a39 // a19,e19 and
A157: a19<> e19 by DIRAF:40;
not a19,e19 // A9
proof
A158: c39<>o9
proof
assume c39=o9;
then
A159: a39,b29 // b39,o9 by A128,A129,A145,AFF_1:5;
b39,o9 // b39,b29 by A9,A11,A12,A22,AFF_1:39,41;
then a39,b29 // b39,b29 by A18,A159,AFF_1:5;
then b29,b39 // b29,a39 by AFF_1:4;
then LIN b29,b39,a39 by AFF_1:def 1;
hence contradiction by A11,A12,A14,A22,A28,AFF_1:25;
end;
assume
A160: a19,e19 // A9;
A161: o9,a39 // o9,a39 by AFF_1:2;
o9,c39 // A9 by A130,A131,A143,AFF_1:40,41;
then a19,e19 // o9,c39 by A130,A160,AFF_1:31;
then c39,a39 // o9,c39 by A156,A157,AFF_1:5;
then c39,o9 // c39,a39 by AFF_1:4;
then LIN c39,o9,a39 by AFF_1:def 1;
then a39 in A9 by A130,A131,A143,A158,AFF_1:25;
then A9 // M9 by A5,A8,A9,A14,A21,A130,A131,A161,AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23,A136,ANALMETR:52;
end;
then consider c19 be Element of the AffinStruct of X such that
A162: c19 in A9 and
A163: LIN a19,e19,c19 by A130,AFF_1:59;
reconsider c1=c19 as Element of X;
a19,e19 // a19,c19 by A163,AFF_1:def 1;
then c39,a39 // a19,c19 by A156,A157,AFF_1:5;
then
A164: c3,a3 // a1,c1 by ANALMETR:36;
then
A165: a3,c3 // a1,c1 by ANALMETR:59;
A166: a39,b29 // b39,c39 by A128,A129,A145,AFF_1:5;
A167: o<>c3 & o<>c2 & o<>c1
proof
A168: now
assume o=c3;
then
A169: a3,b2 // b3,o by A166,ANALMETR:36;
b39,o9 // b29,b39 by A9,A11,A12,A22,AFF_1:39,41;
then b3,o // b2,b3 by ANALMETR:36;
then a3,b2 // b2,b3 by A18,A169,ANALMETR:60;
then b2,b3 // b2,a3 by ANALMETR:59;
then LIN b2,b3,a3 by ANALMETR:def 10;
then LIN b29,b39,a39 by ANALMETR:40;
hence contradiction by A11,A12,A14,A22,A28,AFF_1:25;
end;
A170: now
a29,o9 // a29,a39 by A5,A7,A8,A21,AFF_1:39,41;
then
A171: a2,o // a2,a3 by ANALMETR:36;
assume o=c2 or o=c1;
then
A172: a3,c3 // a2,o or a3,c3 // a1,o by A154,A164,ANALMETR:59;
a19,o9 // a29,a39 by A5,A6,A7,A8,A21,AFF_1:39,41;
then a1,o // a2,a3 by ANALMETR:36;
then a3,c3 // a2, a3 by A15,A16,A172,A171,ANALMETR:60;
then a3,a2 // a3,c3 by ANALMETR:59;
then LIN a3,a2,c3 by ANALMETR:def 10;
then LIN a39,a29,c39 by ANALMETR:40;
then
A173: c39 in M9 by A7,A8,A21,A26,AFF_1:25;
o9,c39 // o9,c39 by AFF_1:2;
then A9 // M9 by A5,A21,A130,A131,A143,A168,A173,AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23,A136,ANALMETR:52;
end;
assume o=c3 or o=c2 or o=c1;
hence contradiction by A168,A170;
end;
A174: not c3 in N
proof
A175: o9,c39 // o9,c39 by AFF_1:2;
assume c3 in N;
then A9 // N9 by A9,A22,A130,A131,A143,A167,A175,AFF_1:38;
then A // N by ANALMETR:46;
hence contradiction by A136,ANALMETR:52;
end;
A176: not LIN a1,a2,c1
proof
assume LIN a1,a2,c1;
then LIN a19,a29,c19 by ANALMETR:40;
then
A177: c19 in M9 by A6,A7,A21,A25,AFF_1:25;
o9,c19 // o9,c19 by AFF_1:2;
then A9 // M9 by A5,A21,A130,A131,A162,A167,A177,AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23,A136,ANALMETR:52;
end;
A178: not LIN a3,a1,c3 & not LIN a3,a2,c3
proof
assume LIN a3,a1,c3 or LIN a3,a2,c3;
then LIN a39,a19,c39 or LIN a39,a29,c39 by ANALMETR:40;
then
A179: c39 in M9 or c39 in M9 by A6,A7,A8,A21,A26,A27,AFF_1:25;
o9,c39 // o9,c39 by AFF_1:2;
then A9 // M9 by A5,A21,A130,A131,A143,A167,A179,AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23,A136,ANALMETR:52;
end;
A180: not b2 in A
proof
A181: o9,b29 // o9,b29 by AFF_1:2;
assume b2 in A;
then A9 // N9 by A5,A9,A11,A13,A22,A130,A131,A181,AFF_1:38;
then A // N by ANALMETR:46;
hence contradiction by A136,ANALMETR:52;
end;
A182: not LIN c1,c2,b2
proof
A183: c19<>c29
proof
A184: a3<>c3
proof
A185: o9,c39 // o9,c39 by AFF_1:2;
assume a3=c3;
then A9 // M9 by A5,A8,A9,A14,A21,A130,A131,A143,A185,AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23,A136,ANALMETR:52;
end;
assume c19=c29;
then a2,c1 // a1,c1 by A155,A165,A184,ANALMETR:60;
then c1,a1 // c1,a2 by ANALMETR:59;
then LIN c1,a1,a2 by ANALMETR:def 10;
then LIN c19,a19,a29 by ANALMETR:40;
then LIN a19,a29,c19 by AFF_1:6;
then
A186: c19 in M9 by A6,A7,A21,A25,AFF_1:25;
o9,c19 // o9,c19 by AFF_1:2;
then A9 // M9 by A5,A21,A130,A131,A162,A167,A186,AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23,A136,ANALMETR:52;
end;
assume LIN c1,c2,b2;
then LIN c19,c29,b29 by ANALMETR:40;
hence contradiction by A130,A152,A162,A180,A183,AFF_1:25;
end;
o9,c19 // o9,c29 by A130,A131,A152,A162,AFF_1:39,41;
then LIN o9,c19,c29 by AFF_1:def 1;
then
A187: LIN o,c1,c2 by ANALMETR:40;
a3<>c3
proof
A188: o9,a39 // o9,a39 by AFF_1:2;
assume a3=c3;
then A9 // M9 by A5,A8,A9,A14,A21,A130,A131,A143,A188,AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23,A136,ANALMETR:52;
end;
then a2,c2 // a1,c1 by A155,A165,ANALMETR:60;
then
A189: c1,a1 // c2,a2 by ANALMETR:59;
o9,c39 // o9,c19 by A130,A131,A143,A162,AFF_1:39,41;
then LIN o9,c39,c19 by AFF_1:def 1;
then LIN o,c3,c1 by ANALMETR:40;
then b3,c3 // b1,c1 by A2,A9,A14,A15,A17,A18,A20,A165,A167,A121,A178
,A124,A123,CONAFFM:def 1;
then
A190: c3,b3 // c1,b1 by ANALMETR:59;
o9,c39 // o9,c29 by A130,A131,A143,A152,AFF_1:39,41;
then LIN o9,c39,c29 by AFF_1:def 1;
then LIN o,c3,c2 by ANALMETR:40;
then b2,c3 // b1,c2 by A2,A5,A9,A13,A14,A16,A17,A19,A155,A167,A121,A178
,A122,A119,CONAFFM:def 1;
then c3,b2 // c2,b1 by ANALMETR:59;
then c1,b2 // c2,b3 by A1,A9,A10,A11,A12,A17,A18,A131,A136,A143,A152
,A162,A167,A190,A180,A174;
hence thesis by A2,A5,A13,A15,A16,A18,A167,A118,A120,A187,A176,A182
,A189,CONAFFM:def 1;
end;
hence thesis by A40;
end;
A191: now
A192: not LIN o9,a39,b39
proof
assume LIN o9,a39,b39;
then LIN o9,b39,a39 by AFF_1:6;
hence contradiction by A9,A12,A14,A18,A22,AFF_1:25;
end;
o9,b39 // o9,b19 by A9,A10,A12,A22,AFF_1:39,41;
then
A193: LIN o9,b39,b19 by AFF_1:def 1;
assume
A194: a1=a3;
then a39,b39 // a39,b19 by A20,ANALMETR:36;
hence thesis by A19,A194,A192,A193,AFF_1:14;
end;
A195: now
o9,b29 // o9,b39 by A9,A11,A12,A22,AFF_1:39,41;
then
A196: LIN o9,b29,b39 by AFF_1:def 1;
assume
A197: a1=a2;
a1<>b1
proof
o9,a19 // o9,a39 by A5,A6,A8,A21,AFF_1:39,41;
then
A198: LIN o9,a19,a39 by AFF_1:def 1;
assume a1=b1;
hence contradiction by A9,A10,A14,A15,A22,A198,AFF_1:25;
end;
then a3,b2 // a3,b3 by A19,A20,A197,ANALMETR:60;
then a39,b29 // a39,b39 by ANALMETR:36;
then b29=b39 by A5,A8,A9,A13,A14,A21,A196,AFF_1:14,25;
then a19,b29 // a29,b39 by A197,AFF_1:2;
hence thesis by ANALMETR:36;
end;
now
o9,b29 // o9,b19 by A9,A10,A11,A22,AFF_1:39,41;
then
A199: LIN o9,b29,b19 by AFF_1:def 1;
assume
A200: a2=a3;
then a39,b29 // a39,b19 by A19,ANALMETR:36;
then b29=b19 by A5,A8,A9,A13,A14,A21,A199,AFF_1:14,25;
hence thesis by A20,A200,ANALMETR:59;
end;
hence thesis by A195,A191,A24;
end;
hence
thesis by A1,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,A15,A16,A17,A18,A19,A20;
end;
theorem
X is satisfying_MH1 & X is satisfying_MH2 implies X is satisfying_OPAP
proof
assume
A1: X is satisfying_MH1;
assume
A2: X is satisfying_MH2;
let o,a1,a2,a3,b1,b2,b3,M,N;
assume that
A3: o in M and
A4: a1 in M and
A5: a2 in M and
A6: a3 in M and
A7: o in N and
A8: b1 in N and
A9: b2 in N and
A10: b3 in N and
A11: not b2 in M and
A12: not a3 in N and
A13: M _|_ N and
A14: o<>a1 and
A15: o<>a2 and
o<>a3 and
A16: o<>b1 and
o<>b2 and
A17: o<>b3 and
A18: a3,b2 // a2,b1 and
A19: a3,b3 // a1,b1;
reconsider o9=o,a19=a1,a29=a2,a39=a3,b19=b1,b29=b2,b39=b3
as Element of the AffinStruct of X;
reconsider M9=M,N9=N as Subset of the AffinStruct of X;
N is being_line by A13,ANALMETR:44;
then
A20: N9 is being_line by ANALMETR:43;
M is being_line by A13,ANALMETR:44;
then
A21: M9 is being_line by ANALMETR:43;
A22: now
consider e1 be Element of X such that
A23: o,a3 // o,e1 and
A24: o<>e1 by ANALMETR:39;
consider d1 such that
A25: o,b3 // o,d1 and
A26: o<>d1 by ANALMETR:39;
reconsider d19=d1 as Element of the AffinStruct of X;
consider e2 be Element of X such that
A27: a1,b3 _|_ d1,e2 and
A28: d1<>e2 by ANALMETR:39;
reconsider e19=e1,e29=e2 as Element of the AffinStruct of X;
assume that
A29: a1<>a2 and
a2<>a3 and
A30: a1<>a3;
A31: LIN o,b3,d1 by A25,ANALMETR:def 10;
then
A32: LIN o9,b39,d19 by ANALMETR:40;
N is being_line by A13,ANALMETR:44;
then
A33: N9 is being_line by ANALMETR:43;
then
A34: o9,b29 // o9,b39 by A7,A9,A10,AFF_1:39,41;
then o,b2 // o,b3 by ANALMETR:36;
then
A35: LIN o,b2,b3 by ANALMETR:def 10;
A36: b2<>b3
proof
A37: not LIN o9,b19,a29
proof
o9,a29 // o9,a39 by A3,A5,A6,A21,AFF_1:39,41;
then
A38: LIN o9,a29,a39 by AFF_1:def 1;
assume LIN o9,b19,a29;
then a29 in N9 by A7,A8,A16,A20,AFF_1:25;
hence contradiction by A7,A12,A15,A20,A38,AFF_1:25;
end;
assume b2=b3;
then a1,b1 // a2,b1 by A6,A11,A18,A19,ANALMETR:60;
then b1,a2 // b1,a1 by ANALMETR:59;
then
A39: b19,a29 // b19,a19 by ANALMETR:36;
o9,a29 // o9,a19 by A3,A4,A5,A21,AFF_1:39,41;
then LIN o9,a29,a19 by AFF_1:def 1;
hence contradiction by A29,A37,A39,AFF_1:14;
end;
A40: not LIN b2,a3,b3
proof
assume LIN b2,a3,b3;
then LIN b29,a39,b39 by ANALMETR:40;
then LIN b29,b39,a39 by AFF_1:6;
hence contradiction by A9,A10,A12,A36,A33,AFF_1:25;
end;
A41: a3<>b3
proof
assume a3=b3;
then LIN b29,a39,b39 by AFF_1:7;
hence contradiction by A40,ANALMETR:40;
end;
b29,b39 // b29,b19 by A8,A9,A10,A33,AFF_1:39,41;
then b2,b3 // b2,b1 by ANALMETR:36;
then
A42: LIN b2,b3,b1 by ANALMETR:def 10;
M is being_line by A13,ANALMETR:44;
then
A43: M9 is being_line by ANALMETR:43;
then o9,a39 // o9,a19 by A3,A4,A6,AFF_1:39,41;
then
A44: o,a3 // o,a1 by ANALMETR:36;
then
A45: LIN o,a3,a1 by ANALMETR:def 10;
A46: not LIN a3,a1,b2
proof
assume LIN a3,a1,b2;
then LIN a39,a19,b29 by ANALMETR:40;
hence contradiction by A4,A6,A11,A30,A43,AFF_1:25;
end;
A47: a3<>b2
proof
assume a3=b2;
then LIN a39,a19,b29 by AFF_1:7;
hence contradiction by A46,ANALMETR:40;
end;
A48: o,a3 _|_ o,b3 by A3,A6,A7,A10,A13,ANALMETR:56;
not o,e1 // d1,e2
proof
reconsider e19=e1,e29=e2 as Element of the AffinStruct of X;
assume o,e1 // d1,e2;
then o9,e19 // d19,e29 by ANALMETR:36;
then d19,e29 // o9,e19 by AFF_1:4;
then d1,e2 // o,e1 by ANALMETR:36;
then o,e1 _|_ a1,b3 by A27,A28,ANALMETR:62;
then o,a3 _|_ a1,b3 by A23,A24,ANALMETR:62;
then o,b3 // a1,b3 by A7,A12,A48,ANALMETR:63;
then o9,b39 // a19,b39 by ANALMETR:36;
then b39,o9 // b39,a19 by AFF_1:4;
then LIN b39,o9,a19 by AFF_1:def 1;
then LIN o9,b39,a19 by AFF_1:6;
then
A49: o9,b39// o9,a19 by AFF_1:def 1;
LIN o9,b29,b39 by A35,ANALMETR:40;
then o9,b29 // o9,b39 by AFF_1:def 1;
then o9,b39 // o9,b29 by AFF_1:4;
then o9,a19 // o9,b29 by A17,A49,DIRAF:40;
then LIN o9,a19,b29 by AFF_1:def 1;
then LIN a19,o9,b29 by AFF_1:6;
then
A50: a19,o9 // a19,b29 by AFF_1:def 1;
LIN o9,a39,a19 by A45,ANALMETR:40;
then LIN a19,o9,a39 by AFF_1:6;
then a19,o9 // a19,a39 by AFF_1:def 1;
then a19,b29 // a19,a39 by A14,A50,DIRAF:40;
then LIN a19,b29,a39 by AFF_1:def 1;
then LIN a39,a19,b29 by AFF_1:6;
hence contradiction by A46,ANALMETR:40;
end;
then not o9,e19 // d19,e29 by ANALMETR:36;
then consider d29 be Element of the AffinStruct of X such that
A51: LIN o9,e19,d29 and
A52: LIN d19,e29,d29 by AFF_1:60;
reconsider d2=d29 as Element of X;
LIN d1,e2,d2 by A52,ANALMETR:40;
then
A53: d1,e2 // d1,d2 by ANALMETR:def 10;
then
A54: a1,b3 _|_ d1,d2 by A27,A28,ANALMETR:62;
then
A55: d1,d2 _|_ b3,a1 by ANALMETR:61;
LIN o,e1,d2 by A51,ANALMETR:40;
then o,e1 // o,d2 by ANALMETR:def 10;
then
A56: o,a3 // o,d2 by A23,A24,ANALMETR:60;
then
A57: LIN o,a3,d2 by ANALMETR:def 10;
then
A58: LIN o9,a39,d29 by ANALMETR:40;
consider e1 be Element of X such that
A59: o,b3 // o,e1 and
A60: o<>e1 by ANALMETR:39;
consider e2 be Element of X such that
A61: b3,a3 _|_ d2,e2 and
A62: d2<>e2 by ANALMETR:39;
reconsider e19=e1,e29=e2 as Element of the AffinStruct of X;
not o,e1 // d2,e2
proof
reconsider e19=e1,e29=e2 as Element of the AffinStruct of X;
assume o,e1 // d2,e2;
then o9,e19 // d29,e29 by ANALMETR:36;
then d29,e29 // o9,e19 by AFF_1:4;
then d2,e2 // o,e1 by ANALMETR:36;
then o,e1 _|_ b3,a3 by A61,A62,ANALMETR:62;
then o,b3 _|_ b3,a3 by A59,A60,ANALMETR:62;
then b3,a3 // o,a3 by A17,A48,ANALMETR:63;
then b39,a39 // o9,a39 by ANALMETR:36;
then a39,b39 // a39,o9 by AFF_1:4;
then LIN a39,b39,o9 by AFF_1:def 1;
then LIN b39,o9,a39 by AFF_1:6;
then
A63: b39,o9 // b39,a39 by AFF_1:def 1;
LIN o9,b29,b39 by A35,ANALMETR:40;
then LIN b39,o9,b29 by AFF_1:6;
then b39,o9 // b39,b29 by AFF_1:def 1;
then b39,a39 // b39,b29 by A17,A63,DIRAF:40;
then LIN b39,a39,b29 by AFF_1:def 1;
then LIN b29,a39,b39 by AFF_1:6;
hence contradiction by A40,ANALMETR:40;
end;
then not o9,e19 // d29,e29 by ANALMETR:36;
then consider d39 be Element of the AffinStruct of X such that
A64: LIN o9,e19,d39 and
A65: LIN d29,e29,d39 by AFF_1:60;
reconsider d3=d39 as Element of X;
LIN d2,e2,d3 by A65,ANALMETR:40;
then
A66: d2,e2 // d2,d3 by ANALMETR:def 10;
then
A67: b3,a3 _|_ d2,d3 by A61,A62,ANALMETR:62;
then d2,d3 _|_ a3,b3 by ANALMETR:61;
then
A68: d2,d3 _|_ a1,b1 by A19,A41,ANALMETR:62;
LIN o,e1,d3 by A64,ANALMETR:40;
then o,e1 // o,d3 by ANALMETR:def 10;
then
A69: o,b3 // o,d3 by A59,A60,ANALMETR:60;
then
A70: LIN o,b3,d3 by ANALMETR:def 10;
then
A71: LIN o9,b39,d39 by ANALMETR:40;
consider e2 be Element of X such that
A72: a3,b2 _|_ d3,e2 and
A73: d3<>e2 by ANALMETR:39;
consider e1 be Element of X such that
A74: o,a3 // o,e1 and
A75: o<>e1 by ANALMETR:39;
reconsider e19=e1,e29=e2 as Element of the AffinStruct of X;
not o,e1 // d3,e2
proof
reconsider e19=e1,e29=e2 as Element of the AffinStruct of X;
LIN o9,b29,b39 by A35,ANALMETR:40;
then LIN b29,o9,b39 by AFF_1:6;
then
A76: b29,o9 // b29,b39 by AFF_1:def 1;
assume o,e1 // d3,e2;
then o9,e19 // d39,e29 by ANALMETR:36;
then d39,e29 // o9,e19 by AFF_1:4;
then d3,e2 // o,e1 by ANALMETR:36;
then o,e1 _|_ a3,b2 by A72,A73,ANALMETR:62;
then o,a3 _|_ a3,b2 by A74,A75,ANALMETR:62;
then
A77: o,b3 // a3,b2 by A7,A12,A48,ANALMETR:63;
LIN o9,b29,b39 by A35,ANALMETR:40;
then LIN o9,b39,b29 by AFF_1:6;
then LIN o,b3,b2 by ANALMETR:40;
then o,b3 // o,b2 by ANALMETR:def 10;
then o,b2 // a3,b2 by A17,A77,ANALMETR:60;
then o9,b29 // a39,b29 by ANALMETR:36;
then b29,o9 // b29,a39 by AFF_1:4;
then b29,a39 // b29,b39 by A3,A11,A76,DIRAF:40;
then LIN b29,a39,b39 by AFF_1:def 1;
hence contradiction by A40,ANALMETR:40;
end;
then not o9,e19 // d39,e29 by ANALMETR:36;
then consider d49 be Element of the AffinStruct of X such that
A78: LIN o9,e19,d49 and
A79: LIN d39,e29,d49 by AFF_1:60;
reconsider d4=d49 as Element of X;
LIN d3,e2,d4 by A79,ANALMETR:40;
then
A80: d3,e2 // d3,d4 by ANALMETR:def 10;
then
A81: d3,d4 _|_ a3,b2 by A72,A73,ANALMETR:62;
LIN o,e1,d4 by A78,ANALMETR:40;
then o,e1 // o,d4 by ANALMETR:def 10;
then
A82: o,a3 // o,d4 by A74,A75,ANALMETR:60;
then
A83: LIN o,a3,d4 by ANALMETR:def 10;
then
A84: LIN o9,a39,d49 by ANALMETR:40;
A85: a3,b2 _|_ d3,d4 by A72,A73,A80,ANALMETR:62;
then d3,d4 _|_ a2,b1 or a3=b2 by A18,ANALMETR:62;
then
A86: d3,d4 _|_ b1,a2 by A47,ANALMETR:61;
A87: d2<>o
proof
o,a3 _|_ o,d1 by A17,A48,A25,ANALMETR:62;
then
A88: d1,o _|_ o,a3 by ANALMETR:61;
assume d2=o;
then d1,o _|_ a1,b3 by A27,A28,A53,ANALMETR:62;
then o,a3 // a1,b3 by A26,A88,ANALMETR:63;
then a1,b3 // o,a1 by A7,A12,A44,ANALMETR:60;
then a19,b39 // o9,a19 by ANALMETR:36;
then a19,b39 // a19,o9 by AFF_1:4;
then LIN a19,b39,o9 by AFF_1:def 1;
then LIN o9,b39,a19 by AFF_1:6;
then
A89: o9,b39 // o9,a19 by AFF_1:def 1;
LIN o9,b29,b39 by A35,ANALMETR:40;
then LIN o9,b39,b29 by AFF_1:6;
then o9,b39 // o9,b29 by AFF_1:def 1;
then o9,a19 // o9,b29 by A17,A89,DIRAF:40;
then LIN o9,a19,b29 by AFF_1:def 1;
then LIN a19,o9,b29 by AFF_1:6;
then
A90: a19,o9 // a19,b29 by AFF_1:def 1;
LIN o9,a39,a19 by A45,ANALMETR:40;
then LIN a19,o9,a39 by AFF_1:6;
then a19,o9 // a19,a39 by AFF_1:def 1;
then a19,b29 // a19,a39 by A14,A90,DIRAF:40;
then LIN a19,b29,a39 by AFF_1:def 1;
then LIN a39,a19,b29 by AFF_1:6;
hence contradiction by A46,ANALMETR:40;
end;
A91: not LIN d1,d2,d3
proof
A92: d2<>d3
proof
assume d2=d3;
then o9,b39 // o9,d29 by A69,ANALMETR:36;
then o9,d29 // o9,b39 by AFF_1:4;
then o,d2 // o,b3 by ANALMETR:36;
then o,b3 // o,a3 by A56,A87,ANALMETR:60;
then o9,b39 // o9,a39 by ANALMETR:36;
then LIN o9,b39,a39 by AFF_1:def 1;
then LIN b39,o9,a39 by AFF_1:6;
then b39,o9 // b39,a39 by AFF_1:def 1;
then
A93: b3,o // b3,a3 by ANALMETR:36;
LIN o9,b29,b39 by A35,ANALMETR:40;
then LIN b39,o9,b29 by AFF_1:6;
then b39,o9 // b39,b29 by AFF_1:def 1;
then b3,o // b3,b2 by ANALMETR:36;
then b3,b2 // b3,a3 by A17,A93,ANALMETR:60;
then LIN b3,b2,a3 by ANALMETR:def 10;
then LIN b39,b29,a39 by ANALMETR:40;
then LIN b29,a39,b39 by AFF_1:6;
hence contradiction by A40,ANALMETR:40;
end;
A94: d1<>d2
proof
assume d1=d2;
then o9,a39 // o9,d19 by A56,ANALMETR:36;
then o9,d19 // o9,a39 by AFF_1:4;
then o,d1 // o,a3 by ANALMETR:36;
then o,b3 // o,a3 by A25,A26,ANALMETR:60;
then o9,b39 // o9,a39 by ANALMETR:36;
then LIN o9,b39,a39 by AFF_1:def 1;
then LIN b39,o9,a39 by AFF_1:6;
then b39,o9 // b39,a39 by AFF_1:def 1;
then
A95: b3,o // b3,a3 by ANALMETR:36;
LIN o9,b29,b39 by A35,ANALMETR:40;
then LIN b39,o9,b29 by AFF_1:6;
then b39,o9 // b39,b29 by AFF_1:def 1;
then b3,o // b3,b2 by ANALMETR:36;
then b3,b2 // b3,a3 by A17,A95,ANALMETR:60;
then LIN b3,b2,a3 by ANALMETR:def 10;
then LIN b39,b29,a39 by ANALMETR:40;
then LIN b29,a39,b39 by AFF_1:6;
hence contradiction by A40,ANALMETR:40;
end;
assume LIN d1,d2,d3;
then LIN d19,d29,d39 by ANALMETR:40;
then LIN d29,d19,d39 by AFF_1:6;
then d29,d19 // d29,d39 by AFF_1:def 1;
then d19,d29 // d29,d39 by AFF_1:4;
then d1,d2 // d2,d3 by ANALMETR:36;
then d2,d3 _|_ a1,b3 by A54,A94,ANALMETR:62;
then a1,b3 // b3,a3 by A67,A92,ANALMETR:63;
then a19,b39 // b39,a39 by ANALMETR:36;
then b39,a19 // b39,a39 by AFF_1:4;
then LIN b39,a19,a39 by AFF_1:def 1;
then LIN a19,a39,b39 by AFF_1:6;
then a19,a39 // a19,b39 by AFF_1:def 1;
then
A96: a1,a3 // a1,b3 by ANALMETR:36;
A97: a1<>a3
proof
assume a1=a3;
then LIN a39,a19,b29 by AFF_1:7;
hence contradiction by A46,ANALMETR:40;
end;
LIN o9,a39,a19 by A45,ANALMETR:40;
then LIN a19,a39,o9 by AFF_1:6;
then a19,a39 // a19,o9 by AFF_1:def 1;
then a1,a3 // a1,o by ANALMETR:36;
then a1,o // a1,b3 by A97,A96,ANALMETR:60;
then LIN a1,o,b3 by ANALMETR:def 10;
then LIN a19,o9,b39 by ANALMETR:40;
then LIN o9,b39,a19 by AFF_1:6;
then
A98: o9,b39 // o9,a19 by AFF_1:def 1;
o9,b39 // o9,b29 by A34,AFF_1:4;
then o9,a19 // o9,b29 by A17,A98,DIRAF:40;
then LIN o9,a19,b29 by AFF_1:def 1;
then LIN a19,o9,b29 by AFF_1:6;
then a19,o9 // a19,b29 by AFF_1:def 1;
then
A99: a1,o // a1,b2 by ANALMETR:36;
LIN o9,a39,a19 by A45,ANALMETR:40;
then LIN a19,o9,a39 by AFF_1:6;
then a19,o9 // a19,a39 by AFF_1:def 1;
then a1,o // a1,a3 by ANALMETR:36;
then a1,b2 // a1,a3 by A14,A99,ANALMETR:60;
then LIN a1,b2,a3 by ANALMETR:def 10;
then LIN a19,b29,a39 by ANALMETR:40;
then LIN a39,a19,b29 by AFF_1:6;
hence contradiction by A46,ANALMETR:40;
end;
A100: d2<>d4
proof
A101: d2<>d3
proof
assume d2=d3;
then LIN d19,d29,d39 by AFF_1:7;
hence contradiction by A91,ANALMETR:40;
end;
assume d2=d4;
then a3,b2 _|_ d2,d3 by A85,ANALMETR:61;
then a3,b2 // b3,a3 by A67,A101,ANALMETR:63;
then a3,b2 // a3,b3 by ANALMETR:59;
then LIN a3,b2,b3 by ANALMETR:def 10;
then LIN a39,b29,b39 by ANALMETR:40;
then LIN b29,b39,a39 by AFF_1:6;
hence contradiction by A9,A10,A12,A20,A36,AFF_1:25;
end;
LIN o9,b39,b39 by AFF_1:7;
then
A102: LIN d19,d39,b39 by A17,A32,A71,AFF_1:8;
then consider A9 such that
A103: A9 is being_line and
A104: d19 in A9 and
A105: d39 in A9 and
A106: b39 in A9 by AFF_1:21;
reconsider A=A9 as Subset of X;
A107: d19<>d39
proof
assume d19=d39;
then LIN d19,d29,d39 by AFF_1:7;
hence contradiction by A91,ANALMETR:40;
end;
then A9=Line(d19,d39) by A103,A104,A105,AFF_1:24;
then
A108: A=Line(d1,d3) by ANALMETR:41;
LIN o9,b29,b39 by A35,ANALMETR:40;
then
A109: LIN o9,b39,b29 by AFF_1:6;
then
A110: b2 in A by A17,A32,A71,A103,A104,A105,A107,AFF_1:8,25;
A111: o<>d3
proof
assume d3=o;
then
A112: d2,o _|_ b3,a3 by A61,A62,A66,ANALMETR:62;
o,b3 _|_ o,d2 by A7,A12,A48,A56,ANALMETR:62;
then d2,o _|_ o,b3 by ANALMETR:61;
then o,b3 // b3,a3 by A87,A112,ANALMETR:63;
then o9,b39 // b39,a39 by ANALMETR:36;
then
A113: b39,o9 // b39,a39 by AFF_1:4;
LIN o9,b29,b39 by A35,ANALMETR:40;
then LIN b39,o9,b29 by AFF_1:6;
then b39,o9 // b39,b29 by AFF_1:def 1;
then b39,a39 // b39,b29 by A17,A113,DIRAF:40;
then LIN b39,a39,b29 by AFF_1:def 1;
then LIN b29,a39,b39 by AFF_1:6;
hence contradiction by A40,ANALMETR:40;
end;
A114: o<>d4
proof
o,a3 _|_ o,d3 by A17,A48,A69,ANALMETR:62;
then
A115: d3,o _|_ o,a3 by ANALMETR:61;
assume d4=o;
then d3,o _|_ a3,b2 by A72,A73,A80,ANALMETR:62;
then o,a3 // a3,b2 by A111,A115,ANALMETR:63;
then o9,a39 // a39,b29 by ANALMETR:36;
then
A116: a39,o9 // a39,b29 by AFF_1:4;
LIN o9,a39,a19 by A45,ANALMETR:40;
then LIN a39,o9,a19 by AFF_1:6;
then a39,o9 // a39,a19 by AFF_1:def 1;
then a39,b29 // a39,a19 by A7,A12,A116,DIRAF:40;
then LIN a39,b29,a19 by AFF_1:def 1;
then LIN a39,a19,b29 by AFF_1:6;
hence contradiction by A46,ANALMETR:40;
end;
A117: not LIN d1,d4,d3
proof
A118: d1<>d3
proof
A119: d1<>d2
proof
assume d1=d2;
then o9,a39 // o9,d19 by A56,ANALMETR:36;
then o9,d19 // o9,a39 by AFF_1:4;
then o,d1 // o,a3 by ANALMETR:36;
then o,b3 // o,a3 by A25,A26,ANALMETR:60;
then o9,b39 // o9,a39 by ANALMETR:36;
then LIN o9,b39,a39 by AFF_1:def 1;
then LIN b39,o9,a39 by AFF_1:6;
then b39,o9 // b39,a39 by AFF_1:def 1;
then
A120: b3,o // b3,a3 by ANALMETR:36;
LIN o9,b29,b39 by A35,ANALMETR:40;
then LIN b39,o9,b29 by AFF_1:6;
then b39,o9 // b39,b29 by AFF_1:def 1;
then b3,o // b3,b2 by ANALMETR:36;
then b3,b2 // b3,a3 by A17,A120,ANALMETR:60;
then LIN b3,b2,a3 by ANALMETR:def 10;
then LIN b39,b29,a39 by ANALMETR:40;
then LIN b29,a39,b39 by AFF_1:6;
hence contradiction by A40,ANALMETR:40;
end;
assume d1=d3;
then a3,b3 _|_ d1,d2 by A67,ANALMETR:61;
then a1,b3 // a3,b3 by A54,A119,ANALMETR:63;
then a19,b39 // a39,b39 by ANALMETR:36;
then b39,a19 // b39,a39 by AFF_1:4;
then LIN b39,a19,a39 by AFF_1:def 1;
then LIN a19,a39,b39 by AFF_1:6;
then a19,a39 // a19,b39 by AFF_1:def 1;
then
A121: a1,a3 // a1,b3 by ANALMETR:36;
A122: a1<>a3
proof
assume a1=a3;
then LIN a39,a19,b29 by AFF_1:7;
hence contradiction by A46,ANALMETR:40;
end;
LIN o9,a39,a19 by A45,ANALMETR:40;
then LIN a19,a39,o9 by AFF_1:6;
then a19,a39 // a19,o9 by AFF_1:def 1;
then a1,a3 // a1,o by ANALMETR:36;
then a1,o // a1,b3 by A122,A121,ANALMETR:60;
then LIN a1,o,b3 by ANALMETR:def 10;
then LIN a19,o9,b39 by ANALMETR:40;
then LIN o9,b39,a19 by AFF_1:6;
then
A123: o9,b39 // o9,a19 by AFF_1:def 1;
o9,b39 // o9,b29 by A34,AFF_1:4;
then o9,a19 // o9,b29 by A17,A123,DIRAF:40;
then LIN o9,a19,b29 by AFF_1:def 1;
then LIN a19,o9,b29 by AFF_1:6;
then a19,o9 // a19,b29 by AFF_1:def 1;
then
A124: a1,o // a1,b2 by ANALMETR:36;
LIN o9,a39,a19 by A45,ANALMETR:40;
then LIN a19,o9,a39 by AFF_1:6;
then a19,o9 // a19,a39 by AFF_1:def 1;
then a1,o // a1,a3 by ANALMETR:36;
then a1,b2 // a1,a3 by A14,A124,ANALMETR:60;
then LIN a1,b2,a3 by ANALMETR:def 10;
then LIN a19,b29,a39 by ANALMETR:40;
then LIN a39,a19,b29 by AFF_1:6;
hence contradiction by A46,ANALMETR:40;
end;
assume LIN d1,d4,d3;
then LIN d19,d49,d39 by ANALMETR:40;
then
A125: LIN d19,d39,d49 by AFF_1:6;
A126: b29<>b39
proof
assume b29=b39;
then LIN b29,a39,b39 by AFF_1:7;
hence contradiction by A40,ANALMETR:40;
end;
LIN o9,b29,b39 by A35,ANALMETR:40;
then LIN b29,b39,o9 by AFF_1:6;
then
A127: b29,b39 // b29,o9 by AFF_1:def 1;
LIN d19,d39,b29 by A17,A32,A71,A109,AFF_1:8;
then LIN b29,b39,d49 by A102,A118,A125,AFF_1:8;
then b29,b39 // b29,d49 by AFF_1:def 1;
then b29,o9 // b29,d49 by A127,A126,DIRAF:40;
then LIN b29,o9,d49 by AFF_1:def 1;
then LIN o9,d49,b29 by AFF_1:6;
then
A128: o9,d49 // o9,b29 by AFF_1:def 1;
o9,a39 // o9,d49 by A82,ANALMETR:36;
then o9,d49 // o9,a39 by AFF_1:4;
then o9,b29 // o9,a39 by A114,A128,DIRAF:40;
then LIN o9,b29,a39 by AFF_1:def 1;
then LIN b29,o9,a39 by AFF_1:6;
then
A129: b29,o9 // b29,a39 by AFF_1:def 1;
LIN o9,b29,b39 by A35,ANALMETR:40;
then LIN b29,o9,b39 by AFF_1:6;
then b29,o9 // b29,b39 by AFF_1:def 1;
then b29,a39 // b29,b39 by A3,A11,A129,DIRAF:40;
then LIN b29,a39,b39 by AFF_1:def 1;
hence contradiction by A40,ANALMETR:40;
end;
A130: not d4 in A
proof
assume d4 in A;
then d19,d49 // d19,d39 by A103,A104,A105,AFF_1:39,41;
then LIN d19,d49,d39 by AFF_1:def 1;
hence contradiction by A117,ANALMETR:40;
end;
A131: d2,d3 _|_ b3,a3 by A61,A62,A66,ANALMETR:62;
take d4;
LIN o9,b39,d19 by A31,ANALMETR:40;
then
A132: o9,b39 // o9,d19 by AFF_1:def 1;
LIN o9,a39,a19 by A45,ANALMETR:40;
then
A133: LIN d29,d49,a19 by A7,A12,A58,A84,AFF_1:8;
then consider K9 such that
A134: K9 is being_line and
A135: d29 in K9 and
A136: d49 in K9 and
A137: a19 in K9 by AFF_1:21;
reconsider K=K9 as Subset of X;
LIN o9,a39,a39 by AFF_1:7;
then
A138: a3 in K by A7,A12,A58,A84,A100,A134,A135,A136,AFF_1:8,25;
a39,a19 // a39,a29 by A4,A5,A6,A43,AFF_1:39,41;
then a3,a1 // a3,a2 by ANALMETR:36;
then
A139: LIN a3,a1,a2 by ANALMETR:def 10;
A140: LIN d1,d3,b3 & LIN d1,d3,b1 & LIN d2,d4,a1 & LIN d2,d4,a2
proof
A141: b39<>b29
proof
assume b39=b29;
then LIN b29,a39,b39 by AFF_1:7;
hence contradiction by A40,ANALMETR:40;
end;
LIN o9,b29,b39 by A35,ANALMETR:40;
then LIN b39,b29,o9 by AFF_1:6;
then
A142: b39,b29 // b39,o9 by AFF_1:def 1;
LIN b29,b39,b19 by A42,ANALMETR:40;
then LIN b39,b29,b19 by AFF_1:6;
then b39,b29 // b39,b19 by AFF_1:def 1;
then b39,b19 // b39,o9 by A142,A141,DIRAF:40;
then LIN b39,b19,o9 by AFF_1:def 1;
then
A143: LIN o9,b39,b19 by AFF_1:6;
A144: LIN o9,b39,d39 by A70,ANALMETR:40;
LIN o9,b39,d19 by A31,ANALMETR:40;
then
A145: LIN d19,d39,b19 by A17,A143,A144,AFF_1:8;
reconsider o9=o,a19=a1,a29=a2,a39=a3,d29=d2,d49=d4
as Element of the AffinStruct of X;
A146: a39<>a19
proof
assume a19=a39;
then LIN a39,a19,b29 by AFF_1:7;
hence contradiction by A46,ANALMETR:40;
end;
LIN o9,a39,a19 by A45,ANALMETR:40;
then LIN a39,a19,o9 by AFF_1:6;
then
A147: a39,a19 // a39,o9 by AFF_1:def 1;
LIN a39,a19,a29 by A139,ANALMETR:40;
then a39,a19 // a39,a29 by AFF_1:def 1;
then a39,a29 // a39,o9 by A147,A146,DIRAF:40;
then LIN a39,a29,o9 by AFF_1:def 1;
then
A148: LIN o9,a39,a29 by AFF_1:6;
A149: LIN o9,a39,d49 by A83,ANALMETR:40;
LIN o9,a39,d29 by A57,ANALMETR:40;
then LIN d29,d49,a29 by A7,A12,A148,A149,AFF_1:8;
hence thesis by A102,A133,A145,ANALMETR:40;
end;
LIN o9,b39,d39 by A70,ANALMETR:40;
then o9,b39 // o9,d39 by AFF_1:def 1;
then o9,d19 // o9,d39 by A17,A132,DIRAF:40;
then LIN o9,d19,d39 by AFF_1:def 1;
then LIN d19,o9,d39 by AFF_1:6;
then d19,o9 // d19,d39 by AFF_1:def 1;
then o9,d19 // d19,d39 by AFF_1:4;
then
A150: o,d1 // d1,d3 by ANALMETR:36;
o,b3 // o,d1 by A132,ANALMETR:36;
then o,d1 _|_ o,a3 by A17,A48,ANALMETR:62;
then
A151: o,a3 _|_ d1,d3 by A26,A150,ANALMETR:62;
LIN o9,a39,d29 by A57,ANALMETR:40;
then
A152: o9,a39 // o9,d29 by AFF_1:def 1;
then o,a3 // o,d2 by ANALMETR:36;
then
A153: o,d2 _|_ d1,d3 by A7,A12,A151,ANALMETR:62;
A154: not d2 in A
proof
assume d2 in A;
then d19,d29 // d19,d39 by A103,A104,A105,AFF_1:39,41;
then LIN d19,d29,d39 by AFF_1:def 1;
hence contradiction by A91,ANALMETR:40;
end;
LIN o9,a39,d49 by A83,ANALMETR:40;
then o9,a39 // o9,d49 by AFF_1:def 1;
then o9,d29 // o9,d49 by A7,A12,A152,DIRAF:40;
then LIN o9,d29,d49 by AFF_1:def 1;
then LIN d29,o9,d49 by AFF_1:6;
then d29,o9 // d29,d49 by AFF_1:def 1;
then o9,d29 // d29,d49 by AFF_1:4;
then o,d2 // d2,d4 by ANALMETR:36;
then
A155: d1,d3 _|_ d2,d4 by A87,A153,ANALMETR:62;
K9=Line(d29,d49) by A100,A134,A135,A136,AFF_1:24;
then K=Line(d2,d4) by ANALMETR:41;
then
A156: A _|_ K by A155,A100,A107,A108,ANALMETR:45;
reconsider d19=d1,d29=d2,d39=d3,d49=d4,b39=b3,a19=a1,b19=b1,a29=a2 as
Element of the AffinStruct of X;
LIN d19,d39,b39 by A140,ANALMETR:40;
then consider A9 such that
A157: A9 is being_line and
A158: d19 in A9 and
A159: d39 in A9 and
A160: b39 in A9 by AFF_1:21;
A161: d19<>d39
proof
assume d19=d39;
then LIN d19,d29,d39 by AFF_1:7;
hence contradiction by A91,ANALMETR:40;
end;
reconsider A=A9 as Subset of X;
LIN d19,d39,b19 by A140,ANALMETR:40;
then
A162: b1 in A by A157,A158,A159,A161,AFF_1:25;
A163: not d2 in A
proof
assume d2 in A;
then d19,d29 // d19,d39 by A157,A158,A159,AFF_1:39,41;
then d1,d2 // d1,d3 by ANALMETR:36;
hence contradiction by A91,ANALMETR:def 10;
end;
A164: d1<>d4
proof
LIN o9,a39,d49 by A83,ANALMETR:40;
then
A165: LIN o9,d49,a39 by AFF_1:6;
LIN o9,d49,o9 by AFF_1:7;
then
A166: o9,d49 // o9,a39 by A165,AFF_1:10;
A167: LIN o9,b39,o9 by AFF_1:7;
LIN o9,b29,b39 by A35,ANALMETR:40;
then
A168: LIN o9,b39,b29 by AFF_1:6;
LIN o9,b39,d19 by A31,ANALMETR:40;
then LIN o9,d19,b29 by A17,A167,A168,AFF_1:8;
then
A169: o9,d19 // o9,b29 by AFF_1:def 1;
assume d1=d4;
then o9,a39 // o9,b29 by A114,A169,A166,DIRAF:40;
then LIN o9,a39,b29 by AFF_1:def 1;
then LIN a39,b29,o9 by AFF_1:6;
then a39,b29 // a39,o9 by AFF_1:def 1;
then
A170: a39,o9 // a39,b29 by AFF_1:4;
LIN o9,a39,a19 by A45,ANALMETR:40;
then LIN a39,o9,a19 by AFF_1:6;
then a39,o9 // a39,a19 by AFF_1:def 1;
then a39,b29 // a39,a19 by A7,A12,A170,DIRAF:40;
then LIN a39,b29,a19 by AFF_1:def 1;
then LIN a39,a19,b29 by AFF_1:6;
hence contradiction by A46,ANALMETR:40;
end;
A171: not d4 in A
proof
assume d4 in A;
then d19,d49 // d19,d39 by A157,A158,A159,AFF_1:39,41;
then d1,d4 // d1,d3 by ANALMETR:36;
hence contradiction by A117,ANALMETR:def 10;
end;
LIN d29,d49,a19 by A140,ANALMETR:40;
then consider K9 such that
A172: K9 is being_line and
A173: d29 in K9 and
A174: d49 in K9 and
A175: a19 in K9 by AFF_1:21;
reconsider K=K9 as Subset of X;
LIN d29,d49,a29 by A140,ANALMETR:40;
then
A176: a2 in K by A100,A172,A173,A174,AFF_1:25;
K9=Line(d29,d49) by A100,A172,A173,A174,AFF_1:24;
then
A177: K=Line(d2,d4) by ANALMETR:41;
A9=Line(d19,d39) by A157,A158,A159,A161,AFF_1:24;
then A=Line(d1,d3) by ANALMETR:41;
then A _|_ K by A155,A100,A161,A177,ANALMETR:45;
then
A178: d1,d4 _|_ b3,a2 by A1,A68,A86,A55,A158,A159,A160,A173,A174,A175,A163,A171
,A162,A176;
d1,d2 _|_ a1,b3 by A27,A28,A53,ANALMETR:62;
then d1,d4 _|_ a1,b2 by A2,A131,A81,A104,A105,A106,A135,A136,A137,A154,A130
,A156,A110,A138;
then a1,b2 // b3,a2 or d1=d4 by A178,ANALMETR:63;
then a19,b29 // b39,a29 by A164,ANALMETR:36;
then a19,b29 // a29,b39 by AFF_1:4;
hence thesis by ANALMETR:36;
end;
now
A179: now
o9,b29 // o9,b39 by A7,A9,A10,A20,AFF_1:39,41;
then
A180: LIN o9,b29,b39 by AFF_1:def 1;
assume
A181: a1=a2;
a1<>b1
proof
o9,a19 // o9,a39 by A3,A4,A6,A21,AFF_1:39,41;
then
A182: LIN o9,a19,a39 by AFF_1:def 1;
assume a1=b1;
hence contradiction by A7,A8,A12,A14,A20,A182,AFF_1:25;
end;
then a3,b2 // a3,b3 by A18,A19,A181,ANALMETR:60;
then a39,b29 // a39,b39 by ANALMETR:36;
then b29=b39 by A3,A6,A7,A11,A12,A21,A180,AFF_1:14,25;
then a19,b29 // a29,b39 by A181,AFF_1:2;
hence thesis by ANALMETR:36;
end;
A183: now
A184: not LIN o9,a39,b19
proof
assume LIN o9,a39,b19;
then LIN o9,b19,a39 by AFF_1:6;
hence contradiction by A7,A8,A12,A16,A20,AFF_1:25;
end;
o9,b19 // o9,b39 by A7,A8,A10,A20,AFF_1:39,41;
then
A185: LIN o9,b19,b39 by AFF_1:def 1;
assume
A186: a1=a3;
then a3,b1 // a3,b3 by A19,ANALMETR:59;
then a39,b19 // a39,b39 by ANALMETR:36;
hence thesis by A18,A186,A184,A185,AFF_1:14;
end;
A187: now
A188: not LIN o9,a39,b19
proof
assume LIN o9,a39,b19;
then LIN o9,b19,a39 by AFF_1:6;
hence contradiction by A7,A8,A12,A16,A20,AFF_1:25;
end;
o9,b19 // o9,b29 by A7,A8,A9,A20,AFF_1:39,41;
then
A189: LIN o9,b19,b29 by AFF_1:def 1;
assume
A190: a2=a3;
then a3,b1 // a3,b2 by A18,ANALMETR:59;
then a39,b19 // a39,b29 by ANALMETR:36;
then a2,b3 // a1,b2 by A19,A190,A188,A189,AFF_1:14;
hence thesis by ANALMETR:59;
end;
assume a1=a2 or a2=a3 or a1=a3;
hence thesis by A179,A187,A183;
end;
hence thesis by A22;
end;
theorem
X is satisfying_3H implies X is satisfying_OPAP
proof
assume
A1: X is satisfying_3H;
let o,a1,a2,a3,b1,b2,b3,M,N;
assume that
A2: o in M and
A3: a1 in M and
A4: a2 in M and
A5: a3 in M and
A6: o in N and
A7: b1 in N and
A8: b2 in N and
A9: b3 in N and
A10: not b2 in M and
A11: not a3 in N and
A12: M _|_ N and
A13: o<>a1 and
A14: o<>a2 and
o<>a3 and
A15: o<>b1 and
o<>b2 and
A16: o<>b3 and
A17: a3,b2 // a2,b1 and
A18: a3,b3 // a1,b1;
reconsider o9=o,a19=a1,a29=a2,a39=a3,b19=b1,b29=b2,b39=b3
as Element of the AffinStruct of X;
reconsider M9=M,N9=N as Subset of the AffinStruct of X;
N is being_line by A12,ANALMETR:44;
then
A19: N9 is being_line by ANALMETR:43;
M is being_line by A12,ANALMETR:44;
then
A20: M9 is being_line by ANALMETR:43;
A21: now
A22: not LIN o9,b19,a19
proof
o9,a19 // o9,a39 by A2,A3,A5,A20,AFF_1:39,41;
then
A23: LIN o9,a19,a39 by AFF_1:def 1;
assume LIN o9,b19,a19;
then a19 in N9 by A6,A7,A15,A19,AFF_1:25;
hence contradiction by A6,A11,A13,A19,A23,AFF_1:25;
end;
A24: b1,a2 // a3,b2 by A17,ANALMETR:59;
o9,a19 // o9,a29 by A2,A3,A4,A20,AFF_1:39,41;
then
A25: LIN o9,a19,a29 by AFF_1:def 1;
assume
A26: b2=b3;
then b1,a1 // a3,b2 by A18,ANALMETR:59;
then b1,a1 // b1,a2 by A5,A10,A24,ANALMETR:60;
then b19,a19 // b19,a29 by ANALMETR:36;
then a19=a29 by A22,A25,AFF_1:14;
then a19,b29 // a29,b39 by A26,AFF_1:2;
hence thesis by ANALMETR:36;
end;
A27: LIN a,b,c implies LIN a,c,b & LIN b,a,c & LIN b,c,a & LIN c,a,b & LIN c
,b,a
proof
reconsider a9=a,b9=b,c9 = c as Element of the AffinStruct of X;
assume LIN a,b,c;
then
A28: LIN a9,b9,c9 by ANALMETR:40;
then
A29: LIN b9,a9,c9 by AFF_1:6;
A30: LIN c9,a9,b9 by A28,AFF_1:6;
A31: LIN b9,c9,a9 by A28,AFF_1:6;
A32: LIN c9,b9,a9 by A28,AFF_1:6;
LIN a9,c9,b9 by A28,AFF_1:6;
hence thesis by A29,A31,A30,A32,ANALMETR:40;
end;
A33: now
o9,a39 // o9,a19 by A2,A3,A5,A20,AFF_1:39,41;
then LIN o9,a39,a19 by AFF_1:def 1;
then
A34: LIN o,a3,a1 by ANALMETR:40;
a39,a19 // a39,a29 by A3,A4,A5,A20,AFF_1:39,41;
then LIN a39,a19,a29 by AFF_1:def 1;
then
A35: LIN a3,a1,a2 by ANALMETR:40;
o9,b29 // o9,b39 by A6,A8,A9,A19,AFF_1:39,41;
then LIN o9,b29,b39 by AFF_1:def 1;
then
A36: LIN o,b2,b3 by ANALMETR:40;
assume that
A37: a1<>a3 and
A38: b2<>b3;
A39: not LIN a3,a1,b2 & not LIN b2,a3,b3
proof
assume LIN a3,a1,b2 or LIN b2,a3,b3;
then LIN a39,a19,b29 or LIN b29,a39,b39 by ANALMETR:40;
then LIN a39,a19,b29 or LIN b29,b39,a39 by AFF_1:6;
hence contradiction by A3,A5,A8,A9,A10,A11,A20,A19,A37,A38,AFF_1:25;
end;
b29,b39 // b29,b19 by A7,A8,A9,A19,AFF_1:39,41;
then LIN b29,b39, b19 by AFF_1:def 1;
then
A40: LIN b2,b3,b1 by ANALMETR:40;
A41: now
assume
A42: b2<>b1;
not LIN a2,a3,b3
proof
A43: a3<>a2
proof
assume a3=a2;
then LIN a3,b2,b1 by A17,ANALMETR:def 10;
then LIN b2,b1,a3 by A27;
then
A44: b2,b1 // b2,a3 by ANALMETR:def 10;
LIN b2,b1,b3 by A27,A40;
then b2,b1 // b2,b3 by ANALMETR:def 10;
then b2,a3 // b2,b3 by A42,A44,ANALMETR:60;
hence contradiction by A39,ANALMETR:def 10;
end;
LIN a3,a1,o by A27,A34;
then
A45: a3,a1 // a3,o by ANALMETR:def 10;
A46: a3<>a1
proof
assume a3 = a1;
then LIN a39,a19,b29 by AFF_1:7;
hence contradiction by A39,ANALMETR:40;
end;
assume LIN a2,a3,b3;
then LIN a3,a2,b3 by A27;
then
A47: a3,a2 // a3,b3 by ANALMETR:def 10;
LIN a3,a2,a1 by A27,A35;
then a3,a2 // a3,a1 by ANALMETR:def 10;
then a3,a1 // a3,b3 by A47,A43,ANALMETR:60;
then a3,o // a3,b3 by A46,A45,ANALMETR:60;
then a39,o9 // a39,b39 by ANALMETR:36;
then
A48: a39,b39 // a39,o9 by AFF_1:4;
LIN b2,b3,o by A27,A36;
then
A49: LIN b29,b39,o9 by ANALMETR:40;
not LIN b29,a39,b39 by A39,ANALMETR:40;
hence contradiction by A16,A48,A49,AFF_1:14;
end;
then consider c1 such that
A50: c1,a2 _|_ a3,b3 and
A51: c1,a3 _|_ a2,b3 and
A52: c1,b3 _|_ a2,a3 by A1,CONAFFM:def 3;
reconsider c19 = c1 as Element of the AffinStruct of X;
A53: now
A54: a2<>a3
proof
A55: not LIN o9,a39,b19
proof
assume LIN o9,a39,b19;
then LIN o9,b19,a39 by AFF_1:6;
hence contradiction by A6,A7,A11,A15,A19,AFF_1:25;
end;
assume a2=a3;
then a39,b29 // a39,b19 by A17,ANALMETR:36;
then
A56: a39,b19 // a39,b29 by AFF_1:4;
o9,b19 // o9,b29 by A6,A7,A8,A19,AFF_1:39,41;
then LIN o9,b19,b29 by AFF_1:def 1;
hence contradiction by A42,A55,A56,AFF_1:14;
end;
a2,a3 _|_ b2,b3 by A4,A5,A8,A9,A12,ANALMETR:56;
then b2,b3 // c1,b3 by A52,A54,ANALMETR:63;
then b3,b2 // b3,c1 by ANALMETR:59;
then LIN b3,b2,c1 by ANALMETR:def 10;
then LIN b39,b29,c19 by ANALMETR:40;
then
A57: c1 in N by A8,A9,A19,A38,AFF_1:25;
A58: not LIN o9,a29,c19
proof
A59: o9<>c19
proof
assume
A60: o9=c19;
o,a2 _|_ b3,b2 by A2,A4,A8,A9,A12,ANALMETR:56;
then b3,b2 // a3,b3 by A14,A50,A60,ANALMETR:63;
then b3,b2 // b3,a3 by ANALMETR:59;
then LIN b3,b2,a3 by ANALMETR:def 10;
then LIN b39,b29,a39 by ANALMETR:40;
hence contradiction by A8,A9,A11,A19,A38,AFF_1:25;
end;
o9,a29 // o9,a39 by A2,A4,A5,A20,AFF_1:39,41;
then
A61: LIN o9,a29,a39 by AFF_1:def 1;
assume LIN o9,a29,c19;
then LIN o9,c19,a29 by AFF_1:6;
then a29 in N9 by A6,A19,A57,A59,AFF_1:25;
hence contradiction by A6,A11,A14,A19,A61,AFF_1:25;
end;
A62: a1<>b1
proof
o9,b19 // o9,b29 by A6,A7,A8,A19,AFF_1:39,41;
then
A63: LIN o9,b19,b29 by AFF_1:def 1;
assume a1=b1;
hence contradiction by A2,A3,A10,A13,A20,A63,AFF_1:25;
end;
assume
A64: a2<>a1;
A65: a1<>b1
proof
LIN a1,a2,a3 by A27,A35;
then a1,a2 // a1,a3 by ANALMETR:def 10;
then
A66: a2,a1 // a3,a1 by ANALMETR:59;
assume a1=b1;
then a3,a1 // a3,b2 by A17,A64,A66,ANALMETR:60;
hence contradiction by A39,ANALMETR:def 10;
end;
not LIN a2,a1,b1
proof
assume LIN a2,a1,b1;
then LIN b1,a1,a2 by A27;
then b1,a1 // b1,a2 by ANALMETR:def 10;
then a1,b1 // a2,b1 by ANALMETR:59;
then
A67: a2,b1 // a3,b3 by A18,A65,ANALMETR:60;
a2<>b1
proof
o9,b19 // o9,b29 by A6,A7,A8,A19,AFF_1:39,41;
then
A68: LIN o9,b19,b29 by AFF_1:def 1;
assume a2=b1;
hence contradiction by A2,A4,A10,A14,A20,A68,AFF_1:25;
end;
then a3,b3 // a3,b2 by A17,A67,ANALMETR:60;
then LIN a3,b3,b2 by ANALMETR:def 10;
hence contradiction by A27,A39;
end;
then consider c2 such that
A69: c2,a2 _|_ a1,b1 and
A70: c2,a1 _|_ a2,b1 and
A71: c2,b1 _|_ a2,a1 by A1,CONAFFM:def 3;
reconsider c29 = c2 as Element of the AffinStruct of X;
a1,b1 _|_ c1,a2 by A9,A11,A18,A50,ANALMETR:62;
then c2,a2 // c1,a2 by A69,A62,ANALMETR:63;
then a2,c1 // a2,c2 by ANALMETR:59;
then
A72: a29,c19 // a29,c29 by ANALMETR:36;
a2,a1 _|_ b1,b2 by A3,A4,A7,A8,A12,ANALMETR:56;
then b1,b2 // c2,b1 by A64,A71,ANALMETR:63;
then b1,b2 // b1,c2 by ANALMETR:59;
then LIN b1,b2,c2 by ANALMETR:def 10;
then LIN b19,b29,c29 by ANALMETR:40;
then
A73: c29 in N9 by A7,A8,A19,A42,AFF_1:25;
A74: not LIN o9,a19,c29
proof
A75: o9<>c29
proof
A76: a2<>b1
proof
o9,b19 // o9,b29 by A6,A7,A8,A19,AFF_1:39,41;
then
A77: LIN o9,b19,b29 by AFF_1:def 1;
assume a2=b1;
hence contradiction by A2,A4,A10,A14,A20,A77,AFF_1:25;
end;
assume o9=c29;
then
A78: o,a1 _|_ a3,b2 by A17,A70,A76,ANALMETR:62;
o,a1 _|_ b3,b2 by A2,A3,A8,A9,A12,ANALMETR:56;
then b3,b2 // a3,b2 by A13,A78,ANALMETR:63;
then b2,b3 // b2,a3 by ANALMETR:59;
then LIN b2,b3,a3 by ANALMETR:def 10;
then LIN b29,b39,a39 by ANALMETR:40;
hence contradiction by A8,A9,A11,A19,A38,AFF_1:25;
end;
o9,a19 // o9,a39 by A2,A3,A5,A20,AFF_1:39,41;
then
A79: LIN o9,a19,a39 by AFF_1:def 1;
assume LIN o9,a19,c29;
then LIN o9,c29,a19 by AFF_1:6;
then a19 in N9 by A6,A19,A73,A75,AFF_1:25;
hence contradiction by A6,A11,A13,A19,A79,AFF_1:25;
end;
not LIN a3,a1,b2
proof
assume LIN a3,a1,b2;
then LIN a39,a19,b29 by ANALMETR:40;
hence contradiction by A3,A5,A10,A20,A37,AFF_1:25;
end;
then consider c3 such that
A80: c3,a3 _|_ a1,b2 and
A81: c3,a1 _|_ a3,b2 and
A82: c3,b2 _|_ a3,a1 by A1,CONAFFM:def 3;
reconsider c39 = c3 as Element of the AffinStruct of X;
a2<>b1
proof
o9,b19 // o9,b29 by A6,A7,A8,A19,AFF_1:39,41;
then
A83: LIN o9,b19,b29 by AFF_1:def 1;
assume a2=b1;
hence contradiction by A2,A4,A10,A14,A20,A83,AFF_1:25;
end;
then a3,b2 _|_ c2,a1 by A17,A70,ANALMETR:62;
then c2,a1 // c3,a1 by A5,A10,A81,ANALMETR:63;
then a1,c2 // a1,c3 by ANALMETR:59;
then
A84: a19,c29 // a19,c39 by ANALMETR:36;
a2,a1 _|_ b2,b1 by A3,A4,A7,A8,A12,ANALMETR:56;
then b2,b1 // c2,b1 by A64,A71,ANALMETR:63;
then b1,b2 // b1,c2 by ANALMETR:59;
then LIN b1,b2,c2 by ANALMETR:def 10;
then LIN b19,b29,c29 by ANALMETR:40;
then c2 in N by A7,A8,A19,A42,AFF_1:25;
then o9,c19 // o9,c29 by A6,A19,A57,AFF_1:39,41;
then LIN o9,c19,c29 by AFF_1:def 1;
then
A85: c1 = c2 by A58,A72,AFF_1:14;
A86: c1<>a3
proof
A87: a2<>a3
proof
A88: not LIN o9,a39,b19
proof
assume LIN o9,a39,b19;
then LIN o9,b19,a39 by AFF_1:6;
hence contradiction by A6,A7,A11,A15,A19,AFF_1:25;
end;
assume a2=a3;
then a39,b29 // a39,b19 by A17,ANALMETR:36;
then
A89: a39,b19 // a39,b29 by AFF_1:4;
o9,b19 // o9,b29 by A6,A7,A8,A19,AFF_1:39,41;
then LIN o9,b19,b29 by AFF_1:def 1;
hence contradiction by A42,A88,A89,AFF_1:14;
end;
assume
A90: c1=a3;
a2,a3 _|_ b2,b3 by A4,A5,A8,A9,A12,ANALMETR:56;
then a3,b3 // b2,b3 by A52,A90,A87,ANALMETR:63;
then b3,b2 // b3,a3 by ANALMETR:59;
then LIN b3,b2,a3 by ANALMETR:def 10;
then LIN b39,b29,a39 by ANALMETR:40;
hence contradiction by A8,A9,A11,A19,A38,AFF_1:25;
end;
a3,a1 _|_ b2,b3 by A3,A5,A8,A9,A12,ANALMETR:56;
then c3,b2 // b2,b3 by A37,A82,ANALMETR:63;
then b2,b3 // b2,c3 by ANALMETR:59;
then LIN b2,b3,c3 by ANALMETR:def 10;
then LIN b29,b39,c39 by ANALMETR:40;
then c39 in N9 by A8,A9,A19,A38,AFF_1:25;
then o9,c29 // o9,c39 by A6,A19,A73,AFF_1:39,41;
then LIN o9,c29,c39 by AFF_1:def 1;
then c2 = c3 by A74,A84,AFF_1:14;
hence thesis by A51,A85,A80,A86,ANALMETR:63;
end;
now
o9,b29 // o9,b39 by A6,A8,A9,A19,AFF_1:39,41;
then
A91: LIN o9,b29,b39 by AFF_1:def 1;
assume
A92: a2=a1;
a1<>b1
proof
o9,b19 // o9,b29 by A6,A7,A8,A19,AFF_1:39,41;
then
A93: LIN o9,b19,b29 by AFF_1:def 1;
assume a1=b1;
hence contradiction by A2,A3,A10,A13,A20,A93,AFF_1:25;
end;
then a3,b2 // a3,b3 by A17,A18,A92,ANALMETR:60;
then a39,b29 // a39,b39 by ANALMETR:36;
then b29=b39 by A2,A5,A6,A10,A11,A20,A91,AFF_1:14,25;
then a19,b29 // a29,b39 by A92,AFF_1:2;
hence thesis by ANALMETR:36;
end;
hence thesis by A53;
end;
now
A94: not LIN o9,b29,a39
proof
assume LIN o9,b29,a39;
then LIN o,b2,a3 by ANALMETR:40;
then LIN b2,o,a3 by A27;
then
A95: b2,o // b2,a3 by ANALMETR:def 10;
LIN b2,o,b3 by A27,A36;
then b2,o // b2,b3 by ANALMETR:def 10;
then b2,a3 // b2,b3 by A2,A10,A95,ANALMETR:60;
hence contradiction by A39,ANALMETR:def 10;
end;
LIN a3,a1,o by A27,A34;
then
A96: a3,a1 // a3,o by ANALMETR:def 10;
A97: a3<>a1
proof
assume a3=a1;
then LIN a39,a19,b29 by AFF_1:7;
hence contradiction by A39,ANALMETR:40;
end;
a3,a1 // a3,a2 by A35,ANALMETR:def 10;
then a3,o // a3,a2 by A96,A97,ANALMETR:60;
then LIN a3,o,a2 by ANALMETR:def 10;
then LIN o,a3,a2 by A27;
then
A98: LIN o9,a39,a29 by ANALMETR:40;
assume
A99: b2=b1;
then b2,a3 // b2,a2 by A17,ANALMETR:59;
then b29,a39 // b29,a29 by ANALMETR:36;
then a39=a29 by A98,A94,AFF_1:14;
hence thesis by A18,A99,ANALMETR:59;
end;
hence thesis by A41;
end;
now
A100: not LIN o9,a19,b19
proof
o9,b19 // o9,b29 by A6,A7,A8,A19,AFF_1:39,41;
then
A101: LIN o9,b19,b29 by AFF_1:def 1;
assume LIN o9,a19,b19;
then b19 in M9 by A2,A3,A13,A20,AFF_1:25;
hence contradiction by A2,A10,A15,A20,A101,AFF_1:25;
end;
o9,b19 // o9,b39 by A6,A7,A9,A19,AFF_1:39,41;
then
A102: LIN o9,b19,b39 by AFF_1:def 1;
assume
A103: a1=a3;
then a1,b1 // a1,b3 by A18,ANALMETR:59;
then a19,b19 // a19,b39 by ANALMETR:36;
hence thesis by A17,A103,A100,A102,AFF_1:14;
end;
hence thesis by A21,A33;
end;