:: Metric-Affine Configurations in Metric Affine Planes - Part II :: by Jolanta \'Swierzy\'nska and Bogdan \'Swierzy\'nski :: :: Received October 31, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies 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; 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 Af(X); reserve A,K,M,N for Subset of X; reserve A9,K9 for Subset of Af(X); definition let X; attr X is satisfying_OPAP means :Def1: 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 :Def3: 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 :Def4: 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 :Def5: 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 :Def7: 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 :Def8: 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 Af(X) by ANALMETR:35; 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 Af(X) by ANALMETR:35; LIN p9,q9,r9 by A1,ANALMETR:40; then consider c9 being Element of Af(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 by ANALMETR:35; 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 Af(X) by ANALMETR:35; 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 Af(X) by ANALMETR:35; reconsider A9=A as Subset of Af(X) by ANALMETR:42; 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 Af X by ANALMETR:42; 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 Af(X), c9,d9 being Element of Af(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 Af(X),c9,d9 be Element of Af(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 Af(X) by ANALMETR:35; 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 Af(X) is Moufangian proof assume A1: X is satisfying_TDES; let K9 be Subset of Af(X); let o9,a9,b9,c9,a19,b19,c19 be Element of Af(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 by ANALMETR:42; reconsider o=o9,a=a9,a1=a19,b=b9,b1=b19,c =c9,c1=c19 as Element of X by ANALMETR:35; 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,Def5; 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: Af(X) is translational implies X is satisfying_des proof assume A1: Af(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 Af(X) by ANALMETR:35; LIN a9,a19,a19 by AFF_1:7; then consider A9 be Subset of Af(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 Af(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 Af(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 ,AFF_2:def 11; 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 Af(X) by ANALMETR:42; 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 Af(X) by ANALMETR:35; 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 Af 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 Af(X) by ANALMETR:35; A25: now assume A26: b2<>b4; A27: now consider e19 be Element of Af(X) such that A28: o9<>e19 and A29: e19 in M9 by A22,AFF_1:20; reconsider e1=e19 as Element of X by ANALMETR:35; ex d49 be Element of Af(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 Af(X) by ANALMETR:35; consider e2 such that A32: a1,a4 _|_ d4,e2 and A33: e2<>d4 by ANALMETR:39; reconsider e29=e2 as Element of Af(X) by ANALMETR:35; 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 Af(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 by ANALMETR:35; consider e19 be Element of Af(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 by ANALMETR:35; consider e2 such that A46: a2,a1 _|_ d1,e2 and A47: e2<>d1 by ANALMETR:39; reconsider e29=e2 as Element of Af(X) by ANALMETR:35; 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 Af(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 by ANALMETR:35; 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 Af(X) such that A59: o9<>e19 and A60: e19 in M9 by A22,AFF_1:20; reconsider e1=e19 as Element of X by ANALMETR:35; consider e2 such that A61: a3,a2 _|_ d2,e2 and A62: e2<>d2 by ANALMETR:39; reconsider e29=e2 as Element of Af(X) by ANALMETR:35; 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 Af(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 by ANALMETR:35; 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 ,Def3; 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 ,Def3; hence thesis by A68,A71,ANALMETR:63; end; now A72: not LIN o9,a29,a19 proof assume LIN o9,a29,a19; then o9,a29 // o9,a19 by AFF_1:def 1; hence contradiction by A7,A12,A15,A21,A23,A24,AFF_1:48; end; 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 Af(X) by ANALMETR:42; 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 Af(X) by ANALMETR:35; 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 Af(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 Af(X) by ANALMETR:35; A25: now assume A26: b2<>b4; A27: now ex d39 be Element of Af(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 Af(X) by ANALMETR:35; 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 Af(X) by ANALMETR:35; 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 Af(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 by ANALMETR:35; 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 Af(X) by ANALMETR:35; 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 Af(X) by ANALMETR:35; 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 Af(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 by ANALMETR:35; 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 Af(X) by ANALMETR:35; 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 Af(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 by ANALMETR:35; 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 ,Def4; a3,a4 _|_ d3,d4 by A1,A2,A3,A4,A7,A8,A11,A12,A28,A40,A41,A50,A51,A60,A62 ,Def4; 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 Af(X) by ANALMETR:35; 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 by ANALMETR:35; 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 Af(X) by ANALMETR:35; 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 by ANALMETR:35; 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 Af(X) by ANALMETR:35; 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 by ANALMETR:35; 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 Af(X) by ANALMETR:35; reconsider M9=M,N9=N as Subset of Af(X) by ANALMETR:42; 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 Af(X) by ANALMETR:35; 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 Af(X) by ANALMETR:35; 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 Af(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 by ANALMETR:35; 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 Af(X) is Moufangian by Th7; then Af(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,Def8; 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,Def8; hence thesis by A2,A77,A82,A65,A70,A79,A80,Def8; end; now assume not M // N; then not M9 // N9 by ANALMETR:46; then consider o9 being Element of Af 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 by ANALMETR:35; consider K such that A85: o in K and A86: N _|_ K by A4,Th3; reconsider K9=K as Subset of Af(X) by ANALMETR:42; 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 Af(X); consider D9 being Subset of Af(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 by ANALMETR:42; 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 Af(X) by ANALMETR:35; take y9; thus y9 in K9 & x9,y9 // N9 by A99,A100,A101,A102,AFF_1:40; end; then consider d19 be Element of Af(X) such that A103: d19 in K9 and A104: a19,d19 // N9; consider e19 be Element of Af(X) such that A105: e19 in K9 and A106: b19,e19 // N9 by A98; consider d39 be Element of Af(X) such that A107: d39 in K9 and A108: a39,d39 // N9 by A98; consider e39 be Element of Af(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 by ANALMETR:35 ; 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 Af(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,Def5; 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,Def5; 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,Def5; then d3,a4 // e3,b4 by A1,A9,A10,A11,A12,A86,A103,A107,A109,A105,A131 ,A134,A136,A120,A119,A132,A89,Def7; hence thesis by A2,A13,A16,A18,A20,A83,A84,A112,A130,A95,A133,A125,A127 ,A135,Def5; 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,Def7; 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 Af(X ) by ANALMETR:35; reconsider M9=M,N9=N as Subset of Af(X) by ANALMETR:42; 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 Af(X) such that A48: a39,b39 // b29,e19 and A49: b29<> e19 by DIRAF:40; reconsider x9=x as Element of Af(X) by ANALMETR:35; LIN o9,x9,x9 by AFF_1:7; then consider A9 be Subset of Af(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 by ANALMETR:42; 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 Af(X) by ANALMETR:35; 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 Af(X) by ANALMETR:35; 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 Af(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 by ANALMETR:35; 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 Af(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 Af(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 Af(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 by ANALMETR:35; reconsider c3=c39 as Element of X by ANALMETR:35; 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 Af(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 Af(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 by ANALMETR:35; 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,Def1; 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 Af(X) such that A128: a39,b29 // b39,e19 and A129: b39<> e19 by DIRAF:40; reconsider x9=x as Element of Af(X) by ANALMETR:35; LIN o9,x9,x9 by AFF_1:7; then consider A9 be Subset of Af(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 by ANALMETR:42; 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 Af(X) by ANALMETR:35; 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 Af(X) by ANALMETR:35; 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 Af(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 by ANALMETR:35; 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 Af(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 Af(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 Af(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 by ANALMETR:35; reconsider c2=c29 as Element of X by ANALMETR:35; 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 Af(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 Af(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 by ANALMETR:35; 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,Def1; 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,Def1; 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 Af(X ) by ANALMETR:35; reconsider M9=M,N9=N as Subset of Af(X) by ANALMETR:42; 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 Af(X) by ANALMETR:35; 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 Af(X) by ANALMETR:35; 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 Af(X) by ANALMETR:35; 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 Af(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 by ANALMETR:35; 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 Af(X) by ANALMETR:35; not o,e1 // d2,e2 proof reconsider e19=e1,e29=e2 as Element of Af(X) by ANALMETR:35; 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 Af(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 by ANALMETR:35; 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 Af(X) by ANALMETR:35; not o,e1 // d3,e2 proof reconsider e19=e1,e29=e2 as Element of Af(X) by ANALMETR:35; 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 Af(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 by ANALMETR:35; 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 by ANALMETR:42; 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 by ANALMETR:42; 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 Af(X) by ANALMETR:35; 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 Af(X) by ANALMETR:35; 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 by ANALMETR:42; 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 by ANALMETR:42; 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,Def3; 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,Def4; 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 Af(X ) by ANALMETR:35; reconsider M9=M,N9=N as Subset of Af(X) by ANALMETR:42; 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 Af(X) by ANALMETR:35; 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 Af(X) by ANALMETR:35; 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 Af(X) by ANALMETR:35; 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 Af(X) by ANALMETR:35; 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;