:: CONMETR semantic presentation begin definition let X be OrtAfPl; attrX is satisfying_OPAP means :Def1: :: CONMETR:def 1 for o, a1, a2, a3, b1, b2, b3 being Element of X for M, N being Subset of X 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; attrX is satisfying_PAP means :: CONMETR:def 2 for o, a1, a2, a3, b1, b2, b3 being Element of X for M, N being Subset of X 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; attrX is satisfying_MH1 means :Def3: :: CONMETR:def 3 for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X 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; attrX is satisfying_MH2 means :Def4: :: CONMETR:def 4 for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X 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; attrX is satisfying_TDES means :Def5: :: CONMETR:def 5 for o, a, a1, b, b1, c, c1 being Element of X 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; attrX is satisfying_SCH means :: CONMETR:def 6 for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X 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; attrX is satisfying_OSCH means :Def7: :: CONMETR:def 7 for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X 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; attrX is satisfying_des means :Def8: :: CONMETR:def 8 for a, a1, b, b1, c, c1 being Element of X 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; :: deftheorem Def1 defines satisfying_OPAP CONMETR:def_1_:_ for X being OrtAfPl holds ( X is satisfying_OPAP iff for o, a1, a2, a3, b1, b2, b3 being Element of X for M, N being Subset of X 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 ); :: deftheorem defines satisfying_PAP CONMETR:def_2_:_ for X being OrtAfPl holds ( X is satisfying_PAP iff for o, a1, a2, a3, b1, b2, b3 being Element of X for M, N being Subset of X 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 ); :: deftheorem Def3 defines satisfying_MH1 CONMETR:def_3_:_ for X being OrtAfPl holds ( X is satisfying_MH1 iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X 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 ); :: deftheorem Def4 defines satisfying_MH2 CONMETR:def_4_:_ for X being OrtAfPl holds ( X is satisfying_MH2 iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X 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 ); :: deftheorem Def5 defines satisfying_TDES CONMETR:def_5_:_ for X being OrtAfPl holds ( X is satisfying_TDES iff for o, a, a1, b, b1, c, c1 being Element of X 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 ); :: deftheorem defines satisfying_SCH CONMETR:def_6_:_ for X being OrtAfPl holds ( X is satisfying_SCH iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X 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 ); :: deftheorem Def7 defines satisfying_OSCH CONMETR:def_7_:_ for X being OrtAfPl holds ( X is satisfying_OSCH iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X 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 ); :: deftheorem Def8 defines satisfying_des CONMETR:def_8_:_ for X being OrtAfPl holds ( X is satisfying_des iff for a, a1, b, b1, c, c1 being Element of X 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 ); theorem Th1: :: CONMETR:1 for X being OrtAfPl ex a, b, c being Element of X st ( LIN a,b,c & a <> b & b <> c & c <> a ) proof let X be OrtAfPl; ::_thesis: ex a, b, c being Element of X st ( LIN a,b,c & a <> b & b <> c & c <> a ) consider a, p being Element of X such that A1: a <> p by ANALMETR:39; consider b being Element of X 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 being Element of X such that A4: p,c _|_ a,b and A5: LIN a,b,c by ANALMETR:69; take a ; ::_thesis: ex b, c being Element of X st ( LIN a,b,c & a <> b & b <> c & c <> a ) take b ; ::_thesis: ex c being Element of X st ( LIN a,b,c & a <> b & b <> c & c <> a ) take c ; ::_thesis: ( LIN a,b,c & a <> b & b <> c & c <> a ) thus LIN a,b,c by A5; ::_thesis: ( a <> b & b <> c & c <> a ) thus a <> b ::_thesis: ( b <> c & c <> a ) proof assume not a <> b ; ::_thesis: contradiction then a,p _|_ a,p by A2, ANALMETR:61; hence contradiction by A1, ANALMETR:39; ::_thesis: verum end; thus b <> c ::_thesis: c <> a proof assume not b <> c ; ::_thesis: contradiction 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; ::_thesis: verum end; assume not c <> a ; ::_thesis: contradiction 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; ::_thesis: verum end; theorem Th2: :: CONMETR:2 for X being OrtAfPl for a, b being Element of X ex c being Element of X st ( LIN a,b,c & a <> c & b <> c ) proof let X be OrtAfPl; ::_thesis: for a, b being Element of X ex c being Element of X st ( LIN a,b,c & a <> c & b <> c ) let a, b be Element of X; ::_thesis: ex c being Element of X st ( LIN a,b,c & a <> c & b <> c ) 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 ex c being Element of X st ( LIN a,b,c & a <> c & b <> c ) by A6, A7; ::_thesis: verum end; theorem Th3: :: CONMETR:3 for X being OrtAfPl for A being Subset of X for a being Element of X st A is being_line holds ex K being Subset of X st ( a in K & A _|_ K ) proof let X be OrtAfPl; ::_thesis: for A being Subset of X for a being Element of X st A is being_line holds ex K being Subset of X st ( a in K & A _|_ K ) let A be Subset of X; ::_thesis: for a being Element of X st A is being_line holds ex K being Subset of X st ( a in K & A _|_ K ) let a be Element of X; ::_thesis: ( A is being_line implies ex K being Subset of X st ( a in K & A _|_ K ) ) assume A is being_line ; ::_thesis: ex K being Subset of X st ( a in K & A _|_ K ) then consider b, c being Element of X such that A1: b <> c and A2: A = Line (b,c) by ANALMETR:def_12; consider d being Element of X 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); ::_thesis: ( a in K & A _|_ K ) K = Line (a9,d9) by ANALMETR:41; hence a in K by AFF_1:15; ::_thesis: A _|_ K thus A _|_ K by A1, A2, A3, A4, ANALMETR:45; ::_thesis: verum end; theorem Th4: :: CONMETR:4 for X being OrtAfPl for a, b, c being Element of X for A being Subset of X st A is being_line & a in A & b in A & c in A holds LIN a,b,c proof let X be OrtAfPl; ::_thesis: for a, b, c being Element of X for A being Subset of X st A is being_line & a in A & b in A & c in A holds LIN a,b,c let a, b, c be Element of X; ::_thesis: for A being Subset of X st A is being_line & a in A & b in A & c in A holds LIN a,b,c let A be Subset of X; ::_thesis: ( A is being_line & a in A & b in A & c in A implies LIN a,b,c ) assume that A1: A is being_line and A2: a in A and A3: b in A and A4: c in A ; ::_thesis: LIN a,b,c 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 LIN a,b,c by ANALMETR:40; ::_thesis: verum end; theorem Th5: :: CONMETR:5 for X being OrtAfPl for a, b being Element of X for A, M being Subset of X st A is being_line & M is being_line & a in A & b in A & a in M & b in M & not a = b holds A = M proof let X be OrtAfPl; ::_thesis: for a, b being Element of X for A, M being Subset of X st A is being_line & M is being_line & a in A & b in A & a in M & b in M & not a = b holds A = M let a, b be Element of X; ::_thesis: for A, M being Subset of X st A is being_line & M is being_line & a in A & b in A & a in M & b in M & not a = b holds A = M let A, M be Subset of X; ::_thesis: ( A is being_line & M is being_line & a in A & b in A & a in M & b in M & not a = b implies A = M ) 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 ; ::_thesis: ( a = b or A = 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 ; ::_thesis: A = M A9 is being_line by A1, ANALMETR:43; hence A = M by A3, A4, A5, A6, A8, A7, AFF_1:18; ::_thesis: verum end; theorem Th6: :: CONMETR:6 for X being OrtAfPl for a, b, c, d being Element of X for M being Subset of X for M9 being Subset of (Af X) for 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 X be OrtAfPl; ::_thesis: for a, b, c, d being Element of X for M being Subset of X for M9 being Subset of (Af X) for 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 let a, b, c, d be Element of X; ::_thesis: for M being Subset of X for M9 being Subset of (Af X) for 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 let M be Subset of X; ::_thesis: for M9 being Subset of (Af X) for 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 let M9 be Subset of (Af X); ::_thesis: for 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 let c9, d9 be Element of (Af X); ::_thesis: ( c = c9 & d = d9 & M = M9 & a in M & b in M & c9,d9 // M9 implies c,d // a,b ) assume 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 ; ::_thesis: c,d // a,b 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 c,d // a,b by A1, A2, ANALMETR:36; ::_thesis: verum end; theorem Th7: :: CONMETR:7 for X being OrtAfPl st X is satisfying_TDES holds Af X is Moufangian proof let X be OrtAfPl; ::_thesis: ( X is satisfying_TDES implies Af X is Moufangian ) assume A1: X is satisfying_TDES ; ::_thesis: Af X is Moufangian let K9 be Subset of (Af X); :: according to AFF_2:def_7 ::_thesis: for b1, b2, b3, b4, b5, b6, b7 being Element of the carrier of (Af X) holds ( not K9 is being_line or not b1 in K9 or not b4 in K9 or not b7 in K9 or b2 in K9 or b1 = b4 or b2 = b3 or not LIN b1,b2,b5 or not LIN b1,b3,b6 or not b2,b3 // b5,b6 or not b2,b4 // b5,b7 or not b2,b3 // K9 or b3,b4 // b6,b7 ) let o9, a9, b9, c9, a19, b19, c19 be Element of (Af X); ::_thesis: ( not K9 is being_line or not o9 in K9 or not c9 in K9 or not c19 in K9 or a9 in K9 or o9 = c9 or a9 = b9 or not LIN o9,a9,a19 or not LIN o9,b9,b19 or not a9,b9 // a19,b19 or not a9,c9 // a19,c19 or not a9,b9 // K9 or b9,c9 // b19,c19 ) 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 ; ::_thesis: b9,c9 // b19,c19 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__::_thesis:_(_not_b_in_K_implies_b9,c9_//_b19,c19_) A16: now__::_thesis:_(_o_<>_a1_implies_b9,c9_//_b19,c19_) assume A17: o <> a1 ; ::_thesis: b9,c9 // b19,c19 A18: ( o <> a & o <> b & o <> c & o <> c1 & o <> b1 ) proof A19: now__::_thesis:_not_o_=_b1 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; A22: now__::_thesis:_not_o_=_c1 o9,a9 // o9,a19 by A9, AFF_1:def_1; then A23: o9,a19 // a9,o9 by AFF_1:4; assume o = c1 ; ::_thesis: contradiction 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; ::_thesis: verum end; assume ( o = a or o = b or o = c or o = c1 or o = b1 ) ; ::_thesis: contradiction hence contradiction by A3, A6, A7, A13, A22, A19, AFF_1:35; ::_thesis: verum end; A24: now__::_thesis:_(_a_<>_a19_implies_b9,c9_//_b19,c19_) assume A25: a <> a19 ; ::_thesis: b9,c9 // b19,c19 A26: ( not LIN a,a1,b & not LIN a,a1,c ) proof A27: now__::_thesis:_not_LIN_a,a1,b 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; A30: now__::_thesis:_not_LIN_a,a1,c 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; assume ( LIN a,a1,b or LIN a,a1,c ) ; ::_thesis: contradiction hence contradiction by A27, A30; ::_thesis: verum end; A32: LIN o,b,b1 by A10, ANALMETR:40; o9,c9 // o9,c19 by A2, A3, A4, A5, AFF_1:39, AFF_1: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, AFF_1: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 b9,c9 // b19,c19 by ANALMETR:36; ::_thesis: verum end; now__::_thesis:_(_a_=_a1_implies_b9,c9_//_b19,c19_) A36: not LIN o9,a9,c9 proof assume LIN o9,a9,c9 ; ::_thesis: contradiction then LIN o9,c9,a9 by AFF_1:6; hence contradiction by A2, A3, A4, A6, A7, AFF_1:25; ::_thesis: verum end; assume A37: a = a1 ; ::_thesis: b9,c9 // b19,c19 o9,c9 // o9,c19 by A2, A3, A4, A5, AFF_1:39, AFF_1: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 ; ::_thesis: contradiction 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; ::_thesis: verum end; then b9 = b19 by A10, A11, A37, AFF_1:14; hence b9,c9 // b19,c19 by A38, AFF_1:2; ::_thesis: verum end; hence b9,c9 // b19,c19 by A24; ::_thesis: verum end; assume A40: not b in K ; ::_thesis: b9,c9 // b19,c19 A41: ( o = a1 implies ( o = b1 & o = c1 ) ) proof assume that A42: o = a1 and A43: ( o <> b1 or o <> c1 ) ; ::_thesis: contradiction A44: now__::_thesis:_not_o_<>_c1 A45: o9,c19 // a9,c9 by A12, A42, AFF_1:4; assume A46: o <> c1 ; ::_thesis: contradiction o9,c19 // o9,c9 by A2, A3, A4, A5, AFF_1:39, AFF_1: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; ::_thesis: verum end; now__::_thesis:_not_o_<>_b1 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 ; ::_thesis: contradiction LIN o9,b19,b9 by A10, AFF_1:6; hence contradiction by A2, A3, A40, A48, A47, AFF_1:25; ::_thesis: verum end; hence contradiction by A43, A44; ::_thesis: verum end; now__::_thesis:_(_o_=_a1_implies_b9,c9_//_b19,c19_) assume o = a1 ; ::_thesis: b9,c9 // b19,c19 then b,c // b1,c1 by A41, ANALMETR:39; hence b9,c9 // b19,c19 by ANALMETR:36; ::_thesis: verum end; hence b9,c9 // b19,c19 by A16; ::_thesis: verum end; hence b9,c9 // b19,c19 by A6, A13, AFF_1:35; ::_thesis: verum end; theorem Th8: :: CONMETR:8 for X being OrtAfPl st Af X is translational holds X is satisfying_des proof let X be OrtAfPl; ::_thesis: ( Af X is translational implies X is satisfying_des ) assume A1: Af X is translational ; ::_thesis: X is satisfying_des let a be Element of X; :: according to CONMETR:def_8 ::_thesis: for a1, b, b1, c, c1 being Element of X 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 let a1, b, b1, c, c1 be Element of X; ::_thesis: ( 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 implies b,c // b1,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 ; ::_thesis: b,c // b1,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 being 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 ; ::_thesis: contradiction then LIN a9,a19,b9 by AFF_1:7; hence contradiction by A2, ANALMETR:40; ::_thesis: verum end; then for x9 being Element of (Af X) holds ( x9 in A9 iff LIN a9,a19,x9 ) by A8, A9, A10, AFF_1:21, AFF_1: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 ; ::_thesis: contradiction then LIN a9,a19,b9 by AFF_1:7; hence contradiction by A2, ANALMETR:40; ::_thesis: verum end; then for x9 being Element of (Af X) holds ( x9 in A9 iff LIN a9,a19,x9 ) by A8, A9, A10, AFF_1:21, AFF_1: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 being 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 being 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 ) ; ::_thesis: contradiction 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; ::_thesis: verum end; A26: c9 <> c19 proof assume c9 = c19 ; ::_thesis: contradiction 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; ::_thesis: verum end; then for x9 being Element of (Af X) holds ( x9 in N9 iff LIN c9,c19,x9 ) by A19, A20, A21, AFF_1:21, AFF_1: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 ; ::_thesis: contradiction 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; ::_thesis: verum end; then for x9 being Element of (Af X) holds ( x9 in M9 iff LIN b9,b19,x9 ) by A22, A23, A24, AFF_1:21, AFF_1: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 b,c // b1,c1 by ANALMETR:36; ::_thesis: verum end; theorem :: CONMETR:9 for X being OrtAfPl st X is satisfying_MH1 holds X is satisfying_OSCH proof let X be OrtAfPl; ::_thesis: ( X is satisfying_MH1 implies X is satisfying_OSCH ) assume A1: X is satisfying_MH1 ; ::_thesis: X is satisfying_OSCH let a1 be Element of X; :: according to CONMETR:def_7 ::_thesis: for a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X 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 let a2, a3, a4, b1, b2, b3, b4 be Element of X; ::_thesis: for M, N being Subset of X 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 let M, N be Subset of X; ::_thesis: ( 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 implies a3,a4 // b3,b4 ) 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 ; ::_thesis: a3,a4 // b3,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 ; ::_thesis: contradiction then M // N by ANALMETR:46; hence contradiction by A2, ANALMETR:52; ::_thesis: verum end; then ex o9 being Element of (Af X) st ( o9 in M9 & o9 in N9 ) by A22, A21, AFF_1:58; then consider o being Element of X such that A23: o in M and A24: o in N ; reconsider o9 = o as Element of (Af X) by ANALMETR:35; A25: now__::_thesis:_(_b2_<>_b4_implies_a3,a4_//_b3,b4_) assume A26: b2 <> b4 ; ::_thesis: a3,a4 // b3,b4 A27: now__::_thesis:_(_b1_<>_b3_implies_a3,a4_//_b3,b4_) consider e19 being 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 being Element of (Af X) st ( o9 <> d49 & d49 in N9 ) by A21, AFF_1:20; then consider d4 being Element of X such that A30: d4 in N and A31: d4 <> o ; reconsider d49 = d4 as Element of (Af X) by ANALMETR:35; consider e2 being Element of X 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 ; ::_thesis: a3,a4 // b3,b4 not o9,e19 // d49,e29 proof A35: a49 <> a29 proof assume a49 = a29 ; ::_thesis: contradiction 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; ::_thesis: verum end; A36: a1 <> a3 proof assume a1 = a3 ; ::_thesis: contradiction 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; ::_thesis: verum end; assume o9,e19 // d49,e29 ; ::_thesis: contradiction 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, AFF_1: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; ::_thesis: verum end; then consider d19 being 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 being 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 being Element of X 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; o9,e19 // a29,a49 by A7, A8, A21, A24, A42, AFF_1:39, AFF_1:41; then A49: o,e1 // a2,a4 by ANALMETR:36; A50: a2 <> a4 proof assume a2 = a4 ; ::_thesis: contradiction 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; ::_thesis: verum end; assume o9,e19 // e29,d19 ; ::_thesis: contradiction 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; ::_thesis: verum end; then consider d29 being 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 being 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 being Element of X 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; assume o9,e19 // e29,d29 ; ::_thesis: contradiction 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; ::_thesis: verum end; then consider d39 being 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 a3,a4 // b3,b4 by A68, A71, ANALMETR:63; ::_thesis: verum end; now__::_thesis:_(_b1_=_b3_implies_a3,a4_//_b3,b4_) A72: not LIN o9,a29,a19 proof assume LIN o9,a29,a19 ; ::_thesis: contradiction then o9,a29 // o9,a19 by AFF_1:def_1; hence contradiction by A7, A12, A15, A21, A23, A24, AFF_1:48; ::_thesis: verum end; A73: LIN o9,a19,a39 by A3, A4, A22, A23, AFF_1:21; assume A74: b1 = b3 ; ::_thesis: a3,a4 // b3,b4 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 a3,a4 // b3,b4 by A20, A74, A72, A73, AFF_1:14; ::_thesis: verum end; hence a3,a4 // b3,b4 by A27; ::_thesis: verum end; now__::_thesis:_(_b2_=_b4_implies_a3,a4_//_b3,b4_) A76: not LIN o9,a19,a49 proof assume LIN o9,a19,a49 ; ::_thesis: contradiction then ex A9 being Subset of (Af X) 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; ::_thesis: verum end; assume A77: b2 = b4 ; ::_thesis: a3,a4 // b3,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 a3,a4 // b3,b4 by A18, A77, A78, A76, AFF_1:14; ::_thesis: verum end; hence a3,a4 // b3,b4 by A25; ::_thesis: verum end; theorem :: CONMETR:10 for X being OrtAfPl st X is satisfying_MH2 holds X is satisfying_OSCH proof let X be OrtAfPl; ::_thesis: ( X is satisfying_MH2 implies X is satisfying_OSCH ) assume A1: X is satisfying_MH2 ; ::_thesis: X is satisfying_OSCH let a1 be Element of X; :: according to CONMETR:def_7 ::_thesis: for a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X 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 let a2, a3, a4, b1, b2, b3, b4 be Element of X; ::_thesis: for M, N being Subset of X 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 let M, N be Subset of X; ::_thesis: ( 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 implies a3,a4 // b3,b4 ) 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 ; ::_thesis: a3,a4 // b3,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 ; ::_thesis: contradiction then M // N by ANALMETR:46; hence contradiction by A2, ANALMETR:52; ::_thesis: verum end; then ex o9 being Element of (Af X) st ( o9 in M9 & o9 in N9 ) by A22, A21, AFF_1:58; then consider o being Element of X such that A23: o in M and A24: o in N ; reconsider o9 = o as Element of (Af X) by ANALMETR:35; A25: now__::_thesis:_(_b2_<>_b4_implies_a3,a4_//_b3,b4_) assume A26: b2 <> b4 ; ::_thesis: a3,a4 // b3,b4 A27: now__::_thesis:_(_b1_<>_b3_implies_a3,a4_//_b3,b4_) ex d39 being Element of (Af X) st ( o9 <> d39 & d39 in N9 ) by A21, AFF_1:20; then consider d3 being Element of X such that A28: d3 in N and A29: d3 <> o ; reconsider d39 = d3 as Element of (Af X) by ANALMETR:35; consider e2 being Element of X such that A30: a3,a2 _|_ d3,e2 and A31: d3 <> e2 by ANALMETR:def_9; consider e1 being Element of X 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 ; ::_thesis: a3,a4 // b3,b4 A35: ( a1 <> a3 & a2 <> a4 ) proof assume ( a1 = a3 or a2 = a4 ) ; ::_thesis: contradiction 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; ::_thesis: verum end; not a39,e19 // d39,e29 proof assume a39,e19 // d39,e29 ; ::_thesis: contradiction 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; ::_thesis: verum end; then consider d29 being 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 being Element of X 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 being Element of X such that A42: a2,a4 // a2,e1 and A43: a2 <> e1 by ANALMETR:39; consider e2 being Element of X 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; then consider d19 being 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 being Element of X such that A53: a1,a4 _|_ d1,e2 and A54: d1 <> e2 by ANALMETR:39; consider e1 being Element of X 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; then consider d49 being 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 a3,a4 // b3,b4 by A63, A61, ANALMETR:63; ::_thesis: verum end; now__::_thesis:_(_b1_=_b3_implies_a3,a4_//_b3,b4_) o9,a19 // o9,a39 by A3, A4, A22, A23, AFF_1:39, AFF_1:41; then A64: LIN o9,a19,a39 by AFF_1:def_1; assume A65: b1 = b3 ; ::_thesis: a3,a4 // b3,b4 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 a3,a4 // b3,b4 by A7, A12, A15, A20, A21, A23, A24, A65, A64, AFF_1:14, AFF_1:25; ::_thesis: verum end; hence a3,a4 // b3,b4 by A27; ::_thesis: verum end; now__::_thesis:_(_b2_=_b4_implies_a3,a4_//_b3,b4_) o9,a29 // o9,a49 by A7, A8, A21, A24, AFF_1:39, AFF_1:41; then A66: LIN o9,a29,a49 by AFF_1:def_1; assume A67: b2 = b4 ; ::_thesis: a3,a4 // b3,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 a3,a4 // b3,b4 by A3, A12, A15, A18, A22, A23, A24, A67, A66, AFF_1:14, AFF_1:25; ::_thesis: verum end; hence a3,a4 // b3,b4 by A25; ::_thesis: verum end; theorem :: CONMETR:11 for X being OrtAfPl st X is satisfying_AH holds X is satisfying_TDES proof let X be OrtAfPl; ::_thesis: ( X is satisfying_AH implies X is satisfying_TDES ) assume A1: X is satisfying_AH ; ::_thesis: X is satisfying_TDES let o be Element of X; :: according to CONMETR:def_5 ::_thesis: for a, a1, b, b1, c, c1 being Element of X 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 let a, a1, b, b1, c, c1 be Element of X; ::_thesis: ( 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 implies a,c // a1,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 ; ::_thesis: a,c // a1,c1 consider e1 being Element of X such that A16: o,b _|_ o,e1 and A17: o <> e1 by ANALMETR:def_9; consider c2 being Element of X such that A18: o,c _|_ o,c2 and A19: o <> c2 by ANALMETR:def_9; consider e2 being Element of X 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 ; ::_thesis: contradiction 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 ; ::_thesis: contradiction then LIN b9,b19,a9 by AFF_1:7; hence contradiction by A8, ANALMETR:40; ::_thesis: verum 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; ::_thesis: verum end; A28: now__::_thesis:_(_not_LIN_a,b,c_implies_a,c_//_a1,c1_) not o9,e19 // c29,e29 proof assume o9,e19 // c29,e29 ; ::_thesis: contradiction 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; ::_thesis: verum end; then consider b29 being Element of (Af X) 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 ; ::_thesis: a,c // a1,c1 A35: b <> a proof assume b = a ; ::_thesis: contradiction then LIN a9,b9,c9 by AFF_1:7; hence contradiction by A34, ANALMETR:40; ::_thesis: verum end; A36: not o,c // o,b proof assume o,c // o,b ; ::_thesis: contradiction 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; ::_thesis: verum end; A38: not o,a // o,c proof assume o,a // o,c ; ::_thesis: contradiction 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; ::_thesis: verum 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 being Element of X such that A41: o,a _|_ o,e1 and A42: o <> e1 by ANALMETR:def_9; consider e2 being Element of X 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; then consider a29 being Element of (Af X) 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 ; ::_thesis: contradiction 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; ::_thesis: verum 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; A54: o <> a2 proof assume A55: o = a2 ; ::_thesis: contradiction 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; ::_thesis: verum end; assume LIN o9,b29,a29 ; ::_thesis: contradiction 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 ; ::_thesis: contradiction then LIN a9,b9,c9 by AFF_1:7; hence contradiction by A34, ANALMETR:40; ::_thesis: verum 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; ::_thesis: verum end; consider e1 being Element of X such that A58: o,a1 _|_ o,e1 and A59: o <> e1 by ANALMETR:def_9; consider e2 being Element of X 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; then consider a39 being Element of (Af X) 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 ; ::_thesis: contradiction then LIN a9,b9,c9 by AFF_1:7; hence contradiction by A34, ANALMETR:40; ::_thesis: verum 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 ; ::_thesis: contradiction 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; ::_thesis: verum 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; a <> b proof assume a = b ; ::_thesis: contradiction then LIN b9,b19,a9 by AFF_1:7; hence contradiction by A8, ANALMETR:40; ::_thesis: verum 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 a,c // a1,c1 by ANALMETR:36; ::_thesis: verum end; now__::_thesis:_(_LIN_a,b,c_implies_a,c_//_a1,c1_) assume A82: LIN a,b,c ; ::_thesis: a,c // a1,c1 then A83: LIN a9,b9,c9 by ANALMETR:40; A84: a <> b proof assume a = b ; ::_thesis: contradiction then LIN b9,b19,a9 by AFF_1:7; hence contradiction by A8, ANALMETR:40; ::_thesis: verum end; A85: now__::_thesis:_(_a1,c1_//_a,b_implies_a,c_//_a1,c1_) assume a1,c1 // a,b ; ::_thesis: a,c // a1,c1 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 a,c // a1,c1 by A84, A86, ANALMETR:60; ::_thesis: verum end; A87: b <> c proof assume b = c ; ::_thesis: contradiction then LIN b9,b19,c9 by AFF_1:7; hence contradiction by A9, ANALMETR:40; ::_thesis: verum end; A88: now__::_thesis:_(_a1_=_b1_implies_a,c_//_a1,c1_) 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 ; ::_thesis: a,c // a1,c1 hence a,c // a1,c1 by A15, A87, A89, ANALMETR:60; ::_thesis: verum 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 a,c // a1,c1 by A90, A85, A88, ANALMETR:60; ::_thesis: verum end; hence a,c // a1,c1 by A28; ::_thesis: verum end; theorem :: CONMETR:12 for X being OrtAfPl st X is satisfying_OSCH & X is satisfying_TDES holds X is satisfying_SCH proof let X be OrtAfPl; ::_thesis: ( X is satisfying_OSCH & X is satisfying_TDES implies X is satisfying_SCH ) assume that A1: X is satisfying_OSCH and A2: X is satisfying_TDES ; ::_thesis: X is satisfying_SCH let a1 be Element of X; :: according to CONMETR:def_6 ::_thesis: for a2, a3, a4, b1, b2, b3, b4 being Element of X for M, N being Subset of X 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 let a2, a3, a4, b1, b2, b3, b4 be Element of X; ::_thesis: for M, N being Subset of X 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 let M, N be Subset of X; ::_thesis: ( 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 implies a3,a4 // b3,b4 ) 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 ; ::_thesis: a3,a4 // b3,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 ; ::_thesis: ( a2 <> b2 & a3 <> b3 & a4 <> b4 ) A28: now__::_thesis:_not_a4_=_b4 assume a4 = b4 ; ::_thesis: contradiction 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; ::_thesis: verum end; A29: now__::_thesis:_not_a2_=_b2 assume a2 = b2 ; ::_thesis: contradiction 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; ::_thesis: verum end; A30: now__::_thesis:_not_a3_=_b3 assume a3 = b3 ; ::_thesis: contradiction 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; ::_thesis: verum end; assume ( a2 = b2 or a3 = b3 or a4 = b4 ) ; ::_thesis: contradiction hence contradiction by A29, A28, A30; ::_thesis: verum end; A31: now__::_thesis:_(_a1_<>_b1_implies_a3,a4_//_b3,b4_) assume A32: a1 <> b1 ; ::_thesis: a3,a4 // b3,b4 A33: now__::_thesis:_(_a2_=_a4_implies_a3,a4_//_b3,b4_) A34: not LIN a29,b19,b29 proof assume LIN a29,b19,b29 ; ::_thesis: contradiction then LIN a29,b29,b19 by AFF_1:6; hence contradiction by A9, A11, A19, A25, A26, A32, AFF_1:25; ::_thesis: verum end; assume A35: a2 = a4 ; ::_thesis: a3,a4 // b3,b4 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, AFF_1:41; then LIN a29,b29,b49 by AFF_1:def_1; hence a3,a4 // b3,b4 by A21, A35, A34, A36, AFF_1:14; ::_thesis: verum end; A37: now__::_thesis:_(_a2_<>_a4_&_a1_<>_a3_implies_a3,a4_//_b3,b4_) assume that A38: a2 <> a4 and A39: a1 <> a3 ; ::_thesis: a3,a4 // b3,b4 A40: now__::_thesis:_(_M_//_N_implies_a3,a4_//_b3,b4_) consider e1 being Element of X such that A41: b1,b2 // b1,e1 and A42: b1 <> e1 by ANALMETR:39; consider x being 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 being 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; then consider y9 being 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; LIN a19,a29,x9 by A43, ANALMETR:40; then A53: LIN a29,x9,a19 by AFF_1:6; assume LIN a2,b2,x ; ::_thesis: contradiction 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; ::_thesis: verum end; A54: not LIN a1,b1,a4 proof assume LIN a1,b1,a4 ; ::_thesis: contradiction then LIN a19,b19,a49 by ANALMETR:40; hence contradiction by A5, A7, A13, A24, A32, AFF_1:25; ::_thesis: verum end; A55: not LIN a1,b1,x proof assume LIN a1,b1,x ; ::_thesis: contradiction 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; ::_thesis: verum end; assume A57: M // N ; ::_thesis: a3,a4 // b3,b4 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 ; ::_thesis: contradiction 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; ::_thesis: verum 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; a19,a39 // a19,b19 by A5, A6, A7, A24, AFF_1:39, AFF_1: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 ; ::_thesis: contradiction 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; ::_thesis: verum end; A70: not LIN x,y,a4 proof A71: x <> y proof assume x = y ; ::_thesis: contradiction 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; ::_thesis: verum 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; A75: not LIN a2,b2,a3 proof A76: a2 <> b2 proof assume a2 = b2 ; ::_thesis: contradiction 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; ::_thesis: verum end; assume LIN a2,b2,a3 ; ::_thesis: contradiction then LIN a29,b29,a39 by ANALMETR:40; hence contradiction by A9, A11, A18, A25, A76, AFF_1:25; ::_thesis: verum end; A77: ( X is satisfying_TDES implies X is satisfying_des ) proof assume X is satisfying_TDES ; ::_thesis: X is satisfying_des then Af X is Moufangian by Th7; then Af X is translational by AFF_2:14; hence X is satisfying_des by Th8; ::_thesis: verum 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, AFF_1: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 a3,a4 // b3,b4 by A2, A77, A82, A65, A70, A79, A80, Def8; ::_thesis: verum end; now__::_thesis:_(_not_M_//_N_implies_a3,a4_//_b3,b4_) assume not M // N ; ::_thesis: a3,a4 // b3,b4 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 being Subset of X 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__::_thesis:_(_K_<>_M_implies_a3,a4_//_b3,b4_) A89: ( not a2 in K & not a4 in K & not b2 in K & not b4 in K ) proof A90: now__::_thesis:_for_x_being_Element_of_X_st_x_in_N_&_o_<>_x_holds_ not_x_in_K let x be Element of X; ::_thesis: ( x in N & o <> x implies not x in K ) assume that A91: x in N and A92: o <> x ; ::_thesis: not x in K assume x in K ; ::_thesis: contradiction then o,x _|_ o,x by A84, A85, A86, A91, ANALMETR:56; hence contradiction by A92, ANALMETR:39; ::_thesis: verum end; assume ( a2 in K or a4 in K or b2 in K or b4 in K ) ; ::_thesis: contradiction hence contradiction by A9, A10, A11, A12, A13, A14, A15, A16, A83, A90; ::_thesis: verum end; A93: LIN o,a2,b2 by A4, A9, A11, A84, Th4; A94: now__::_thesis:_not_LIN_a1,b1,a4 assume LIN a1,b1,a4 ; ::_thesis: contradiction then LIN a19,b19,a49 by ANALMETR:40; hence contradiction by A5, A7, A13, A24, A32, AFF_1:25; ::_thesis: verum end; A95: LIN o,a3,b3 by A3, A6, A8, A83, Th4; A96: now__::_thesis:_not_LIN_a3,b3,a2 assume LIN a3,b3,a2 ; ::_thesis: contradiction then LIN a39,b39,a29 by ANALMETR:40; hence contradiction by A6, A8, A14, A24, A26, A32, AFF_1:25; ::_thesis: verum end; A97: LIN o,a1,b1 by A3, A5, A7, A83, Th4; A98: now__::_thesis:_for_x9_being_Element_of_(Af_X)_ex_y9_being_Element_of_(Af_X)_st_ (_y9_in_K9_&_x9,y9_//_N9_) let x9 be Element of (Af X); ::_thesis: ex y9 being Element of (Af X) st ( y9 in K9 & x9,y9 // N9 ) 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 = y9; ::_thesis: ( y9 in K9 & x9,y9 // N9 ) thus ( y9 in K9 & x9,y9 // N9 ) by A99, A100, A101, A102, AFF_1:40; ::_thesis: verum end; then consider d19 being Element of (Af X) such that A103: d19 in K9 and A104: a19,d19 // N9 ; consider e19 being Element of (Af X) such that A105: e19 in K9 and A106: b19,e19 // N9 by A98; consider d39 being Element of (Af X) such that A107: d39 in K9 and A108: a39,d39 // N9 by A98; consider e39 being 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__::_thesis:_for_x,_y_being_Element_of_X for_x9,_y9_being_Element_of_(Af_X)_st_x9,y9_//_N9_&_x_=_x9_&_y_=_y9_&_x_in_M_&_y_in_K_&_not_x_in_N_holds_ not_o_=_y let x, y be Element of X; ::_thesis: for x9, y9 being Element of (Af X) st x9,y9 // N9 & x = x9 & y = y9 & x in M & y in K & not x in N holds not o = y let x9, y9 be Element of (Af X); ::_thesis: ( x9,y9 // N9 & x = x9 & y = y9 & x in M & y in K & not x in N implies not o = y ) 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 ; ::_thesis: not o = y assume o = y ; ::_thesis: contradiction then o9,x9 // N9 by A114, A116, AFF_1:34; hence contradiction by A25, A84, A115, A117, AFF_1:23; ::_thesis: verum end; assume ( not o <> e1 or not o <> e3 or not o <> d1 or not o <> d3 ) ; ::_thesis: contradiction hence contradiction by A5, A6, A7, A8, A17, A18, A19, A20, A103, A104, A107, A108, A109, A110, A105, A106, A113; ::_thesis: verum 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 ; ::_thesis: a3,a4 // b3,b4 A123: now__::_thesis:_not_LIN_a3,b3,d3 assume LIN a3,b3,d3 ; ::_thesis: contradiction 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; ::_thesis: verum end; A124: now__::_thesis:_not_LIN_a1,b1,d1 assume LIN a1,b1,d1 ; ::_thesis: contradiction 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; ::_thesis: verum 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 d3 <> e3 ; ::_thesis: contradiction 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; ::_thesis: verum end; assume ( LIN d3,e3,a3 or LIN d3,e3,a4 ) ; ::_thesis: contradiction 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; ::_thesis: verum end; A129: now__::_thesis:_not_LIN_a1,b1,a2 assume LIN a1,b1,a2 ; ::_thesis: contradiction then LIN a19,b19,a29 by ANALMETR:40; hence contradiction by A5, A7, A14, A24, A32, AFF_1:25; ::_thesis: verum 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 a3,a4 // b3,b4 by A2, A13, A16, A18, A20, A83, A84, A112, A130, A95, A133, A125, A127, A135, Def5; ::_thesis: verum end; hence a3,a4 // b3,b4 by A1, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22, A23, A86, Def7; ::_thesis: verum end; hence a3,a4 // b3,b4 by A40; ::_thesis: verum end; now__::_thesis:_(_a1_=_a3_implies_a3,a4_//_b3,b4_) A137: not LIN a19,b29,b19 proof assume LIN a19,b29,b19 ; ::_thesis: contradiction then LIN a19,b19,b29 by AFF_1:6; hence contradiction by A5, A7, A15, A24, A32, AFF_1:25; ::_thesis: verum end; a19,b19 // a19,b39 by A5, A7, A8, A24, AFF_1:39, AFF_1:41; then A138: LIN a19,b19,b39 by AFF_1:def_1; assume A139: a1 = a3 ; ::_thesis: a3,a4 // b3,b4 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 a3,a4 // b3,b4 by A23, A139, A137, A138, AFF_1:14; ::_thesis: verum end; hence a3,a4 // b3,b4 by A33, A37; ::_thesis: verum end; A140: ( a1 = b1 implies ( a2 = b2 & a3 = b3 & a4 = b4 ) ) proof assume A141: a1 = b1 ; ::_thesis: ( a2 = b2 & a3 = b3 & a4 = b4 ) A142: now__::_thesis:_not_a4_<>_b4 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 ; ::_thesis: contradiction hence contradiction by A10, A12, A17, A25, A143, AFF_1:25; ::_thesis: verum end; A144: now__::_thesis:_not_a2_<>_b2 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 ; ::_thesis: contradiction hence contradiction by A9, A11, A17, A25, A145, AFF_1:25; ::_thesis: verum end; A146: now__::_thesis:_not_a3_<>_b3 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 ; ::_thesis: contradiction hence contradiction by A6, A8, A14, A24, A147, AFF_1:25; ::_thesis: verum end; assume ( a2 <> b2 or a3 <> b3 or a4 <> b4 ) ; ::_thesis: contradiction hence contradiction by A144, A142, A146; ::_thesis: verum end; now__::_thesis:_(_a1_=_b1_implies_a3,a4_//_b3,b4_) assume a1 = b1 ; ::_thesis: a3,a4 // b3,b4 then a39,a49 // b39,b49 by A140, AFF_1:2; hence a3,a4 // b3,b4 by ANALMETR:36; ::_thesis: verum end; hence a3,a4 // b3,b4 by A31; ::_thesis: verum end; theorem :: CONMETR:13 for X being OrtAfPl st X is satisfying_OPAP & X is satisfying_DES holds X is satisfying_PAP proof let X be OrtAfPl; ::_thesis: ( X is satisfying_OPAP & X is satisfying_DES implies X is satisfying_PAP ) assume that A1: X is satisfying_OPAP and A2: X is satisfying_DES ; ::_thesis: X is satisfying_PAP let o be Element of X; :: according to CONMETR:def_2 ::_thesis: for a1, a2, a3, b1, b2, b3 being Element of X for M, N being Subset of X 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 let a1, a2, a3, b1, b2, b3 be Element of X; ::_thesis: for M, N being Subset of X 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 let M, N be Subset of X; ::_thesis: ( 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 implies a1,b2 // a2,b3 ) 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 ; ::_thesis: a1,b2 // a2,b3 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__::_thesis:_(_not_M__|__N_implies_a1,b2_//_a2,b3_) assume A23: not M _|_ N ; ::_thesis: a1,b2 // a2,b3 A24: now__::_thesis:_(_a1_<>_a2_&_a2_<>_a3_&_a1_<>_a3_implies_a1,b2_//_a2,b3_) assume that A25: a1 <> a2 and A26: a2 <> a3 and A27: a1 <> a3 ; ::_thesis: a1,b2 // a2,b3 A28: ( b1 <> b2 & b2 <> b3 & b1 <> b3 ) proof A29: now__::_thesis:_not_b1_=_b3 A30: not LIN o9,b19,a19 proof o9,a19 // o9,a39 by A5, A6, A8, A21, AFF_1:39, AFF_1:41; then A31: LIN o9,a19,a39 by AFF_1:def_1; assume LIN o9,b19,a19 ; ::_thesis: contradiction then a19 in N9 by A9, A10, A17, A22, AFF_1:25; hence contradiction by A9, A14, A15, A22, A31, AFF_1:25; ::_thesis: verum end; assume b1 = b3 ; ::_thesis: contradiction 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, AFF_1:41; then LIN o9,a19,a39 by AFF_1:def_1; hence contradiction by A27, A30, A32, AFF_1:14; ::_thesis: verum end; A33: now__::_thesis:_not_b2_=_b3 A34: not LIN o9,b19,a19 proof o9,a19 // o9,a39 by A5, A6, A8, A21, AFF_1:39, AFF_1:41; then A35: LIN o9,a19,a39 by AFF_1:def_1; assume LIN o9,b19,a19 ; ::_thesis: contradiction then a19 in N9 by A9, A10, A17, A22, AFF_1:25; hence contradiction by A9, A14, A15, A22, A35, AFF_1:25; ::_thesis: verum end; assume b2 = b3 ; ::_thesis: contradiction 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, AFF_1:41; then LIN o9,a19,a29 by AFF_1:def_1; hence contradiction by A25, A34, A36, AFF_1:14; ::_thesis: verum end; A37: now__::_thesis:_not_b1_=_b2 A38: not LIN o9,b29,a29 proof assume LIN o9,b29,a29 ; ::_thesis: contradiction then LIN o9,a29,b29 by AFF_1:6; hence contradiction by A5, A7, A13, A16, A21, AFF_1:25; ::_thesis: verum end; assume b1 = b2 ; ::_thesis: contradiction 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, AFF_1:41; then LIN o9,a29,a39 by AFF_1:def_1; hence contradiction by A26, A38, A39, AFF_1:14; ::_thesis: verum end; assume ( b1 = b2 or b2 = b3 or b1 = b3 ) ; ::_thesis: contradiction hence contradiction by A37, A33, A29; ::_thesis: verum end; A40: now__::_thesis:_(_not_a3,b3__|__o,b2_implies_a1,b2_//_a2,b3_) A41: not LIN b3,b1,a3 proof assume LIN b3,b1,a3 ; ::_thesis: contradiction then LIN b39,b19,a39 by ANALMETR:40; hence contradiction by A10, A12, A14, A22, A28, AFF_1:25; ::_thesis: verum end; o9,b29 // o9,b39 by A9, A11, A12, A22, AFF_1:39, AFF_1: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 ; ::_thesis: contradiction then LIN b29,b19,a39 by ANALMETR:40; hence contradiction by A10, A11, A14, A22, A28, AFF_1:25; ::_thesis: verum end; o9,a39 // o9,a19 by A5, A6, A8, A21, AFF_1:39, AFF_1:41; then LIN o9,a39,a19 by AFF_1:def_1; then A44: LIN o,a3,a1 by ANALMETR:40; consider x being 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 being 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 being 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 being Element of X st e1 in A holds LIN o,x,e1 proof let e1 be Element of X; ::_thesis: ( e1 in A implies LIN o,x,e1 ) assume A54: e1 in A ; ::_thesis: LIN o,x,e1 reconsider e19 = e1 as Element of (Af X) by ANALMETR:35; o9,x9 // o9,e19 by A50, A51, A52, A54, AFF_1:39, AFF_1:41; then LIN o9,x9,e19 by AFF_1:def_1; hence LIN o,x,e1 by ANALMETR:40; ::_thesis: verum end; for e1 being Element of X st LIN o,x,e1 holds e1 in A proof let e1 be Element of X; ::_thesis: ( LIN o,x,e1 implies e1 in A ) assume A55: LIN o,x,e1 ; ::_thesis: e1 in A reconsider e19 = e1 as Element of (Af X) by ANALMETR:35; LIN o9,x9,e19 by A55, ANALMETR:40; hence e1 in A by A46, A50, A51, A52, AFF_1:25; ::_thesis: verum 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; assume A59: not a3,b3 _|_ o,b2 ; ::_thesis: a1,b2 // a2,b3 not b29,e19 // A9 proof assume A60: b29,e19 // A9 ; ::_thesis: contradiction consider d19, d29 being 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; ::_thesis: verum end; then consider c39 being 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 being 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 ; ::_thesis: contradiction then A71: a3,b3 // b2,o by A67, ANALMETR:36; b29,o9 // b29,b39 by A9, A11, A12, A22, AFF_1:39, AFF_1: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; ::_thesis: verum end; assume A72: a19,e19 // A9 ; ::_thesis: contradiction A73: o9,a39 // o9,a39 by AFF_1:2; o9,c39 // A9 by A50, A51, A65, AFF_1:40, AFF_1: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; ::_thesis: verum end; then consider c19 being 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 being 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 ; ::_thesis: contradiction then A81: a3,b3 // b2,o by A67, ANALMETR:36; b29,o9 // b29,b39 by A9, A11, A12, A22, AFF_1:39, AFF_1: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; ::_thesis: verum end; assume A82: a29,e19 // A9 ; ::_thesis: contradiction A83: o9,a39 // o9,a39 by AFF_1:2; o9,c39 // A9 by A50, A51, A65, AFF_1:40, AFF_1: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; ::_thesis: verum end; then consider c29 being 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__::_thesis:_not_o_=_c3 assume A90: o = c3 ; ::_thesis: contradiction b29,o9 // b39,b29 by A9, A11, A12, A22, AFF_1:39, AFF_1: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; ::_thesis: verum end; A91: now__::_thesis:_(_not_o_=_c2_&_not_o_=_c1_) a19,o9 // a19,a39 by A5, A6, A8, A21, AFF_1:39, AFF_1:41; then A92: a1,o // a1,a3 by ANALMETR:36; assume ( o = c2 or o = c1 ) ; ::_thesis: contradiction 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, AFF_1: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; ::_thesis: verum end; assume ( o = c3 or o = c2 or o = c1 ) ; ::_thesis: contradiction hence contradiction by A89, A91; ::_thesis: verum end; A95: not c3 in N proof A96: o9,c39 // o9,c39 by AFF_1:2; assume c3 in N ; ::_thesis: contradiction 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; ::_thesis: verum end; A97: not LIN a3,a2,c3 proof assume LIN a3,a2,c3 ; ::_thesis: contradiction 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; ::_thesis: verum end; A99: not LIN a3,a1,c3 proof assume LIN a3,a1,c3 ; ::_thesis: contradiction 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; ::_thesis: verum end; A101: not LIN a1,a2,c1 proof assume LIN a1,a2,c1 ; ::_thesis: contradiction 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; ::_thesis: verum end; o9,a19 // o9,a29 by A5, A6, A7, A21, AFF_1:39, AFF_1: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, AFF_1: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, AFF_1: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, AFF_1: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, AFF_1: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 ; ::_thesis: contradiction 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; ::_thesis: verum 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; assume c19 = c29 ; ::_thesis: contradiction 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; ::_thesis: verum end; assume LIN c1,c2,b2 ; ::_thesis: contradiction 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; ::_thesis: verum end; o9,a39 // o9,a29 by A5, A7, A8, A21, AFF_1:39, AFF_1: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, AFF_1: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 a1,b2 // a2,b3 by A2, A5, A13, A15, A16, A18, A88, A103, A42, A105, A101, A110, A109, CONAFFM:def_1; ::_thesis: verum end; now__::_thesis:_(_a3,b3__|__o,b2_implies_a1,b2_//_a2,b3_) o9,a19 // o9,a29 by A5, A6, A7, A21, AFF_1:39, AFF_1: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, AFF_1: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, AFF_1: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 ) ; ::_thesis: contradiction 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; ::_thesis: verum end; o9,a39 // o9,a29 by A5, A7, A8, A21, AFF_1:39, AFF_1: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, AFF_1: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, AFF_1:41; then LIN o9,a39,a19 by AFF_1:def_1; then A124: LIN o,a3,a1 by ANALMETR:40; consider x being 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 being 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 being 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 being Element of X st e1 in A holds LIN o,x,e1 proof let e1 be Element of X; ::_thesis: ( e1 in A implies LIN o,x,e1 ) assume A134: e1 in A ; ::_thesis: LIN o,x,e1 reconsider e19 = e1 as Element of (Af X) by ANALMETR:35; o9,x9 // o9,e19 by A130, A131, A132, A134, AFF_1:39, AFF_1:41; then LIN o9,x9,e19 by AFF_1:def_1; hence LIN o,x,e1 by ANALMETR:40; ::_thesis: verum end; for e1 being Element of X st LIN o,x,e1 holds e1 in A proof let e1 be Element of X; ::_thesis: ( LIN o,x,e1 implies e1 in A ) assume A135: LIN o,x,e1 ; ::_thesis: e1 in A reconsider e19 = e1 as Element of (Af X) by ANALMETR:35; LIN o9,x9,e19 by A135, ANALMETR:40; hence e1 in A by A126, A130, A131, A132, AFF_1:25; ::_thesis: verum 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 ; ::_thesis: a1,b2 // a2,b3 not b39,e19 // A9 proof assume A138: b39,e19 // A9 ; ::_thesis: contradiction consider d19, d29 being 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; ::_thesis: verum end; then consider c39 being 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 being 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 ; ::_thesis: contradiction 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, AFF_1: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; ::_thesis: verum end; assume A150: a29,e19 // A9 ; ::_thesis: contradiction A151: o9,a39 // o9,a39 by AFF_1:2; o9,c39 // A9 by A130, A131, A143, AFF_1:40, AFF_1: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; ::_thesis: verum end; then consider c29 being 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 being 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 ; ::_thesis: contradiction 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, AFF_1: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; ::_thesis: verum end; assume A160: a19,e19 // A9 ; ::_thesis: contradiction A161: o9,a39 // o9,a39 by AFF_1:2; o9,c39 // A9 by A130, A131, A143, AFF_1:40, AFF_1: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; ::_thesis: verum end; then consider c19 being 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__::_thesis:_not_o_=_c3 assume o = c3 ; ::_thesis: contradiction then A169: a3,b2 // b3,o by A166, ANALMETR:36; b39,o9 // b29,b39 by A9, A11, A12, A22, AFF_1:39, AFF_1: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; ::_thesis: verum end; A170: now__::_thesis:_(_not_o_=_c2_&_not_o_=_c1_) a29,o9 // a29,a39 by A5, A7, A8, A21, AFF_1:39, AFF_1:41; then A171: a2,o // a2,a3 by ANALMETR:36; assume ( o = c2 or o = c1 ) ; ::_thesis: contradiction 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, AFF_1: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; ::_thesis: verum end; assume ( o = c3 or o = c2 or o = c1 ) ; ::_thesis: contradiction hence contradiction by A168, A170; ::_thesis: verum end; A174: not c3 in N proof A175: o9,c39 // o9,c39 by AFF_1:2; assume c3 in N ; ::_thesis: contradiction 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; ::_thesis: verum end; A176: not LIN a1,a2,c1 proof assume LIN a1,a2,c1 ; ::_thesis: contradiction 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; ::_thesis: verum end; A178: ( not LIN a3,a1,c3 & not LIN a3,a2,c3 ) proof assume ( LIN a3,a1,c3 or LIN a3,a2,c3 ) ; ::_thesis: contradiction 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; ::_thesis: verum end; A180: not b2 in A proof A181: o9,b29 // o9,b29 by AFF_1:2; assume b2 in A ; ::_thesis: contradiction 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; ::_thesis: verum 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; assume c19 = c29 ; ::_thesis: contradiction 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; ::_thesis: verum end; assume LIN c1,c2,b2 ; ::_thesis: contradiction then LIN c19,c29,b29 by ANALMETR:40; hence contradiction by A130, A152, A162, A180, A183, AFF_1:25; ::_thesis: verum end; o9,c19 // o9,c29 by A130, A131, A152, A162, AFF_1:39, AFF_1: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 ; ::_thesis: contradiction 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; ::_thesis: verum 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, AFF_1: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, AFF_1: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 a1,b2 // a2,b3 by A2, A5, A13, A15, A16, A18, A167, A118, A120, A187, A176, A182, A189, CONAFFM:def_1; ::_thesis: verum end; hence a1,b2 // a2,b3 by A40; ::_thesis: verum end; A191: now__::_thesis:_(_a1_=_a3_implies_a1,b2_//_a2,b3_) A192: not LIN o9,a39,b39 proof assume LIN o9,a39,b39 ; ::_thesis: contradiction then LIN o9,b39,a39 by AFF_1:6; hence contradiction by A9, A12, A14, A18, A22, AFF_1:25; ::_thesis: verum end; o9,b39 // o9,b19 by A9, A10, A12, A22, AFF_1:39, AFF_1:41; then A193: LIN o9,b39,b19 by AFF_1:def_1; assume A194: a1 = a3 ; ::_thesis: a1,b2 // a2,b3 then a39,b39 // a39,b19 by A20, ANALMETR:36; hence a1,b2 // a2,b3 by A19, A194, A192, A193, AFF_1:14; ::_thesis: verum end; A195: now__::_thesis:_(_a1_=_a2_implies_a1,b2_//_a2,b3_) o9,b29 // o9,b39 by A9, A11, A12, A22, AFF_1:39, AFF_1:41; then A196: LIN o9,b29,b39 by AFF_1:def_1; assume A197: a1 = a2 ; ::_thesis: a1,b2 // a2,b3 a1 <> b1 proof o9,a19 // o9,a39 by A5, A6, A8, A21, AFF_1:39, AFF_1:41; then A198: LIN o9,a19,a39 by AFF_1:def_1; assume a1 = b1 ; ::_thesis: contradiction hence contradiction by A9, A10, A14, A15, A22, A198, AFF_1:25; ::_thesis: verum 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, AFF_1:25; then a19,b29 // a29,b39 by A197, AFF_1:2; hence a1,b2 // a2,b3 by ANALMETR:36; ::_thesis: verum end; now__::_thesis:_(_a2_=_a3_implies_a1,b2_//_a2,b3_) o9,b29 // o9,b19 by A9, A10, A11, A22, AFF_1:39, AFF_1:41; then A199: LIN o9,b29,b19 by AFF_1:def_1; assume A200: a2 = a3 ; ::_thesis: a1,b2 // a2,b3 then a39,b29 // a39,b19 by A19, ANALMETR:36; then b29 = b19 by A5, A8, A9, A13, A14, A21, A199, AFF_1:14, AFF_1:25; hence a1,b2 // a2,b3 by A20, A200, ANALMETR:59; ::_thesis: verum end; hence a1,b2 // a2,b3 by A195, A191, A24; ::_thesis: verum end; hence a1,b2 // a2,b3 by A1, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, Def1; ::_thesis: verum end; theorem :: CONMETR:14 for X being OrtAfPl st X is satisfying_MH1 & X is satisfying_MH2 holds X is satisfying_OPAP proof let X be OrtAfPl; ::_thesis: ( X is satisfying_MH1 & X is satisfying_MH2 implies X is satisfying_OPAP ) assume A1: X is satisfying_MH1 ; ::_thesis: ( not X is satisfying_MH2 or X is satisfying_OPAP ) assume A2: X is satisfying_MH2 ; ::_thesis: X is satisfying_OPAP let o be Element of X; :: according to CONMETR:def_1 ::_thesis: for a1, a2, a3, b1, b2, b3 being Element of X for M, N being Subset of X 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 let a1, a2, a3, b1, b2, b3 be Element of X; ::_thesis: for M, N being Subset of X 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 let M, N be Subset of X; ::_thesis: ( 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 implies a1,b2 // a2,b3 ) 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 ; ::_thesis: a1,b2 // a2,b3 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__::_thesis:_(_a1_<>_a2_&_a2_<>_a3_&_a1_<>_a3_implies_ex_d4_being_Element_of_X_st_a1,b2_//_a2,b3_) consider e1 being Element of X such that A23: o,a3 // o,e1 and A24: o <> e1 by ANALMETR:39; consider d1 being Element of X 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 being 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 ; ::_thesis: ex d4 being Element of X st a1,b2 // a2,b3 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, AFF_1: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, AFF_1:41; then A38: LIN o9,a29,a39 by AFF_1:def_1; assume LIN o9,b19,a29 ; ::_thesis: contradiction then a29 in N9 by A7, A8, A16, A20, AFF_1:25; hence contradiction by A7, A12, A15, A20, A38, AFF_1:25; ::_thesis: verum end; assume b2 = b3 ; ::_thesis: contradiction 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, AFF_1:41; then LIN o9,a29,a19 by AFF_1:def_1; hence contradiction by A29, A37, A39, AFF_1:14; ::_thesis: verum end; A40: not LIN b2,a3,b3 proof assume LIN b2,a3,b3 ; ::_thesis: contradiction 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; ::_thesis: verum end; A41: a3 <> b3 proof assume a3 = b3 ; ::_thesis: contradiction then LIN b29,a39,b39 by AFF_1:7; hence contradiction by A40, ANALMETR:40; ::_thesis: verum end; b29,b39 // b29,b19 by A8, A9, A10, A33, AFF_1:39, AFF_1: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, AFF_1: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 ; ::_thesis: contradiction then LIN a39,a19,b29 by ANALMETR:40; hence contradiction by A4, A6, A11, A30, A43, AFF_1:25; ::_thesis: verum end; A47: a3 <> b2 proof assume a3 = b2 ; ::_thesis: contradiction then LIN a39,a19,b29 by AFF_1:7; hence contradiction by A46, ANALMETR:40; ::_thesis: verum 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; then not o9,e19 // d19,e29 by ANALMETR:36; then consider d29 being 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 being Element of X such that A59: o,b3 // o,e1 and A60: o <> e1 by ANALMETR:39; consider e2 being 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; then not o9,e19 // d29,e29 by ANALMETR:36; then consider d39 being 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 being Element of X such that A72: a3,b2 _|_ d3,e2 and A73: d3 <> e2 by ANALMETR:39; consider e1 being 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; then not o9,e19 // d39,e29 by ANALMETR:36; then consider d49 being 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; A91: not LIN d1,d2,d3 proof A92: d2 <> d3 proof assume d2 = d3 ; ::_thesis: contradiction 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; ::_thesis: verum end; A94: d1 <> d2 proof assume d1 = d2 ; ::_thesis: contradiction 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; ::_thesis: verum end; assume LIN d1,d2,d3 ; ::_thesis: contradiction 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 ; ::_thesis: contradiction then LIN a39,a19,b29 by AFF_1:7; hence contradiction by A46, ANALMETR:40; ::_thesis: verum 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; ::_thesis: verum end; A100: d2 <> d4 proof A101: d2 <> d3 proof assume d2 = d3 ; ::_thesis: contradiction then LIN d19,d29,d39 by AFF_1:7; hence contradiction by A91, ANALMETR:40; ::_thesis: verum end; assume d2 = d4 ; ::_thesis: contradiction 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; ::_thesis: verum 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 being Subset of (Af X) 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 ; ::_thesis: contradiction then LIN d19,d29,d39 by AFF_1:7; hence contradiction by A91, ANALMETR:40; ::_thesis: verum 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, AFF_1:25; A111: o <> d3 proof assume d3 = o ; ::_thesis: contradiction 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; ::_thesis: verum 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; A117: not LIN d1,d4,d3 proof A118: d1 <> d3 proof A119: d1 <> d2 proof assume d1 = d2 ; ::_thesis: contradiction 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; ::_thesis: verum end; assume d1 = d3 ; ::_thesis: contradiction 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 ; ::_thesis: contradiction then LIN a39,a19,b29 by AFF_1:7; hence contradiction by A46, ANALMETR:40; ::_thesis: verum 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; ::_thesis: verum end; assume LIN d1,d4,d3 ; ::_thesis: contradiction 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 ; ::_thesis: contradiction then LIN b29,a39,b39 by AFF_1:7; hence contradiction by A40, ANALMETR:40; ::_thesis: verum 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; ::_thesis: verum end; A130: not d4 in A proof assume d4 in A ; ::_thesis: contradiction then d19,d49 // d19,d39 by A103, A104, A105, AFF_1:39, AFF_1:41; then LIN d19,d49,d39 by AFF_1:def_1; hence contradiction by A117, ANALMETR:40; ::_thesis: verum end; A131: d2,d3 _|_ b3,a3 by A61, A62, A66, ANALMETR:62; take d4 = d4; ::_thesis: a1,b2 // a2,b3 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 being Subset of (Af X) 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, AFF_1:25; a39,a19 // a39,a29 by A4, A5, A6, A43, AFF_1:39, AFF_1: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 ; ::_thesis: contradiction then LIN b29,a39,b39 by AFF_1:7; hence contradiction by A40, ANALMETR:40; ::_thesis: verum 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 ; ::_thesis: contradiction then LIN a39,a19,b29 by AFF_1:7; hence contradiction by A46, ANALMETR:40; ::_thesis: verum 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 ( LIN d1,d3,b3 & LIN d1,d3,b1 & LIN d2,d4,a1 & LIN d2,d4,a2 ) by A102, A133, A145, ANALMETR:40; ::_thesis: verum 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 ; ::_thesis: contradiction then d19,d29 // d19,d39 by A103, A104, A105, AFF_1:39, AFF_1:41; then LIN d19,d29,d39 by AFF_1:def_1; hence contradiction by A91, ANALMETR:40; ::_thesis: verum 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 being Subset of (Af X) 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 ; ::_thesis: contradiction then LIN d19,d29,d39 by AFF_1:7; hence contradiction by A91, ANALMETR:40; ::_thesis: verum 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 ; ::_thesis: contradiction then d19,d29 // d19,d39 by A157, A158, A159, AFF_1:39, AFF_1:41; then d1,d2 // d1,d3 by ANALMETR:36; hence contradiction by A91, ANALMETR:def_10; ::_thesis: verum 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; A171: not d4 in A proof assume d4 in A ; ::_thesis: contradiction then d19,d49 // d19,d39 by A157, A158, A159, AFF_1:39, AFF_1:41; then d1,d4 // d1,d3 by ANALMETR:36; hence contradiction by A117, ANALMETR:def_10; ::_thesis: verum end; LIN d29,d49,a19 by A140, ANALMETR:40; then consider K9 being Subset of (Af X) 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 a1,b2 // a2,b3 by ANALMETR:36; ::_thesis: verum end; now__::_thesis:_(_(_a1_=_a2_or_a2_=_a3_or_a1_=_a3_)_implies_a1,b2_//_a2,b3_) A179: now__::_thesis:_(_a1_=_a2_implies_a1,b2_//_a2,b3_) o9,b29 // o9,b39 by A7, A9, A10, A20, AFF_1:39, AFF_1:41; then A180: LIN o9,b29,b39 by AFF_1:def_1; assume A181: a1 = a2 ; ::_thesis: a1,b2 // a2,b3 a1 <> b1 proof o9,a19 // o9,a39 by A3, A4, A6, A21, AFF_1:39, AFF_1:41; then A182: LIN o9,a19,a39 by AFF_1:def_1; assume a1 = b1 ; ::_thesis: contradiction hence contradiction by A7, A8, A12, A14, A20, A182, AFF_1:25; ::_thesis: verum 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, AFF_1:25; then a19,b29 // a29,b39 by A181, AFF_1:2; hence a1,b2 // a2,b3 by ANALMETR:36; ::_thesis: verum end; A183: now__::_thesis:_(_a1_=_a3_implies_a1,b2_//_a2,b3_) A184: not LIN o9,a39,b19 proof assume LIN o9,a39,b19 ; ::_thesis: contradiction then LIN o9,b19,a39 by AFF_1:6; hence contradiction by A7, A8, A12, A16, A20, AFF_1:25; ::_thesis: verum end; o9,b19 // o9,b39 by A7, A8, A10, A20, AFF_1:39, AFF_1:41; then A185: LIN o9,b19,b39 by AFF_1:def_1; assume A186: a1 = a3 ; ::_thesis: a1,b2 // a2,b3 then a3,b1 // a3,b3 by A19, ANALMETR:59; then a39,b19 // a39,b39 by ANALMETR:36; hence a1,b2 // a2,b3 by A18, A186, A184, A185, AFF_1:14; ::_thesis: verum end; A187: now__::_thesis:_(_a2_=_a3_implies_a1,b2_//_a2,b3_) A188: not LIN o9,a39,b19 proof assume LIN o9,a39,b19 ; ::_thesis: contradiction then LIN o9,b19,a39 by AFF_1:6; hence contradiction by A7, A8, A12, A16, A20, AFF_1:25; ::_thesis: verum end; o9,b19 // o9,b29 by A7, A8, A9, A20, AFF_1:39, AFF_1:41; then A189: LIN o9,b19,b29 by AFF_1:def_1; assume A190: a2 = a3 ; ::_thesis: a1,b2 // a2,b3 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 a1,b2 // a2,b3 by ANALMETR:59; ::_thesis: verum end; assume ( a1 = a2 or a2 = a3 or a1 = a3 ) ; ::_thesis: a1,b2 // a2,b3 hence a1,b2 // a2,b3 by A179, A187, A183; ::_thesis: verum end; hence a1,b2 // a2,b3 by A22; ::_thesis: verum end; theorem :: CONMETR:15 for X being OrtAfPl st X is satisfying_3H holds X is satisfying_OPAP proof let X be OrtAfPl; ::_thesis: ( X is satisfying_3H implies X is satisfying_OPAP ) assume A1: X is satisfying_3H ; ::_thesis: X is satisfying_OPAP let o be Element of X; :: according to CONMETR:def_1 ::_thesis: for a1, a2, a3, b1, b2, b3 being Element of X for M, N being Subset of X 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 let a1, a2, a3, b1, b2, b3 be Element of X; ::_thesis: for M, N being Subset of X 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 let M, N be Subset of X; ::_thesis: ( 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 implies a1,b2 // a2,b3 ) 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 ; ::_thesis: a1,b2 // a2,b3 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__::_thesis:_(_b2_=_b3_implies_a1,b2_//_a2,b3_) A22: not LIN o9,b19,a19 proof o9,a19 // o9,a39 by A2, A3, A5, A20, AFF_1:39, AFF_1:41; then A23: LIN o9,a19,a39 by AFF_1:def_1; assume LIN o9,b19,a19 ; ::_thesis: contradiction then a19 in N9 by A6, A7, A15, A19, AFF_1:25; hence contradiction by A6, A11, A13, A19, A23, AFF_1:25; ::_thesis: verum end; A24: b1,a2 // a3,b2 by A17, ANALMETR:59; o9,a19 // o9,a29 by A2, A3, A4, A20, AFF_1:39, AFF_1:41; then A25: LIN o9,a19,a29 by AFF_1:def_1; assume A26: b2 = b3 ; ::_thesis: a1,b2 // a2,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 a1,b2 // a2,b3 by ANALMETR:36; ::_thesis: verum end; A27: for a, b, c being Element of X st LIN a,b,c holds ( LIN a,c,b & LIN b,a,c & LIN b,c,a & LIN c,a,b & LIN c,b,a ) proof let a, b, c be Element of X; ::_thesis: ( 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 ) ) reconsider a9 = a, b9 = b, c9 = c as Element of (Af X) by ANALMETR:35; assume LIN a,b,c ; ::_thesis: ( LIN a,c,b & LIN b,a,c & LIN b,c,a & LIN c,a,b & LIN c,b,a ) 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 ( LIN a,c,b & LIN b,a,c & LIN b,c,a & LIN c,a,b & LIN c,b,a ) by A29, A31, A30, A32, ANALMETR:40; ::_thesis: verum end; A33: now__::_thesis:_(_a1_<>_a3_&_b2_<>_b3_implies_a1,b2_//_a2,b3_) o9,a39 // o9,a19 by A2, A3, A5, A20, AFF_1:39, AFF_1: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, AFF_1: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, AFF_1: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 ; ::_thesis: a1,b2 // a2,b3 A39: ( not LIN a3,a1,b2 & not LIN b2,a3,b3 ) proof assume ( LIN a3,a1,b2 or LIN b2,a3,b3 ) ; ::_thesis: contradiction 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; ::_thesis: verum end; b29,b39 // b29,b19 by A7, A8, A9, A19, AFF_1:39, AFF_1:41; then LIN b29,b39,b19 by AFF_1:def_1; then A40: LIN b2,b3,b1 by ANALMETR:40; A41: now__::_thesis:_(_b2_<>_b1_implies_a1,b2_//_a2,b3_) assume A42: b2 <> b1 ; ::_thesis: a1,b2 // a2,b3 not LIN a2,a3,b3 proof A43: a3 <> a2 proof assume a3 = a2 ; ::_thesis: contradiction 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; ::_thesis: verum 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 ; ::_thesis: contradiction then LIN a39,a19,b29 by AFF_1:7; hence contradiction by A39, ANALMETR:40; ::_thesis: verum end; assume LIN a2,a3,b3 ; ::_thesis: contradiction 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; ::_thesis: verum end; then consider c1 being Element of X 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__::_thesis:_(_a2_<>_a1_implies_a1,b2_//_a2,b3_) A54: a2 <> a3 proof A55: not LIN o9,a39,b19 proof assume LIN o9,a39,b19 ; ::_thesis: contradiction then LIN o9,b19,a39 by AFF_1:6; hence contradiction by A6, A7, A11, A15, A19, AFF_1:25; ::_thesis: verum end; assume a2 = a3 ; ::_thesis: contradiction 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, AFF_1:41; then LIN o9,b19,b29 by AFF_1:def_1; hence contradiction by A42, A55, A56, AFF_1:14; ::_thesis: verum 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; o9,a29 // o9,a39 by A2, A4, A5, A20, AFF_1:39, AFF_1:41; then A61: LIN o9,a29,a39 by AFF_1:def_1; assume LIN o9,a29,c19 ; ::_thesis: contradiction 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; ::_thesis: verum end; A62: a1 <> b1 proof o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41; then A63: LIN o9,b19,b29 by AFF_1:def_1; assume a1 = b1 ; ::_thesis: contradiction hence contradiction by A2, A3, A10, A13, A20, A63, AFF_1:25; ::_thesis: verum end; assume A64: a2 <> a1 ; ::_thesis: a1,b2 // a2,b3 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 ; ::_thesis: contradiction then a3,a1 // a3,b2 by A17, A64, A66, ANALMETR:60; hence contradiction by A39, ANALMETR:def_10; ::_thesis: verum end; not LIN a2,a1,b1 proof assume LIN a2,a1,b1 ; ::_thesis: contradiction 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, AFF_1:41; then A68: LIN o9,b19,b29 by AFF_1:def_1; assume a2 = b1 ; ::_thesis: contradiction hence contradiction by A2, A4, A10, A14, A20, A68, AFF_1:25; ::_thesis: verum 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; ::_thesis: verum end; then consider c2 being Element of X 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, AFF_1:41; then A77: LIN o9,b19,b29 by AFF_1:def_1; assume a2 = b1 ; ::_thesis: contradiction hence contradiction by A2, A4, A10, A14, A20, A77, AFF_1:25; ::_thesis: verum end; assume o9 = c29 ; ::_thesis: contradiction 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; ::_thesis: verum end; o9,a19 // o9,a39 by A2, A3, A5, A20, AFF_1:39, AFF_1:41; then A79: LIN o9,a19,a39 by AFF_1:def_1; assume LIN o9,a19,c29 ; ::_thesis: contradiction 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; ::_thesis: verum end; not LIN a3,a1,b2 proof assume LIN a3,a1,b2 ; ::_thesis: contradiction then LIN a39,a19,b29 by ANALMETR:40; hence contradiction by A3, A5, A10, A20, A37, AFF_1:25; ::_thesis: verum end; then consider c3 being Element of X 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, AFF_1:41; then A83: LIN o9,b19,b29 by AFF_1:def_1; assume a2 = b1 ; ::_thesis: contradiction hence contradiction by A2, A4, A10, A14, A20, A83, AFF_1:25; ::_thesis: verum 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, AFF_1: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 ; ::_thesis: contradiction then LIN o9,b19,a39 by AFF_1:6; hence contradiction by A6, A7, A11, A15, A19, AFF_1:25; ::_thesis: verum end; assume a2 = a3 ; ::_thesis: contradiction 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, AFF_1:41; then LIN o9,b19,b29 by AFF_1:def_1; hence contradiction by A42, A88, A89, AFF_1:14; ::_thesis: verum end; assume A90: c1 = a3 ; ::_thesis: contradiction 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; ::_thesis: verum 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, AFF_1:41; then LIN o9,c29,c39 by AFF_1:def_1; then c2 = c3 by A74, A84, AFF_1:14; hence a1,b2 // a2,b3 by A51, A85, A80, A86, ANALMETR:63; ::_thesis: verum end; now__::_thesis:_(_a2_=_a1_implies_a1,b2_//_a2,b3_) o9,b29 // o9,b39 by A6, A8, A9, A19, AFF_1:39, AFF_1:41; then A91: LIN o9,b29,b39 by AFF_1:def_1; assume A92: a2 = a1 ; ::_thesis: a1,b2 // a2,b3 a1 <> b1 proof o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41; then A93: LIN o9,b19,b29 by AFF_1:def_1; assume a1 = b1 ; ::_thesis: contradiction hence contradiction by A2, A3, A10, A13, A20, A93, AFF_1:25; ::_thesis: verum 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, AFF_1:25; then a19,b29 // a29,b39 by A92, AFF_1:2; hence a1,b2 // a2,b3 by ANALMETR:36; ::_thesis: verum end; hence a1,b2 // a2,b3 by A53; ::_thesis: verum end; now__::_thesis:_(_b2_=_b1_implies_a1,b2_//_a2,b3_) A94: not LIN o9,b29,a39 proof assume LIN o9,b29,a39 ; ::_thesis: contradiction 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; ::_thesis: verum 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 ; ::_thesis: contradiction then LIN a39,a19,b29 by AFF_1:7; hence contradiction by A39, ANALMETR:40; ::_thesis: verum 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 ; ::_thesis: a1,b2 // a2,b3 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 a1,b2 // a2,b3 by A18, A99, ANALMETR:59; ::_thesis: verum end; hence a1,b2 // a2,b3 by A41; ::_thesis: verum end; now__::_thesis:_(_a1_=_a3_implies_a1,b2_//_a2,b3_) A100: not LIN o9,a19,b19 proof o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41; then A101: LIN o9,b19,b29 by AFF_1:def_1; assume LIN o9,a19,b19 ; ::_thesis: contradiction then b19 in M9 by A2, A3, A13, A20, AFF_1:25; hence contradiction by A2, A10, A15, A20, A101, AFF_1:25; ::_thesis: verum end; o9,b19 // o9,b39 by A6, A7, A9, A19, AFF_1:39, AFF_1:41; then A102: LIN o9,b19,b39 by AFF_1:def_1; assume A103: a1 = a3 ; ::_thesis: a1,b2 // a2,b3 then a1,b1 // a1,b3 by A18, ANALMETR:59; then a19,b19 // a19,b39 by ANALMETR:36; hence a1,b2 // a2,b3 by A17, A103, A100, A102, AFF_1:14; ::_thesis: verum end; hence a1,b2 // a2,b3 by A21, A33; ::_thesis: verum end;