:: AFF_3 semantic presentation begin definition let AP be AffinPlane; attrAP is satisfying_DES1 means :Def1: :: AFF_3:def 1 for A, P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds a,c // p,q; end; :: deftheorem Def1 defines satisfying_DES1 AFF_3:def_1_:_ for AP being AffinPlane holds ( AP is satisfying_DES1 iff for A, P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds a,c // p,q ); definition let AP be AffinPlane; attrAP is satisfying_DES1_1 means :Def2: :: AFF_3:def 2 for A, P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & c <> q & not LIN b,a,c & not LIN b9,a9,c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds a,c // a9,c9; end; :: deftheorem Def2 defines satisfying_DES1_1 AFF_3:def_2_:_ for AP being AffinPlane holds ( AP is satisfying_DES1_1 iff for A, P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & c <> q & not LIN b,a,c & not LIN b9,a9,c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds a,c // a9,c9 ); definition let AP be AffinPlane; attrAP is satisfying_DES1_2 means :Def3: :: AFF_3:def 3 for A, P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds o in C; end; :: deftheorem Def3 defines satisfying_DES1_2 AFF_3:def_3_:_ for AP being AffinPlane holds ( AP is satisfying_DES1_2 iff for A, P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds o in C ); definition let AP be AffinPlane; attrAP is satisfying_DES1_3 means :Def4: :: AFF_3:def 4 for A, P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & b <> b9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds o in P; end; :: deftheorem Def4 defines satisfying_DES1_3 AFF_3:def_4_:_ for AP being AffinPlane holds ( AP is satisfying_DES1_3 iff for A, P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & b <> b9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds o in P ); definition let AP be AffinPlane; attrAP is satisfying_DES2 means :Def5: :: AFF_3:def 5 for A, P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds a,c // p,q; end; :: deftheorem Def5 defines satisfying_DES2 AFF_3:def_5_:_ for AP being AffinPlane holds ( AP is satisfying_DES2 iff for A, P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds a,c // p,q ); definition let AP be AffinPlane; attrAP is satisfying_DES2_1 means :Def6: :: AFF_3:def 6 for A, P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds a,c // a9,c9; end; :: deftheorem Def6 defines satisfying_DES2_1 AFF_3:def_6_:_ for AP being AffinPlane holds ( AP is satisfying_DES2_1 iff for A, P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds a,c // a9,c9 ); definition let AP be AffinPlane; attrAP is satisfying_DES2_2 means :Def7: :: AFF_3:def 7 for A, P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds A // P; end; :: deftheorem Def7 defines satisfying_DES2_2 AFF_3:def_7_:_ for AP being AffinPlane holds ( AP is satisfying_DES2_2 iff for A, P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds A // P ); definition let AP be AffinPlane; attrAP is satisfying_DES2_3 means :Def8: :: AFF_3:def 8 for A, P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds A // C; end; :: deftheorem Def8 defines satisfying_DES2_3 AFF_3:def_8_:_ for AP being AffinPlane holds ( AP is satisfying_DES2_3 iff for A, P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds A // C ); theorem :: AFF_3:1 for AP being AffinPlane st AP is satisfying_DES1 holds AP is satisfying_DES1_1 proof let AP be AffinPlane; ::_thesis: ( AP is satisfying_DES1 implies AP is satisfying_DES1_1 ) assume A1: AP is satisfying_DES1 ; ::_thesis: AP is satisfying_DES1_1 let A be Subset of AP; :: according to AFF_3:def_2 ::_thesis: for P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & c <> q & not LIN b,a,c & not LIN b9,a9,c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds a,c // a9,c9 let P, C be Subset of AP; ::_thesis: for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & c <> q & not LIN b,a,c & not LIN b9,a9,c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds a,c // a9,c9 let o, a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & c <> q & not LIN b,a,c & not LIN b9,a9,c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q implies a,c // a9,c9 ) assume that A2: A is being_line and A3: P is being_line and A4: C is being_line and A5: P <> A and A6: P <> C and A7: A <> C and A8: o in A and A9: a in A and A10: a9 in A and A11: o in P and A12: ( b in P & b9 in P ) and A13: ( o in C & c in C ) and A14: c9 in C and A15: o <> a and A16: o <> b and A17: o <> c and A18: p <> q and A19: c <> q and A20: not LIN b,a,c and A21: not LIN b9,a9,c9 and A22: LIN b,a,p and A23: LIN b9,a9,p and A24: LIN b,c,q and A25: LIN b9,c9,q and A26: a,c // p,q ; ::_thesis: a,c // a9,c9 A27: ( LIN o,a,a9 & LIN b9,p,a9 ) by A2, A8, A9, A10, A23, AFF_1:6, AFF_1:21; set K = Line (b,a); A28: a in Line (b,a) by AFF_1:15; then A29: Line (b,a) <> P by A2, A3, A5, A8, A9, A11, A15, AFF_1:18; A30: not LIN o,a,c proof assume LIN o,a,c ; ::_thesis: contradiction then c in A by A2, A8, A9, A15, AFF_1:25; hence contradiction by A2, A4, A7, A8, A13, A17, AFF_1:18; ::_thesis: verum end; A31: p in Line (b,a) by A22, AFF_1:def_2; A32: ( LIN o,c,c9 & LIN b9,q,c9 ) by A4, A13, A14, A25, AFF_1:6, AFF_1:21; A33: ( b <> c & a <> p ) by A19, A20, A24, A26, AFF_1:7, AFF_1:14; A34: ( a9 <> c9 & b <> a ) by A20, A21, AFF_1:7; b <> a by A20, AFF_1:7; then A35: Line (b,a) is being_line by AFF_1:def_3; set M = Line (b,c); A36: c in Line (b,c) by AFF_1:15; then A37: Line (b,c) <> P by A3, A4, A6, A11, A13, A17, AFF_1:18; b <> c by A20, AFF_1:7; then A38: Line (b,c) is being_line by AFF_1:def_3; A39: ( b in Line (b,c) & q in Line (b,c) ) by A24, AFF_1:15, AFF_1:def_2; q <> b proof assume A40: q = b ; ::_thesis: contradiction ( not LIN b,c,a & c,a // q,p ) by A20, A26, AFF_1:4, AFF_1:6; hence contradiction by A18, A22, A40, AFF_1:55; ::_thesis: verum end; then A41: q <> b9 by A3, A12, A38, A39, A37, AFF_1:18; A42: b in Line (b,a) by AFF_1:15; p <> b by A18, A20, A24, A26, AFF_1:55; then A43: p <> b9 by A3, A12, A35, A42, A31, A29, AFF_1:18; A44: not LIN b9,p,q proof set N = Line (p,q); A45: Line (p,q) is being_line by A18, AFF_1:def_3; assume LIN b9,p,q ; ::_thesis: contradiction then LIN p,q,b9 by AFF_1:6; then A46: b9 in Line (p,q) by AFF_1:def_2; ( q in Line (p,q) & LIN q,b9,c9 ) by A25, AFF_1:6, AFF_1:15; then A47: c9 in Line (p,q) by A41, A45, A46, AFF_1:25; ( p in Line (p,q) & LIN p,b9,a9 ) by A23, AFF_1:6, AFF_1:15; then a9 in Line (p,q) by A43, A45, A46, AFF_1:25; hence contradiction by A21, A45, A46, A47, AFF_1:21; ::_thesis: verum end; Line (b,a) <> Line (b,c) by A20, A35, A42, A28, A36, AFF_1:21; hence a,c // a9,c9 by A1, A3, A11, A12, A16, A26, A35, A38, A42, A28, A36, A31, A39, A37, A29, A34, A30, A44, A33, A27, A32, Def1; ::_thesis: verum end; theorem :: AFF_3:2 for AP being AffinPlane st AP is satisfying_DES1_1 holds AP is satisfying_DES1 proof let AP be AffinPlane; ::_thesis: ( AP is satisfying_DES1_1 implies AP is satisfying_DES1 ) assume A1: AP is satisfying_DES1_1 ; ::_thesis: AP is satisfying_DES1 let A be Subset of AP; :: according to AFF_3:def_1 ::_thesis: for P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds a,c // p,q let P, C be Subset of AP; ::_thesis: for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds a,c // p,q let o, a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 implies a,c // p,q ) assume that A2: A is being_line and A3: P is being_line and A4: C is being_line and A5: P <> A and A6: P <> C and A7: A <> C and A8: o in A and A9: a in A and A10: a9 in A and A11: o in P and A12: b in P and A13: b9 in P and A14: o in C and A15: c in C and A16: c9 in C and A17: o <> a and A18: o <> b and A19: o <> c and A20: p <> q and A21: not LIN b,a,c and A22: not LIN b9,a9,c9 and A23: a <> a9 and A24: LIN b,a,p and A25: LIN b9,a9,p and A26: LIN b,c,q and A27: LIN b9,c9,q and A28: a,c // a9,c9 ; ::_thesis: a,c // p,q A29: a9 <> b9 by A22, AFF_1:7; set M = Line (b,c); A30: c in Line (b,c) by AFF_1:15; then A31: Line (b,c) <> P by A3, A4, A6, A11, A14, A15, A19, AFF_1:18; A32: Line (b,c) <> P by A3, A4, A6, A11, A14, A15, A19, A30, AFF_1:18; A33: b in Line (b,c) by AFF_1:15; set K = Line (b,a); A34: a in Line (b,a) by AFF_1:15; then A35: Line (b,a) <> P by A2, A3, A5, A8, A9, A11, A17, AFF_1:18; A36: p in Line (b,a) by A24, AFF_1:def_2; A37: ( a9 <> c9 & b <> a ) by A21, A22, AFF_1:7; A38: b <> c by A21, AFF_1:7; A39: q in Line (b,c) by A26, AFF_1:def_2; A40: b9 <> c9 by A22, AFF_1:7; A41: b in Line (b,a) by AFF_1:15; A42: not LIN o,a,c proof assume LIN o,a,c ; ::_thesis: contradiction then c in A by A2, A8, A9, A17, AFF_1:25; hence contradiction by A2, A4, A7, A8, A14, A15, A19, AFF_1:18; ::_thesis: verum end; A43: c <> c9 proof assume c = c9 ; ::_thesis: contradiction then A44: c,a // c,a9 by A28, AFF_1:4; ( LIN o,a,a9 & not LIN o,c,a ) by A2, A8, A9, A10, A42, AFF_1:6, AFF_1:21; hence contradiction by A23, A44, AFF_1:14; ::_thesis: verum end; b <> c by A21, AFF_1:7; then A45: Line (b,c) is being_line by AFF_1:def_3; b <> a by A21, AFF_1:7; then A46: Line (b,a) is being_line by AFF_1:def_3; A47: Line (b,a) <> P by A2, A3, A5, A8, A9, A11, A17, A34, AFF_1:18; A48: now__::_thesis:_(_LIN_b9,p,q_implies_a,c_//_p,q_) set C9 = Line (b9,c9); set A9 = Line (b9,a9); A49: c9 in Line (b9,c9) by AFF_1:15; A50: ( Line (b9,a9) is being_line & b9 in Line (b9,a9) ) by A29, AFF_1:15, AFF_1:def_3; A51: a9 in Line (b9,a9) by AFF_1:15; then A52: Line (b9,a9) <> Line (b9,c9) by A22, A50, A49, AFF_1:21; A53: q in Line (b9,c9) by A27, AFF_1:def_2; A54: p in Line (b9,a9) by A25, AFF_1:def_2; A55: ( Line (b9,c9) is being_line & b9 in Line (b9,c9) ) by A40, AFF_1:15, AFF_1:def_3; assume A56: LIN b9,p,q ; ::_thesis: a,c // p,q then A57: LIN b9,q,p by AFF_1:6; A58: now__::_thesis:_(_b9_<>_q_implies_a,c_//_p,q_) A59: Line (b9,c9) <> Line (b,c) proof assume Line (b9,c9) = Line (b,c) ; ::_thesis: contradiction then LIN c,c9,b by A45, A33, A30, A49, AFF_1:21; then b in C by A4, A15, A16, A43, AFF_1:25; hence contradiction by A3, A4, A6, A11, A12, A14, A18, AFF_1:18; ::_thesis: verum end; assume b9 <> q ; ::_thesis: a,c // p,q then A60: p in Line (b9,c9) by A57, A55, A53, AFF_1:25; then LIN b,a,b9 by A24, A50, A54, A55, A52, AFF_1:18; then b9 in Line (b,a) by AFF_1:def_2; then A61: b = b9 by A3, A12, A13, A46, A41, A47, AFF_1:18; p = b9 by A50, A54, A55, A52, A60, AFF_1:18; then p = q by A45, A33, A39, A55, A53, A61, A59, AFF_1:18; hence a,c // p,q by AFF_1:3; ::_thesis: verum end; now__::_thesis:_(_b9_<>_p_implies_a,c_//_p,q_) A62: Line (b9,a9) <> Line (b,a) proof assume Line (b9,a9) = Line (b,a) ; ::_thesis: contradiction then LIN a,a9,b by A46, A41, A34, A51, AFF_1:21; then b in A by A2, A9, A10, A23, AFF_1:25; hence contradiction by A2, A3, A5, A8, A11, A12, A18, AFF_1:18; ::_thesis: verum end; assume b9 <> p ; ::_thesis: a,c // p,q then A63: q in Line (b9,a9) by A56, A50, A54, AFF_1:25; then LIN b,c,b9 by A26, A50, A55, A53, A52, AFF_1:18; then b9 in Line (b,c) by AFF_1:def_2; then A64: b = b9 by A3, A12, A13, A45, A33, A32, AFF_1:18; q = b9 by A50, A55, A53, A52, A63, AFF_1:18; then p = q by A46, A41, A36, A50, A54, A64, A62, AFF_1:18; hence a,c // p,q by AFF_1:3; ::_thesis: verum end; hence a,c // p,q by A20, A58; ::_thesis: verum end; A65: Line (b,a) <> Line (b,c) by A21, A46, A41, A34, A30, AFF_1:21; now__::_thesis:_(_not_LIN_b9,p,q_implies_a,c_//_p,q_) A66: ( LIN o,c,c9 & LIN b9,q,c9 ) by A4, A14, A15, A16, A27, AFF_1:6, AFF_1:21; assume A67: not LIN b9,p,q ; ::_thesis: a,c // p,q ( LIN o,a,a9 & LIN b9,p,a9 ) by A2, A8, A9, A10, A25, AFF_1:6, AFF_1:21; hence a,c // p,q by A1, A3, A11, A12, A13, A18, A28, A46, A45, A41, A34, A33, A30, A36, A39, A31, A35, A37, A38, A65, A42, A43, A67, A66, Def2; ::_thesis: verum end; hence a,c // p,q by A48; ::_thesis: verum end; theorem :: AFF_3:3 for AP being AffinPlane st AP is Desarguesian holds AP is satisfying_DES1 proof let AP be AffinPlane; ::_thesis: ( AP is Desarguesian implies AP is satisfying_DES1 ) assume A1: AP is Desarguesian ; ::_thesis: AP is satisfying_DES1 let A be Subset of AP; :: according to AFF_3:def_1 ::_thesis: for P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds a,c // p,q let P, C be Subset of AP; ::_thesis: for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds a,c // p,q let o, a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 implies a,c // p,q ) assume that A2: A is being_line and A3: P is being_line and A4: C is being_line and A5: P <> A and A6: P <> C and A7: A <> C and A8: o in A and A9: a in A and A10: a9 in A and A11: o in P and A12: b in P and A13: b9 in P and A14: o in C and A15: c in C and A16: c9 in C and A17: o <> a and A18: o <> b and A19: o <> c and p <> q and A20: not LIN b,a,c and A21: not LIN b9,a9,c9 and A22: a <> a9 and A23: LIN b,a,p and A24: LIN b9,a9,p and A25: LIN b,c,q and A26: LIN b9,c9,q and A27: a,c // a9,c9 ; ::_thesis: a,c // p,q set D = Line (b,c); b <> c by A20, AFF_1:7; then Line (b,c) is being_line by AFF_1:def_3; then consider D9 being Subset of AP such that A28: c9 in D9 and A29: Line (b,c) // D9 by AFF_1:49; A30: D9 is being_line by A29, AFF_1:36; set M = Line (b9,c9); A31: q in Line (b9,c9) by A26, AFF_1:def_2; A32: b in Line (b,c) by AFF_1:15; A33: c in Line (b,c) by AFF_1:15; not D9 // P proof assume D9 // P ; ::_thesis: contradiction then Line (b,c) // P by A29, AFF_1:44; then c in P by A12, A32, A33, AFF_1:45; hence contradiction by A3, A4, A6, A11, A14, A15, A19, AFF_1:18; ::_thesis: verum end; then consider d being Element of AP such that A34: d in D9 and A35: d in P by A3, A30, AFF_1:58; A36: q in Line (b,c) by A25, AFF_1:def_2; then A37: d,c9 // b,q by A32, A28, A29, A34, AFF_1:39; A38: ( a <> b & b,a // b,p ) by A20, A23, AFF_1:7, AFF_1:def_1; A39: c,a // c9,a9 by A27, AFF_1:4; c,b // c9,d by A32, A33, A28, A29, A34, AFF_1:39; then b,a // d,a9 by A1, A2, A3, A4, A6, A7, A8, A9, A10, A11, A12, A14, A15, A16, A17, A18, A19, A35, A39, AFF_2:def_4; then A40: d,a9 // b,p by A38, AFF_1:5; set K = Line (b9,a9); A41: ( b9 in Line (b9,a9) & p in Line (b9,a9) ) by A24, AFF_1:15, AFF_1:def_2; A42: a9 <> b9 by A21, AFF_1:7; then A43: Line (b9,a9) is being_line by AFF_1:def_3; A44: b9 in Line (b9,c9) by AFF_1:15; A45: c9 in Line (b9,c9) by AFF_1:15; A46: b9 <> c9 by A21, AFF_1:7; then A47: Line (b9,c9) is being_line by AFF_1:def_3; A48: not LIN o,a,c proof assume LIN o,a,c ; ::_thesis: contradiction then c in A by A2, A8, A9, A17, AFF_1:25; hence contradiction by A2, A4, A7, A8, A14, A15, A19, AFF_1:18; ::_thesis: verum end; A49: c <> c9 proof assume c = c9 ; ::_thesis: contradiction then A50: c,a // c,a9 by A27, AFF_1:4; ( LIN o,a,a9 & not LIN o,c,a ) by A2, A8, A9, A10, A48, AFF_1:6, AFF_1:21; hence contradiction by A22, A50, AFF_1:14; ::_thesis: verum end; A51: d <> b9 proof assume d = b9 ; ::_thesis: contradiction then Line (b9,c9) = D9 by A46, A47, A44, A45, A28, A30, A34, AFF_1:18; then Line (b,c) = Line (b9,c9) by A31, A36, A29, AFF_1:45; then LIN c,c9,b by A47, A45, A32, A33, AFF_1:21; then b in C by A4, A15, A16, A49, AFF_1:25; hence contradiction by A3, A4, A6, A11, A12, A14, A18, AFF_1:18; ::_thesis: verum end; A52: a9 <> c9 by A21, AFF_1:7; A53: o <> a9 proof assume A54: o = a9 ; ::_thesis: contradiction LIN o,c,c9 by A4, A14, A15, A16, AFF_1:21; hence contradiction by A27, A52, A48, A54, AFF_1:55; ::_thesis: verum end; o <> c9 proof A55: not LIN o,c,a by A48, AFF_1:6; assume A56: o = c9 ; ::_thesis: contradiction ( LIN o,a,a9 & c,a // c9,a9 ) by A2, A8, A9, A10, A27, AFF_1:4, AFF_1:21; hence contradiction by A53, A56, A55, AFF_1:55; ::_thesis: verum end; then A57: Line (b9,c9) <> P by A3, A4, A6, A11, A14, A16, A45, AFF_1:18; A58: a9 in Line (b9,a9) by AFF_1:15; then Line (b9,a9) <> P by A2, A3, A5, A8, A10, A11, A53, AFF_1:18; then a9,c9 // p,q by A1, A3, A12, A13, A42, A46, A43, A47, A58, A41, A44, A45, A31, A57, A35, A51, A40, A37, AFF_2:def_4; hence a,c // p,q by A27, A52, AFF_1:5; ::_thesis: verum end; theorem :: AFF_3:4 for AP being AffinPlane st AP is Desarguesian holds AP is satisfying_DES1_2 proof let AP be AffinPlane; ::_thesis: ( AP is Desarguesian implies AP is satisfying_DES1_2 ) assume A1: AP is Desarguesian ; ::_thesis: AP is satisfying_DES1_2 then A2: AP is satisfying_DES_1 by AFF_2:2; let A be Subset of AP; :: according to AFF_3:def_3 ::_thesis: for P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds o in C let P, C be Subset of AP; ::_thesis: for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds o in C let o, a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q implies o in C ) assume that A3: A is being_line and A4: P is being_line and A5: C is being_line and A6: P <> A and A7: P <> C and A <> C and A8: o in A and A9: ( a in A & a9 in A ) and A10: o in P and A11: b in P and A12: b9 in P and A13: c in C and A14: c9 in C and A15: o <> a and A16: o <> b and o <> c and A17: p <> q and A18: not LIN b,a,c and A19: not LIN b9,a9,c9 and A20: c <> c9 and A21: LIN b,a,p and A22: LIN b9,a9,p and A23: LIN b,c,q and A24: LIN b9,c9,q and A25: a,c // a9,c9 and A26: a,c // p,q ; ::_thesis: o in C A27: b <> p by A17, A18, A23, A26, AFF_1:55; set K = Line (b9,a9); A28: p in Line (b9,a9) by A22, AFF_1:def_2; a9 <> b9 by A19, AFF_1:7; then A29: Line (b9,a9) is being_line by AFF_1:def_3; A30: b <> q proof assume A31: b = q ; ::_thesis: contradiction ( not LIN b,c,a & c,a // q,p ) by A18, A26, AFF_1:4, AFF_1:6; hence contradiction by A17, A21, A31, AFF_1:55; ::_thesis: verum end; set M = Line (b9,c9); A32: q in Line (b9,c9) by A24, AFF_1:def_2; A33: c9 in Line (b9,c9) by AFF_1:15; A34: a <> c by A18, AFF_1:7; A35: b9 <> p proof assume A36: b9 = p ; ::_thesis: contradiction a9,c9 // p,q by A25, A26, A34, AFF_1:5; hence contradiction by A17, A19, A24, A36, AFF_1:55; ::_thesis: verum end; A37: b9 <> q proof a9,c9 // p,q by A25, A26, A34, AFF_1:5; then A38: c9,a9 // q,p by AFF_1:4; assume A39: b9 = q ; ::_thesis: contradiction not LIN b9,c9,a9 by A19, AFF_1:6; hence contradiction by A17, A22, A39, A38, AFF_1:55; ::_thesis: verum end; A40: b <> c by A18, AFF_1:7; A41: a <> b by A18, AFF_1:7; A42: ( b9 <> a9 & b9 <> c9 ) by A19, AFF_1:7; A43: a9 in Line (b9,a9) by AFF_1:15; A44: b9 in Line (b9,c9) by AFF_1:15; A45: b9 <> c9 by A19, AFF_1:7; then A46: Line (b9,c9) is being_line by AFF_1:def_3; A47: b9 in Line (b9,a9) by AFF_1:15; then A48: Line (b9,a9) <> Line (b9,c9) by A19, A29, A43, A33, AFF_1:21; now__::_thesis:_o_in_C A49: now__::_thesis:_(_Line_(b9,c9)_<>_P_implies_o_in_C_) p,q // a9,c9 by A25, A26, A34, AFF_1:5; then A50: c9,a9 // q,p by AFF_1:4; A51: b,a // b,p by A21, AFF_1:def_1; set D = Line (b,c); A52: b in Line (b,c) by AFF_1:15; Line (b,c) is being_line by A40, AFF_1:def_3; then consider D9 being Subset of AP such that A53: c9 in D9 and A54: Line (b,c) // D9 by AFF_1:49; A55: D9 is being_line by A54, AFF_1:36; A56: q in Line (b,c) by A23, AFF_1:def_2; assume A57: Line (b9,c9) <> P ; ::_thesis: o in C not D9 // P proof assume D9 // P ; ::_thesis: contradiction then Line (b,c) // P by A54, AFF_1:44; then q in P by A11, A52, A56, AFF_1:45; hence contradiction by A4, A12, A46, A44, A32, A37, A57, AFF_1:18; ::_thesis: verum end; then consider d being Element of AP such that A58: d in D9 and A59: d in P by A4, A55, AFF_1:58; A60: c in Line (b,c) by AFF_1:15; A61: d <> b9 proof assume d = b9 ; ::_thesis: contradiction then Line (b9,c9) = D9 by A45, A46, A44, A33, A53, A55, A58, AFF_1:18; then A62: Line (b,c) = Line (b9,c9) by A32, A56, A54, AFF_1:45; then LIN c,c9,b by A46, A33, A52, A60, AFF_1:21; then A63: b in C by A5, A13, A14, A20, AFF_1:25; set N = Line (a,c); set T = Line (b,a); A64: b in Line (b,a) by AFF_1:15; A65: c in Line (a,c) by AFF_1:15; A66: a in Line (b,a) by AFF_1:15; A67: Line (a,c) is being_line by A34, AFF_1:def_3; A68: a in Line (a,c) by AFF_1:15; A69: a <> a9 proof assume a = a9 ; ::_thesis: contradiction then LIN a,c,c9 by A25, AFF_1:def_1; then c9 in Line (a,c) by AFF_1:def_2; then Line (a,c) = C by A5, A13, A14, A20, A67, A65, AFF_1:18; hence contradiction by A13, A18, A63, A67, A68, AFF_1:21; ::_thesis: verum end; A70: ( Line (b,a) is being_line & p in Line (b,a) ) by A21, A41, AFF_1:def_2, AFF_1:def_3; A71: b <> b9 proof A72: Line (b9,a9) <> Line (b,a) proof assume Line (b9,a9) = Line (b,a) ; ::_thesis: contradiction then Line (b,a) = A by A3, A9, A29, A43, A66, A69, AFF_1:18; hence contradiction by A3, A4, A6, A8, A10, A11, A16, A64, AFF_1:18; ::_thesis: verum end; assume b = b9 ; ::_thesis: contradiction hence contradiction by A29, A47, A28, A35, A64, A70, A72, AFF_1:18; ::_thesis: verum end; LIN c,c9,b9 by A46, A44, A33, A60, A62, AFF_1:21; then b9 in C by A5, A13, A14, A20, AFF_1:25; hence contradiction by A4, A5, A7, A11, A12, A63, A71, AFF_1:18; ::_thesis: verum end; c9,d // q,b by A52, A56, A53, A54, A58, AFF_1:39; then d,a9 // b,p by A1, A4, A11, A12, A42, A29, A46, A47, A43, A28, A44, A33, A32, A48, A57, A59, A61, A50, AFF_2:def_4; then A73: b,a // d,a9 by A27, A51, AFF_1:5; b,c // d,c9 by A52, A60, A53, A54, A58, AFF_1:39; hence o in C by A2, A3, A4, A5, A6, A8, A9, A10, A11, A13, A14, A15, A16, A18, A20, A25, A59, A73, AFF_2:def_5; ::_thesis: verum end; now__::_thesis:_(_Line_(b9,c9)_=_P_implies_o_in_C_) assume A74: Line (b9,c9) = P ; ::_thesis: o in C LIN b,q,c by A23, AFF_1:6; then c in P by A11, A46, A32, A30, A74, AFF_1:25; then P = Line (c,c9) by A20, A46, A33, A74, AFF_1:57; hence o in C by A5, A10, A13, A14, A20, AFF_1:57; ::_thesis: verum end; hence o in C by A49; ::_thesis: verum end; hence o in C ; ::_thesis: verum end; theorem :: AFF_3:5 for AP being AffinPlane st AP is satisfying_DES1_2 holds AP is satisfying_DES1_3 proof let AP be AffinPlane; ::_thesis: ( AP is satisfying_DES1_2 implies AP is satisfying_DES1_3 ) assume A1: AP is satisfying_DES1_2 ; ::_thesis: AP is satisfying_DES1_3 let A be Subset of AP; :: according to AFF_3:def_4 ::_thesis: for P, C being Subset of AP for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & b <> b9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds o in P let P, C be Subset of AP; ::_thesis: for o, a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & b <> b9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds o in P let o, a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & b <> b9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q implies o in P ) assume that A2: A is being_line and A3: P is being_line and A4: C is being_line and A5: P <> A and A6: P <> C and A7: A <> C and A8: o in A and A9: a in A and A10: a9 in A and A11: b in P and A12: b9 in P and A13: o in C and A14: c in C and A15: c9 in C and A16: o <> a and A17: o <> b and A18: o <> c and A19: p <> q and A20: not LIN b,a,c and A21: not LIN b9,a9,c9 and A22: b <> b9 and A23: a <> a9 and A24: LIN b,a,p and A25: LIN b9,a9,p and A26: LIN b,c,q and A27: LIN b9,c9,q and A28: a,c // a9,c9 and A29: a,c // p,q ; ::_thesis: o in P set D = Line (b,c); set K = Line (b9,a9); assume A30: not o in P ; ::_thesis: contradiction A31: not LIN o,c,a proof assume LIN o,c,a ; ::_thesis: contradiction then a in C by A4, A13, A14, A18, AFF_1:25; hence contradiction by A2, A4, A7, A8, A9, A13, A16, AFF_1:18; ::_thesis: verum end; A32: c <> c9 proof assume c = c9 ; ::_thesis: contradiction then A33: c,a // c,a9 by A28, AFF_1:4; LIN o,a,a9 by A2, A8, A9, A10, AFF_1:21; hence contradiction by A23, A31, A33, AFF_1:14; ::_thesis: verum end; a <> c by A20, AFF_1:7; then A34: a9,c9 // p,q by A28, A29, AFF_1:5; A35: ( p <> b & p <> b9 & q <> b & q <> b9 ) proof A36: now__::_thesis:_not_b9_=_q assume A37: b9 = q ; ::_thesis: contradiction ( not LIN b9,c9,a9 & c9,a9 // q,p ) by A21, A34, AFF_1:4, AFF_1:6; hence contradiction by A19, A25, A37, AFF_1:55; ::_thesis: verum end; A38: now__::_thesis:_not_b_=_q assume A39: b = q ; ::_thesis: contradiction ( not LIN b,c,a & c,a // q,p ) by A20, A29, AFF_1:4, AFF_1:6; hence contradiction by A19, A24, A39, AFF_1:55; ::_thesis: verum end; assume ( not p <> b or not p <> b9 or not q <> b or not q <> b9 ) ; ::_thesis: contradiction hence contradiction by A20, A21, A26, A27, A29, A34, A38, A36, AFF_1:55; ::_thesis: verum end; A40: b <> c by A20, AFF_1:7; then A41: ( Line (b,c) is being_line & c in Line (b,c) ) by AFF_1:24; A42: b in Line (b,c) by A40, AFF_1:24; then A43: q in Line (b,c) by A26, A40, A41, AFF_1:25; A44: now__::_thesis:_C_//_P assume not C // P ; ::_thesis: contradiction then consider x being Element of AP such that A45: x in C and A46: x in P by A3, A4, AFF_1:58; A47: x <> c proof A48: ( LIN q,b9,c9 & LIN q,b9,b9 ) by A27, AFF_1:6, AFF_1:7; assume A49: x = c ; ::_thesis: contradiction then ( LIN b,c,b9 & LIN b,c,c ) by A3, A11, A12, A46, AFF_1:21; then LIN q,b9,c by A26, A40, AFF_1:8; then A50: b9 in C by A4, A14, A15, A32, A35, A48, AFF_1:8, AFF_1:25; then LIN c,c9,q by A3, A4, A6, A12, A14, A27, A46, A49, AFF_1:18; then A51: q in C by A4, A14, A15, A32, AFF_1:25; c = b9 by A3, A4, A6, A12, A14, A46, A49, A50, AFF_1:18; then C = Line (b,c) by A4, A14, A35, A41, A43, A51, AFF_1:18; hence contradiction by A3, A4, A6, A11, A12, A22, A42, A50, AFF_1:18; ::_thesis: verum end; A52: x <> b proof A53: LIN q,c9,b9 by A27, AFF_1:6; assume A54: x = b ; ::_thesis: contradiction then q in C by A4, A14, A26, A40, A45, AFF_1:25; then ( q = c9 or b9 in C ) by A4, A15, A53, AFF_1:25; then c9,a9 // c9,p by A3, A4, A6, A11, A12, A22, A34, A45, A54, AFF_1:4, AFF_1:18; then LIN c9,a9,p by AFF_1:def_1; then A55: LIN p,a9,c9 by AFF_1:6; ( LIN p,a9,b9 & LIN p,a9,a9 ) by A25, AFF_1:6, AFF_1:7; then p = a9 by A21, A55, AFF_1:8; then LIN a,a9,b by A24, AFF_1:6; then b in A by A2, A9, A10, A23, AFF_1:25; hence contradiction by A2, A4, A7, A8, A13, A17, A45, A54, AFF_1:18; ::_thesis: verum end; A56: ( c,a // q,p & c,a // c9,a9 ) by A28, A29, AFF_1:4; ( not LIN b,c,a & not LIN b9,c9,a9 ) by A20, A21, AFF_1:6; then x in A by A1, A2, A3, A4, A6, A9, A10, A11, A12, A14, A15, A19, A23, A24, A25, A26, A27, A45, A46, A47, A52, A56, Def3; hence contradiction by A2, A4, A7, A8, A13, A30, A45, A46, AFF_1:18; ::_thesis: verum end; A57: a <> b by A20, AFF_1:7; A58: a9 <> b9 by A21, AFF_1:7; then A59: a9 in Line (b9,a9) by AFF_1:24; A60: ( Line (b9,a9) is being_line & b9 in Line (b9,a9) ) by A58, AFF_1:24; then A61: p in Line (b9,a9) by A25, A58, A59, AFF_1:25; A62: now__::_thesis:_P_//_A assume not P // A ; ::_thesis: contradiction then consider x being Element of AP such that A63: x in P and A64: x in A by A2, A3, AFF_1:58; A65: x <> b proof assume A66: x = b ; ::_thesis: contradiction then p in A by A2, A9, A24, A57, A64, AFF_1:25; then ( a9,c9 // a9,q or b9 in A ) by A2, A10, A34, A60, A59, A61, AFF_1:18; then LIN a9,c9,q by A2, A3, A5, A11, A12, A22, A64, A66, AFF_1:18, AFF_1:def_1; then A67: LIN q,c9,a9 by AFF_1:6; ( LIN q,c9,b9 & LIN q,c9,c9 ) by A27, AFF_1:6, AFF_1:7; then q = c9 by A21, A67, AFF_1:8; then LIN c,c9,b by A26, AFF_1:6; then b in C by A4, A14, A15, A32, AFF_1:25; hence contradiction by A2, A4, A7, A8, A13, A17, A64, A66, AFF_1:18; ::_thesis: verum end; x <> a proof assume x = a ; ::_thesis: contradiction then ( p in P & Line (b9,a9) <> P ) by A2, A3, A5, A9, A10, A11, A23, A24, A57, A59, A63, AFF_1:18, AFF_1:25; hence contradiction by A3, A12, A35, A60, A61, AFF_1:18; ::_thesis: verum end; then x in C by A1, A2, A3, A4, A5, A9, A10, A11, A12, A14, A15, A19, A20, A21, A24, A25, A26, A27, A28, A29, A32, A63, A64, A65, Def3; hence contradiction by A2, A4, A7, A8, A13, A30, A63, A64, AFF_1:18; ::_thesis: verum end; ( not P // A or not C // P ) proof assume ( P // A & C // P ) ; ::_thesis: contradiction then C // A by AFF_1:44; hence contradiction by A7, A8, A13, AFF_1:45; ::_thesis: verum end; hence contradiction by A62, A44; ::_thesis: verum end; theorem :: AFF_3:6 for AP being AffinPlane st AP is satisfying_DES1_2 holds AP is Desarguesian proof let AP be AffinPlane; ::_thesis: ( AP is satisfying_DES1_2 implies AP is Desarguesian ) assume A1: AP is satisfying_DES1_2 ; ::_thesis: AP is Desarguesian let A be Subset of AP; :: according to AFF_2:def_4 ::_thesis: for b1, b2 being M2(K24( the U1 of AP)) for b3, b4, b5, b6, b7, b8, b9 being M2( the U1 of AP) holds ( not b3 in A or not b3 in b1 or not b3 in b2 or b3 = b4 or b3 = b5 or b3 = b6 or not b4 in A or not b7 in A or not b5 in b1 or not b8 in b1 or not b6 in b2 or not b9 in b2 or not A is being_line or not b1 is being_line or not b2 is being_line or A = b1 or A = b2 or not b4,b5 // b7,b8 or not b4,b6 // b7,b9 or b5,b6 // b8,b9 ) let P, C be Subset of AP; ::_thesis: for b1, b2, b3, b4, b5, b6, b7 being M2( the U1 of AP) holds ( not b1 in A or not b1 in P or not b1 in C or b1 = b2 or b1 = b3 or b1 = b4 or not b2 in A or not b5 in A or not b3 in P or not b6 in P or not b4 in C or not b7 in C or not A is being_line or not P is being_line or not C is being_line or A = P or A = C or not b2,b3 // b5,b6 or not b2,b4 // b5,b7 or b3,b4 // b6,b7 ) let o, a, b, c, a9, b9, c9 be Element of AP; ::_thesis: ( not o in A or not o in P or not o in C or o = a or o = b or o = c or not a in A or not a9 in A or not b in P or not b9 in P or not c in C or not c9 in C or not A is being_line or not P is being_line or not C is being_line or A = P or A = C or not a,b // a9,b9 or not a,c // a9,c9 or b,c // b9,c9 ) assume that A2: o in A and A3: o in P and A4: o in C and A5: o <> a and A6: o <> b and A7: o <> c and A8: a in A and A9: a9 in A and A10: b in P and A11: b9 in P and A12: c in C and A13: c9 in C and A14: A is being_line and A15: P is being_line and A16: C is being_line and A17: A <> P and A18: A <> C and A19: a,b // a9,b9 and A20: a,c // a9,c9 ; ::_thesis: b,c // b9,c9 now__::_thesis:_(_P_<>_C_implies_b,c_//_b9,c9_) A21: ( not LIN o,b,a & not LIN o,a,c ) proof A22: now__::_thesis:_not_LIN_o,a,c assume LIN o,a,c ; ::_thesis: contradiction then c in A by A2, A5, A8, A14, AFF_1:25; hence contradiction by A2, A4, A7, A12, A14, A16, A18, AFF_1:18; ::_thesis: verum end; A23: now__::_thesis:_not_LIN_o,b,a assume LIN o,b,a ; ::_thesis: contradiction then a in P by A3, A6, A10, A15, AFF_1:25; hence contradiction by A2, A3, A5, A8, A14, A15, A17, AFF_1:18; ::_thesis: verum end; assume ( LIN o,b,a or LIN o,a,c ) ; ::_thesis: contradiction hence contradiction by A23, A22; ::_thesis: verum end; A24: ( b = b9 implies b,c // b9,c9 ) proof A25: LIN o,c,c9 by A4, A12, A13, A16, AFF_1:21; A26: LIN o,a,a9 by A2, A8, A9, A14, AFF_1:21; assume A27: b = b9 ; ::_thesis: b,c // b9,c9 then b,a // b,a9 by A19, AFF_1:4; then a,c // a,c9 by A20, A21, A26, AFF_1:14; then c = c9 by A21, A25, AFF_1:14; hence b,c // b9,c9 by A27, AFF_1:2; ::_thesis: verum end; A28: ( a9 = o implies b,c // b9,c9 ) proof assume A29: a9 = o ; ::_thesis: b,c // b9,c9 ( LIN o,b,b9 & not LIN o,a,b ) by A3, A10, A11, A15, A21, AFF_1:6, AFF_1:21; then A30: o = b9 by A19, A29, AFF_1:55; LIN o,c,c9 by A4, A12, A13, A16, AFF_1:21; then o = c9 by A20, A21, A29, AFF_1:55; hence b,c // b9,c9 by A30, AFF_1:3; ::_thesis: verum end; A31: ( c9 = o implies b,c // b9,c9 ) proof A32: c,a // c9,a9 by A20, AFF_1:4; assume A33: c9 = o ; ::_thesis: b,c // b9,c9 ( LIN o,a,a9 & not LIN o,c,a ) by A2, A8, A9, A14, A21, AFF_1:6, AFF_1:21; hence b,c // b9,c9 by A28, A33, A32, AFF_1:55; ::_thesis: verum end; set K = Line (a,c); A34: a in Line (a,c) by AFF_1:15; A35: a <> c by A2, A4, A5, A8, A12, A14, A16, A18, AFF_1:18; then A36: Line (a,c) is being_line by AFF_1:def_3; A37: c in Line (a,c) by AFF_1:15; A38: a <> b by A2, A3, A5, A8, A10, A14, A15, A17, AFF_1:18; A39: ( LIN a,b,c implies b,c // b9,c9 ) proof consider N being Subset of AP such that A40: a9 in N and A41: Line (a,c) // N by A36, AFF_1:49; A42: N is being_line by A41, AFF_1:36; a9,c9 // Line (a,c) by A20, A35, AFF_1:29, AFF_1:32; then a9,c9 // N by A41, AFF_1:43; then A43: c9 in N by A40, A42, AFF_1:23; assume LIN a,b,c ; ::_thesis: b,c // b9,c9 then LIN a,c,b by AFF_1:6; then A44: b in Line (a,c) by AFF_1:def_2; then Line (a,c) = Line (a,b) by A38, A36, A34, AFF_1:57; then a9,b9 // Line (a,c) by A19, A38, AFF_1:29, AFF_1:32; then a9,b9 // N by A41, AFF_1:43; then b9 in N by A40, A42, AFF_1:23; hence b,c // b9,c9 by A37, A44, A41, A43, AFF_1:39; ::_thesis: verum end; assume A45: P <> C ; ::_thesis: b,c // b9,c9 A46: now__::_thesis:_(_o_<>_a9_&_o_<>_b9_&_o_<>_c9_&_b_<>_b9_&_not_LIN_a,b,c_implies_b,c_//_b9,c9_) set T = Line (b9,a9); set D = Line (b,a); set N = Line (a9,c9); assume that A47: o <> a9 and A48: o <> b9 and A49: o <> c9 and A50: b <> b9 and A51: not LIN a,b,c ; ::_thesis: b,c // b9,c9 A52: c9 in Line (a9,c9) by AFF_1:15; assume not b,c // b9,c9 ; ::_thesis: contradiction then consider q being Element of AP such that A53: LIN b,c,q and A54: LIN b9,c9,q by AFF_1:60; consider M being Subset of AP such that A55: q in M and A56: Line (a,c) // M by A36, AFF_1:49; A57: M is being_line by A56, AFF_1:36; not a,b // M proof assume a,b // M ; ::_thesis: contradiction then a,b // Line (a,c) by A56, AFF_1:43; then b in Line (a,c) by A36, A34, AFF_1:23; hence contradiction by A36, A34, A37, A51, AFF_1:21; ::_thesis: verum end; then consider p being Element of AP such that A58: p in M and A59: LIN a,b,p by A57, AFF_1:59; A60: a9 in Line (a9,c9) by AFF_1:15; A61: p <> q proof A62: ( LIN p,b,a & LIN p,b,b ) by A59, AFF_1:6, AFF_1:7; assume A63: p = q ; ::_thesis: contradiction then LIN p,b,c by A53, AFF_1:6; then p = b by A51, A62, AFF_1:8; then LIN b,b9,c9 by A54, A63, AFF_1:6; then c9 in P by A10, A11, A15, A50, AFF_1:25; hence contradiction by A3, A4, A13, A15, A16, A45, A49, AFF_1:18; ::_thesis: verum end; A64: c,a // q,p by A34, A37, A55, A56, A58, AFF_1:39; A65: LIN b,a,p by A59, AFF_1:6; A66: b9 <> c9 by A3, A4, A11, A13, A15, A16, A45, A48, AFF_1:18; A67: a9 <> c9 by A2, A4, A9, A13, A14, A16, A18, A47, AFF_1:18; then A68: Line (a9,c9) is being_line by AFF_1:def_3; A69: Line (a,c) // Line (a9,c9) by A20, A35, A67, AFF_1:37; then A70: Line (a9,c9) // M by A56, AFF_1:44; A71: a9 <> b9 by A2, A3, A9, A11, A14, A15, A17, A47, AFF_1:18; A72: not LIN a9,b9,c9 proof assume LIN a9,b9,c9 ; ::_thesis: contradiction then LIN a9,c9,b9 by AFF_1:6; then b9 in Line (a9,c9) by AFF_1:def_2; then a9,b9 // Line (a9,c9) by A68, A60, AFF_1:23; then A73: a9,b9 // Line (a,c) by A69, AFF_1:43; a9,b9 // a,b by A19, AFF_1:4; then a,b // Line (a,c) by A71, A73, AFF_1:32; then b in Line (a,c) by A36, A34, AFF_1:23; hence contradiction by A36, A34, A37, A51, AFF_1:21; ::_thesis: verum end; not b9,p // Line (a9,c9) proof assume b9,p // Line (a9,c9) ; ::_thesis: contradiction then b9,p // M by A70, AFF_1:43; then p,b9 // M by AFF_1:34; then A74: b9 in M by A57, A58, AFF_1:23; A75: now__::_thesis:_not_b9_<>_q assume A76: b9 <> q ; ::_thesis: contradiction LIN b9,q,c9 by A54, AFF_1:6; then c9 in M by A55, A57, A74, A76, AFF_1:25; then ( a9 in Line (a9,c9) & b9 in Line (a9,c9) ) by A52, A70, A74, AFF_1:15, AFF_1:45; hence contradiction by A68, A52, A72, AFF_1:21; ::_thesis: verum end; now__::_thesis:_not_b9_=_q assume b9 = q ; ::_thesis: contradiction then LIN b,b9,c by A53, AFF_1:6; then c in P by A10, A11, A15, A50, AFF_1:25; hence contradiction by A3, A4, A7, A12, A15, A16, A45, AFF_1:18; ::_thesis: verum end; hence contradiction by A75; ::_thesis: verum end; then consider x being Element of AP such that A77: x in Line (a9,c9) and A78: LIN b9,p,x by A68, AFF_1:59; set A9 = Line (x,a); A79: a <> a9 proof assume A80: a = a9 ; ::_thesis: contradiction ( not LIN o,a,b & LIN o,b,b9 ) by A3, A10, A11, A15, A21, AFF_1:6, AFF_1:21; hence contradiction by A19, A50, A80, AFF_1:14; ::_thesis: verum end; A81: x <> a proof assume x = a ; ::_thesis: contradiction then a9 in Line (a,c) by A34, A60, A69, A77, AFF_1:45; then A = Line (a,c) by A8, A9, A14, A36, A34, A79, AFF_1:18; hence contradiction by A2, A4, A7, A12, A14, A16, A18, A37, AFF_1:18; ::_thesis: verum end; then A82: Line (x,a) is being_line by AFF_1:def_3; A83: c <> c9 proof assume c = c9 ; ::_thesis: contradiction then A84: c,a // c,a9 by A20, AFF_1:4; ( not LIN o,c,a & LIN o,a,a9 ) by A2, A8, A9, A14, A21, AFF_1:6, AFF_1:21; hence contradiction by A79, A84, AFF_1:14; ::_thesis: verum end; A85: not LIN b9,c9,x proof A86: now__::_thesis:_(_c9_=_x_implies_LIN_b9,c9,a9_) A87: now__::_thesis:_not_q_=_c9 assume q = c9 ; ::_thesis: contradiction then LIN c,c9,b by A53, AFF_1:6; then b in C by A12, A13, A16, A83, AFF_1:25; hence contradiction by A3, A4, A6, A10, A15, A16, A45, AFF_1:18; ::_thesis: verum end; assume c9 = x ; ::_thesis: LIN b9,c9,a9 then A88: LIN b9,c9,p by A78, AFF_1:6; LIN b9,c9,c9 by AFF_1:7; then c9 in M by A66, A54, A55, A57, A58, A61, A88, AFF_1:8, AFF_1:25; then A89: q in Line (a9,c9) by A55, A52, A70, AFF_1:45; LIN q,c9,b9 by A54, AFF_1:6; then ( q = c9 or b9 in Line (a9,c9) ) by A68, A52, A89, AFF_1:25; hence LIN b9,c9,a9 by A68, A60, A52, A87, AFF_1:21; ::_thesis: verum end; assume LIN b9,c9,x ; ::_thesis: contradiction then A90: LIN c9,x,b9 by AFF_1:6; A91: ( LIN c9,x,a9 & LIN c9,x,c9 ) by A68, A60, A52, A77, AFF_1:21; then LIN c9,a9,b9 by A90, A86, AFF_1:6, AFF_1:8; then c9,a9 // c9,b9 by AFF_1:def_1; then a9,c9 // b9,c9 by AFF_1:4; then A92: a,c // b9,c9 by A20, A67, AFF_1:5; ( c9 = x or LIN b9,c9,a9 ) by A90, A91, AFF_1:8; then b9,c9 // b9,a9 by A86, AFF_1:def_1; then b9,c9 // a9,b9 by AFF_1:4; then b9,c9 // a,b by A19, A71, AFF_1:5; then a,c // a,b by A66, A92, AFF_1:5; then LIN a,c,b by AFF_1:def_1; hence contradiction by A51, AFF_1:6; ::_thesis: verum end; A93: ( x in Line (x,a) & a in Line (x,a) ) by AFF_1:15; A <> Line (a,c) by A2, A4, A7, A12, A14, A16, A18, A37, AFF_1:18; then A94: A <> Line (a9,c9) by A8, A34, A69, AFF_1:45; A95: not LIN b,c,a by A51, AFF_1:6; A96: p in Line (b,a) by A59, AFF_1:def_2; A97: ( Line (b,a) is being_line & b in Line (b,a) ) by A38, AFF_1:15, AFF_1:def_3; A98: LIN b9,x,p by A78, AFF_1:6; c,a // c9,x by A34, A37, A52, A69, A77, AFF_1:39; then o in Line (x,a) by A1, A3, A4, A6, A7, A10, A11, A12, A13, A15, A16, A45, A53, A54, A98, A81, A82, A93, A61, A85, A64, A95, A65, Def3; then x in A by A2, A5, A8, A14, A82, A93, AFF_1:18; then x = a9 by A9, A14, A68, A60, A77, A94, AFF_1:18; then A99: ( a9 in Line (b9,a9) & p in Line (b9,a9) ) by A98, AFF_1:15, AFF_1:def_2; Line (b,a) // Line (b9,a9) by A19, A38, A71, AFF_1:37; then ( a in Line (b,a) & a9 in Line (b,a) ) by A96, A99, AFF_1:15, AFF_1:45; then b in A by A8, A9, A14, A79, A97, AFF_1:18; hence contradiction by A2, A3, A6, A10, A14, A15, A17, AFF_1:18; ::_thesis: verum end; ( b9 = o implies b,c // b9,c9 ) proof assume A100: b9 = o ; ::_thesis: b,c // b9,c9 ( LIN o,a,a9 & b,a // b9,a9 ) by A2, A8, A9, A14, A19, AFF_1:4, AFF_1:21; hence b,c // b9,c9 by A21, A28, A100, AFF_1:55; ::_thesis: verum end; hence b,c // b9,c9 by A28, A31, A39, A24, A46; ::_thesis: verum end; hence b,c // b9,c9 by A10, A11, A12, A13, A15, AFF_1:51; ::_thesis: verum end; theorem :: AFF_3:7 for AP being AffinPlane st AP is satisfying_DES2_1 holds AP is satisfying_DES2 proof let AP be AffinPlane; ::_thesis: ( AP is satisfying_DES2_1 implies AP is satisfying_DES2 ) assume A1: AP is satisfying_DES2_1 ; ::_thesis: AP is satisfying_DES2 let A be Subset of AP; :: according to AFF_3:def_5 ::_thesis: for P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds a,c // p,q let P, C be Subset of AP; ::_thesis: for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds a,c // p,q let a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 implies a,c // p,q ) assume that A2: A is being_line and A3: P is being_line and A4: C is being_line and A5: A <> P and A6: A <> C and A7: P <> C and A8: a in A and A9: a9 in A and A10: b in P and A11: b9 in P and A12: c in C and A13: c9 in C and A14: A // P and A15: A // C and A16: not LIN b,a,c and A17: not LIN b9,a9,c9 and A18: p <> q and A19: a <> a9 and A20: LIN b,a,p and A21: LIN b9,a9,p and A22: ( LIN b,c,q & LIN b9,c9,q ) and A23: a,c // a9,c9 ; ::_thesis: a,c // p,q A24: P // C by A14, A15, AFF_1:44; set P9 = Line (b9,a9); A25: p in Line (b9,a9) by A21, AFF_1:def_2; a9 <> b9 by A17, AFF_1:7; then A26: Line (b9,a9) is being_line by AFF_1:def_3; set K = Line (a,c); set N = Line (a9,c9); set D = Line (b,c); set T = Line (b9,c9); A27: ( q in Line (b,c) & q in Line (b9,c9) ) by A22, AFF_1:def_2; A28: c9 in Line (a9,c9) by AFF_1:15; b <> c by A16, AFF_1:7; then A29: Line (b,c) is being_line by AFF_1:def_3; b9 <> c9 by A17, AFF_1:7; then A30: Line (b9,c9) is being_line by AFF_1:def_3; A31: a <> c by A16, AFF_1:7; then A32: Line (a,c) is being_line by AFF_1:def_3; A33: a9 <> c9 by A17, AFF_1:7; then A34: Line (a9,c9) is being_line by AFF_1:def_3; then consider M being Subset of AP such that A35: p in M and A36: Line (a9,c9) // M by AFF_1:49; A37: Line (a,c) // Line (a9,c9) by A23, A31, A33, AFF_1:37; then A38: Line (a,c) // M by A36, AFF_1:44; A39: c in Line (b,c) by AFF_1:15; A40: b in Line (b,c) by AFF_1:15; set A9 = Line (b,a); A41: p in Line (b,a) by A20, AFF_1:def_2; a <> b by A16, AFF_1:7; then A42: Line (b,a) is being_line by AFF_1:def_3; A43: c9 in Line (b9,c9) by AFF_1:15; A44: b9 in Line (b9,c9) by AFF_1:15; A45: a9 in Line (a9,c9) by AFF_1:15; A46: a in Line (a,c) by AFF_1:15; A47: a9 in Line (b9,a9) by AFF_1:15; A48: b9 in Line (b9,a9) by AFF_1:15; A49: a in Line (b,a) by AFF_1:15; A50: b in Line (b,a) by AFF_1:15; A51: c in Line (a,c) by AFF_1:15; then A52: Line (a,c) <> A by A6, A12, A15, AFF_1:45; A53: c <> c9 proof assume c = c9 ; ::_thesis: contradiction then Line (a,c) = Line (a9,c9) by A51, A28, A37, AFF_1:45; hence contradiction by A2, A8, A9, A19, A32, A46, A45, A52, AFF_1:18; ::_thesis: verum end; A54: Line (b,c) <> Line (b9,c9) proof assume Line (b,c) = Line (b9,c9) ; ::_thesis: contradiction then Line (b,c) = C by A4, A12, A13, A29, A39, A43, A53, AFF_1:18; hence contradiction by A7, A10, A24, A40, AFF_1:45; ::_thesis: verum end; A55: b <> b9 proof A56: Line (b,a) <> Line (b9,a9) proof assume Line (b,a) = Line (b9,a9) ; ::_thesis: contradiction then Line (b,a) = A by A2, A8, A9, A19, A42, A49, A47, AFF_1:18; hence contradiction by A5, A10, A14, A50, AFF_1:45; ::_thesis: verum end; assume A57: b = b9 ; ::_thesis: contradiction then b9 = q by A29, A30, A40, A44, A27, A54, AFF_1:18; hence contradiction by A18, A42, A26, A50, A41, A48, A25, A57, A56, AFF_1:18; ::_thesis: verum end; A58: M is being_line by A36, AFF_1:36; A59: now__::_thesis:_(_not_Line_(b9,c9)_//_M_implies_a,c_//_p,q_) assume not Line (b9,c9) // M ; ::_thesis: a,c // p,q then consider x being Element of AP such that A60: x in Line (b9,c9) and A61: x in M by A30, A58, AFF_1:58; A62: p <> x proof assume p = x ; ::_thesis: contradiction then ( p = b9 or Line (b9,c9) = Line (b9,a9) ) by A30, A44, A26, A48, A25, A60, AFF_1:18; then ( LIN b,b9,a or c9 in Line (b9,a9) ) by A42, A50, A49, A41, AFF_1:15, AFF_1:21; then a in P by A3, A10, A11, A17, A55, AFF_1:25, AFF_1:def_2; hence contradiction by A5, A8, A14, AFF_1:45; ::_thesis: verum end; not b,x // C proof assume A63: b,x // C ; ::_thesis: contradiction C // P by A14, A15, AFF_1:44; then b,x // P by A63, AFF_1:43; then x in P by A3, A10, AFF_1:23; then ( b9 in M or c9 in P ) by A3, A11, A30, A44, A43, A60, A61, AFF_1:18; then ( b9 = p or M = Line (b9,a9) ) by A7, A13, A24, A26, A48, A25, A35, A58, AFF_1:18, AFF_1:45; then ( LIN b,b9,a or Line (a9,c9) // Line (b9,a9) ) by A20, A36, AFF_1:6; then ( a in P or Line (a9,c9) = Line (b9,a9) ) by A3, A10, A11, A45, A47, A55, AFF_1:25, AFF_1:45; hence contradiction by A5, A8, A14, A17, A28, AFF_1:45, AFF_1:def_2; ::_thesis: verum end; then consider y being Element of AP such that A64: y in C and A65: LIN b,x,y by A4, AFF_1:59; A66: LIN b,y,x by A65, AFF_1:6; A67: not LIN b,a,y proof A68: now__::_thesis:_not_x_=_p assume x = p ; ::_thesis: contradiction then ( p = b9 or Line (b9,c9) = Line (b9,a9) ) by A30, A44, A26, A48, A25, A60, AFF_1:18; then ( LIN b,b9,a or c9 in Line (b9,a9) ) by A42, A50, A49, A41, AFF_1:15, AFF_1:21; then a in P by A3, A10, A11, A17, A55, AFF_1:25, AFF_1:def_2; hence contradiction by A5, A8, A14, AFF_1:45; ::_thesis: verum end; assume LIN b,a,y ; ::_thesis: contradiction then A69: LIN b,y,a by AFF_1:6; LIN b,y,b by AFF_1:7; then ( b = y or LIN a,b,x ) by A66, A69, AFF_1:8; then x in Line (b,a) by A7, A10, A24, A64, AFF_1:45, AFF_1:def_2; then ( x = p or Line (b,a) = M ) by A42, A41, A35, A58, A61, AFF_1:18; then Line (a,c) = Line (b,a) by A46, A49, A38, A68, AFF_1:45; hence contradiction by A16, A51, AFF_1:def_2; ::_thesis: verum end; ( LIN b9,c9,x & a9,c9 // p,x ) by A30, A45, A28, A44, A43, A35, A36, A60, A61, AFF_1:21, AFF_1:39; then a9,c9 // a,y by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A13, A14, A15, A17, A20, A21, A64, A66, A67, A62, Def6; then a,c // a,y by A23, A33, AFF_1:5; then LIN a,c,y by AFF_1:def_1; then y in Line (a,c) by AFF_1:def_2; then ( Line (a,c) = C or y = c ) by A4, A12, A32, A51, A64, AFF_1:18; then ( a in C or LIN b,c,x ) by A65, AFF_1:6, AFF_1:15; then x in Line (b,c) by A6, A8, A15, AFF_1:45, AFF_1:def_2; then ( q in M or c9 in Line (b,c) ) by A29, A30, A43, A27, A60, A61, AFF_1:18; then ( a,c // p,q or LIN c,c9,b ) by A29, A46, A51, A40, A39, A35, A38, AFF_1:21, AFF_1:39; then ( a,c // p,q or b in C ) by A4, A12, A13, A53, AFF_1:25; hence a,c // p,q by A7, A10, A24, AFF_1:45; ::_thesis: verum end; A70: now__::_thesis:_(_not_M_//_Line_(b,c)_implies_a,c_//_p,q_) assume not M // Line (b,c) ; ::_thesis: a,c // p,q then consider x being Element of AP such that A71: x in M and A72: x in Line (b,c) by A29, A58, AFF_1:58; A73: p <> x proof assume p = x ; ::_thesis: contradiction then ( p = b or Line (b,c) = Line (b,a) ) by A29, A40, A42, A50, A41, A72, AFF_1:18; then ( LIN b,b9,a9 or c in Line (b,a) ) by A26, A48, A47, A25, AFF_1:15, AFF_1:21; then a9 in P by A3, A10, A11, A16, A55, AFF_1:25, AFF_1:def_2; hence contradiction by A5, A9, A14, AFF_1:45; ::_thesis: verum end; not b9,x // C proof A74: now__::_thesis:_not_b_=_p assume b = p ; ::_thesis: contradiction then LIN b,b9,a9 by A26, A48, A47, A25, AFF_1:21; then a9 in P by A3, A10, A11, A55, AFF_1:25; hence contradiction by A5, A9, A14, AFF_1:45; ::_thesis: verum end; assume A75: b9,x // C ; ::_thesis: contradiction C // P by A14, A15, AFF_1:44; then b9,x // P by A75, AFF_1:43; then x in P by A3, A11, AFF_1:23; then ( x = b or Line (b,c) = P ) by A3, A10, A29, A40, A72, AFF_1:18; then ( b = p or M = Line (b,a) ) by A7, A12, A24, A39, A42, A50, A41, A35, A58, A71, AFF_1:18, AFF_1:45; then b in Line (a,c) by A46, A50, A49, A38, A74, AFF_1:45; hence contradiction by A16, A32, A46, A51, AFF_1:21; ::_thesis: verum end; then consider y being Element of AP such that A76: y in C and A77: LIN b9,x,y by A4, AFF_1:59; A78: LIN b9,y,x by A77, AFF_1:6; A79: not LIN b9,a9,y proof A80: now__::_thesis:_not_x_=_p assume x = p ; ::_thesis: contradiction then ( p = b or Line (b,c) = Line (b,a) ) by A29, A40, A42, A50, A41, A72, AFF_1:18; then ( LIN b,b9,a9 or c in Line (b,a) ) by A26, A48, A47, A25, AFF_1:15, AFF_1:21; then a9 in P by A3, A10, A11, A16, A55, AFF_1:25, AFF_1:def_2; hence contradiction by A5, A9, A14, AFF_1:45; ::_thesis: verum end; assume LIN b9,a9,y ; ::_thesis: contradiction then A81: LIN b9,y,a9 by AFF_1:6; LIN b9,y,b9 by AFF_1:7; then ( b9 = y or LIN a9,b9,x ) by A78, A81, AFF_1:8; then x in Line (b9,a9) by A7, A11, A24, A76, AFF_1:45, AFF_1:def_2; then ( x = p or Line (b9,a9) = M ) by A26, A25, A35, A58, A71, AFF_1:18; then Line (a9,c9) = Line (b9,a9) by A45, A47, A36, A80, AFF_1:45; hence contradiction by A17, A28, AFF_1:def_2; ::_thesis: verum end; ( LIN b,c,x & a,c // p,x ) by A29, A46, A51, A40, A39, A35, A38, A71, A72, AFF_1:21, AFF_1:39; then a,c // a9,y by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A14, A15, A16, A20, A21, A76, A78, A79, A73, Def6; then a9,y // a9,c9 by A23, A31, AFF_1:5; then LIN a9,y,c9 by AFF_1:def_1; then LIN a9,c9,y by AFF_1:6; then y in Line (a9,c9) by AFF_1:def_2; then ( Line (a9,c9) = C or y = c9 ) by A4, A13, A34, A28, A76, AFF_1:18; then ( a9 in C or LIN b9,c9,x ) by A77, AFF_1:6, AFF_1:15; then x in Line (b9,c9) by A6, A9, A15, AFF_1:45, AFF_1:def_2; then ( q in M or c9 in Line (b,c) ) by A29, A30, A43, A27, A71, A72, AFF_1:18; then ( a,c // p,q or LIN c,c9,b ) by A29, A46, A51, A40, A39, A35, A38, AFF_1:21, AFF_1:39; then ( a,c // p,q or b in C ) by A4, A12, A13, A53, AFF_1:25; hence a,c // p,q by A7, A10, A24, AFF_1:45; ::_thesis: verum end; ( not M // Line (b,c) or not Line (b9,c9) // M ) proof assume ( M // Line (b,c) & Line (b9,c9) // M ) ; ::_thesis: contradiction then Line (b9,c9) // Line (b,c) by AFF_1:44; hence contradiction by A27, A54, AFF_1:45; ::_thesis: verum end; hence a,c // p,q by A70, A59; ::_thesis: verum end; theorem :: AFF_3:8 for AP being AffinPlane holds ( AP is satisfying_DES2_1 iff AP is satisfying_DES2_3 ) proof let AP be AffinPlane; ::_thesis: ( AP is satisfying_DES2_1 iff AP is satisfying_DES2_3 ) A1: ( AP is satisfying_DES2_1 implies AP is satisfying_DES2_3 ) proof assume A2: AP is satisfying_DES2_1 ; ::_thesis: AP is satisfying_DES2_3 thus AP is satisfying_DES2_3 ::_thesis: verum proof let A be Subset of AP; :: according to AFF_3:def_8 ::_thesis: for P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds A // C let P, C be Subset of AP; ::_thesis: for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds A // C let a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & c <> c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q implies A // C ) assume that A3: A is being_line and A4: P is being_line and A5: C is being_line and A6: A <> P and A7: A <> C and A8: P <> C and A9: a in A and A10: a9 in A and A11: b in P and A12: b9 in P and A13: c in C and A14: c9 in C and A15: A // P and A16: not LIN b,a,c and A17: not LIN b9,a9,c9 and A18: p <> q and A19: c <> c9 and A20: LIN b,a,p and A21: LIN b9,a9,p and A22: LIN b,c,q and A23: LIN b9,c9,q and A24: a,c // a9,c9 and A25: a,c // p,q ; ::_thesis: A // C now__::_thesis:_A_//_C set A9 = Line (a,c); set P9 = Line (p,q); set C9 = Line (a9,c9); A26: LIN p,a9,b9 by A21, AFF_1:6; A27: a <> c by A16, AFF_1:7; then A28: ( Line (a,c) is being_line & a in Line (a,c) ) by AFF_1:24; A29: q <> c proof assume A30: q = c ; ::_thesis: contradiction then c,p // c,a by A25, AFF_1:4; then LIN c,p,a by AFF_1:def_1; then A31: LIN p,a,c by AFF_1:6; ( LIN p,a,b & LIN p,a,a ) by A20, AFF_1:6, AFF_1:7; then a = p by A16, A31, AFF_1:8; then LIN a,a9,b9 by A21, AFF_1:6; then ( b9 in A or a = a9 ) by A3, A9, A10, AFF_1:25; then a9,c9 // a9,c by A6, A12, A15, A24, AFF_1:4, AFF_1:45; then LIN a9,c9,c by AFF_1:def_1; then LIN c,c9,a9 by AFF_1:6; then A32: a9 in C by A5, A13, A14, A19, AFF_1:25; LIN c,c9,b9 by A23, A30, AFF_1:6; then b9 in C by A5, A13, A14, A19, AFF_1:25; hence contradiction by A5, A14, A17, A32, AFF_1:21; ::_thesis: verum end; A33: a <> p proof assume a = p ; ::_thesis: contradiction then LIN a,c,q by A25, AFF_1:def_1; then A34: LIN c,q,a by AFF_1:6; ( LIN c,q,b & LIN c,q,c ) by A22, AFF_1:6, AFF_1:7; hence contradiction by A16, A29, A34, AFF_1:8; ::_thesis: verum end; A35: a <> a9 proof A36: ( LIN p,a,b & LIN p,a,a ) by A20, AFF_1:6, AFF_1:7; assume A37: a = a9 ; ::_thesis: contradiction then LIN a,c,c9 by A24, AFF_1:def_1; then LIN c,c9,a by AFF_1:6; then A38: a in C by A5, A13, A14, A19, AFF_1:25; LIN p,a,b9 by A21, A37, AFF_1:6; then ( b = b9 or a in P ) by A4, A11, A12, A33, A36, AFF_1:8, AFF_1:25; then A39: LIN q,b,c9 by A6, A9, A15, A23, AFF_1:6, AFF_1:45; ( LIN q,b,c & LIN q,b,b ) by A22, AFF_1:6, AFF_1:7; then A40: ( q = b or LIN c,c9,b ) by A39, AFF_1:8; not b in C by A5, A13, A16, A38, AFF_1:21; then LIN p,q,a by A5, A13, A14, A19, A20, A40, AFF_1:6, AFF_1:25; then p,q // p,a by AFF_1:def_1; then a,c // p,a by A18, A25, AFF_1:5; then a,c // a,p by AFF_1:4; then LIN a,c,p by AFF_1:def_1; then A41: p in C by A5, A13, A27, A38, AFF_1:25; LIN p,a,b by A20, AFF_1:6; then b in C by A5, A33, A38, A41, AFF_1:25; hence contradiction by A5, A13, A16, A38, AFF_1:21; ::_thesis: verum end; A42: b <> b9 proof A43: p,q // c,a by A25, AFF_1:4; A44: ( LIN q,b,c & LIN q,b,b ) by A22, AFF_1:6, AFF_1:7; A45: ( LIN p,b,a & LIN p,b,b ) by A20, AFF_1:6, AFF_1:7; assume A46: b = b9 ; ::_thesis: contradiction then LIN p,b,a9 by A21, AFF_1:6; then A47: ( p = b or b in A ) by A3, A9, A10, A35, A45, AFF_1:8, AFF_1:25; LIN q,b,c9 by A23, A46, AFF_1:6; then ( b = q or LIN c,c9,b ) by A44, AFF_1:8; then A48: b in C by A5, A6, A11, A13, A14, A15, A18, A19, A47, AFF_1:25, AFF_1:45; then q in C by A5, A6, A11, A13, A15, A16, A20, A22, A47, AFF_1:25, AFF_1:45; then a in C by A5, A6, A11, A13, A15, A18, A47, A48, A43, AFF_1:45, AFF_1:48; hence contradiction by A5, A13, A16, A48, AFF_1:21; ::_thesis: verum end; then A49: a9,a // b9,b by A3, A4, A9, A10, A11, A12, A15, A35, AFF_1:38; A50: a9 <> c9 by A17, AFF_1:7; then A51: Line (a9,c9) is being_line by AFF_1:24; A52: c9 in Line (a9,c9) by A50, AFF_1:24; A53: LIN p,a,b by A20, AFF_1:6; A54: not LIN p,a9,a proof assume LIN p,a9,a ; ::_thesis: contradiction then A55: LIN p,a,a9 by AFF_1:6; LIN p,a,a by AFF_1:7; then b in A by A3, A9, A10, A33, A35, A53, A55, AFF_1:8, AFF_1:25; hence contradiction by A6, A11, A15, AFF_1:45; ::_thesis: verum end; A56: LIN q,c9,b9 by A23, AFF_1:6; A57: a9 in Line (a9,c9) by A50, AFF_1:24; A58: c in Line (a,c) by A27, AFF_1:24; then A59: Line (a9,c9) // Line (a,c) by A24, A27, A50, A51, A28, A57, A52, AFF_1:38; A60: Line (a,c) <> Line (a9,c9) proof assume A61: Line (a,c) = Line (a9,c9) ; ::_thesis: contradiction then LIN a,a9,c9 by A28, A57, A52, AFF_1:21; then A62: c9 in A by A3, A9, A10, A35, AFF_1:25; LIN a,a9,c by A28, A58, A57, A61, AFF_1:21; then c in A by A3, A9, A10, A35, AFF_1:25; hence contradiction by A3, A5, A7, A13, A14, A19, A62, AFF_1:18; ::_thesis: verum end; A63: LIN q,c,b by A22, AFF_1:6; A64: p in Line (p,q) by A18, AFF_1:24; A65: Line (a,c) <> Line (p,q) proof assume Line (a,c) = Line (p,q) ; ::_thesis: contradiction then A66: ( LIN p,a,c & LIN p,a,a ) by A28, A58, A64, AFF_1:21; LIN p,a,b by A20, AFF_1:6; hence contradiction by A16, A33, A66, AFF_1:8; ::_thesis: verum end; A67: Line (p,q) is being_line by A18, AFF_1:24; A68: Line (p,q) <> Line (a9,c9) proof assume Line (p,q) = Line (a9,c9) ; ::_thesis: contradiction then A69: ( LIN p,a9,c9 & LIN p,a9,a9 ) by A67, A64, A57, A52, AFF_1:21; LIN p,a9,b9 by A21, AFF_1:6; then p = a9 by A17, A69, AFF_1:8; then LIN a,a9,b by A20, AFF_1:6; then b in A by A3, A9, A10, A35, AFF_1:25; hence contradiction by A6, A11, A15, AFF_1:45; ::_thesis: verum end; A70: a9,c9 // p,q by A24, A25, A27, AFF_1:5; A71: not LIN q,c9,c proof A72: now__::_thesis:_not_q_=_c9 assume q = c9 ; ::_thesis: contradiction then c9,a9 // c9,p by A70, AFF_1:4; then LIN c9,a9,p by AFF_1:def_1; then p in Line (a9,c9) by A50, A51, A57, A52, AFF_1:25; then ( p = a9 or b9 in Line (a9,c9) ) by A51, A57, A26, AFF_1:25; then LIN a,a9,b by A17, A20, A51, A57, A52, AFF_1:6, AFF_1:21; then b in A by A3, A9, A10, A35, AFF_1:25; hence contradiction by A6, A11, A15, AFF_1:45; ::_thesis: verum end; assume A73: LIN q,c9,c ; ::_thesis: contradiction LIN q,c9,c9 by AFF_1:7; then A74: b9 in C by A5, A13, A14, A19, A56, A73, A72, AFF_1:8, AFF_1:25; A75: LIN q,c,c by AFF_1:7; LIN q,c,c9 by A73, AFF_1:6; then b in C by A5, A13, A14, A19, A29, A63, A75, AFF_1:8, AFF_1:25; hence contradiction by A4, A5, A8, A11, A12, A42, A74, AFF_1:18; ::_thesis: verum end; A76: q in Line (p,q) by A18, AFF_1:24; then Line (a9,c9) // Line (p,q) by A18, A50, A67, A51, A64, A57, A52, A70, AFF_1:38; then a9,a // c9,c by A2, A67, A51, A28, A58, A64, A76, A57, A52, A42, A65, A60, A68, A59, A49, A53, A26, A63, A56, A54, A71, Def6; hence A // C by A3, A5, A9, A10, A13, A14, A19, A35, AFF_1:38; ::_thesis: verum end; hence A // C ; ::_thesis: verum end; end; ( AP is satisfying_DES2_3 implies AP is satisfying_DES2_1 ) proof assume A77: AP is satisfying_DES2_3 ; ::_thesis: AP is satisfying_DES2_1 thus AP is satisfying_DES2_1 ::_thesis: verum proof let A be Subset of AP; :: according to AFF_3:def_6 ::_thesis: for P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds a,c // a9,c9 let P, C be Subset of AP; ::_thesis: for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds a,c // a9,c9 let a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q implies a,c // a9,c9 ) assume that A78: A is being_line and A79: P is being_line and A80: C is being_line and A81: A <> P and A <> C and A82: P <> C and A83: a in A and A84: a9 in A and A85: b in P and A86: b9 in P and A87: c in C and A88: c9 in C and A89: A // P and A90: A // C and A91: not LIN b,a,c and A92: not LIN b9,a9,c9 and A93: p <> q and A94: LIN b,a,p and A95: LIN b9,a9,p and A96: LIN b,c,q and A97: LIN b9,c9,q and A98: a,c // p,q ; ::_thesis: a,c // a9,c9 A99: C // P by A89, A90, AFF_1:44; then A100: c,c9 // b,b9 by A85, A86, A87, A88, AFF_1:39; assume A101: not a,c // a9,c9 ; ::_thesis: contradiction A102: q <> c proof assume A103: q = c ; ::_thesis: contradiction then c,p // c,a by A98, AFF_1:4; then LIN c,p,a by AFF_1:def_1; then A104: LIN p,a,c by AFF_1:6; ( LIN p,a,b & LIN p,a,a ) by A94, AFF_1:6, AFF_1:7; then a = p by A91, A104, AFF_1:8; then LIN a,a9,b9 by A95, AFF_1:6; then A105: ( b9 in A or a = a9 ) by A78, A83, A84, AFF_1:25; LIN c,c9,b9 by A97, A103, AFF_1:6; then ( c = c9 or b9 in C ) by A80, A87, A88, AFF_1:25; hence contradiction by A81, A82, A86, A89, A101, A99, A105, AFF_1:2, AFF_1:45; ::_thesis: verum end; A106: a <> p proof assume a = p ; ::_thesis: contradiction then LIN a,c,q by A98, AFF_1:def_1; then A107: LIN c,q,a by AFF_1:6; ( LIN c,q,b & LIN c,q,c ) by A96, AFF_1:6, AFF_1:7; hence contradiction by A91, A102, A107, AFF_1:8; ::_thesis: verum end; A108: a <> a9 proof A109: ( LIN p,a,b & LIN p,a,a ) by A94, AFF_1:6, AFF_1:7; assume A110: a = a9 ; ::_thesis: contradiction then LIN p,a,b9 by A95, AFF_1:6; then ( a in P or b = b9 ) by A79, A85, A86, A106, A109, AFF_1:8, AFF_1:25; then A111: LIN b,q,c9 by A81, A83, A89, A97, AFF_1:6, AFF_1:45; ( LIN b,q,c & LIN b,q,b ) by A96, AFF_1:6, AFF_1:7; then ( b = q or c = c9 or b in C ) by A80, A87, A88, A111, AFF_1:8, AFF_1:25; then LIN p,q,a by A82, A85, A94, A101, A99, A110, AFF_1:2, AFF_1:6, AFF_1:45; then p,q // p,a by AFF_1:def_1; then a,c // p,a by A93, A98, AFF_1:5; then a,c // a,p by AFF_1:4; then LIN a,c,p by AFF_1:def_1; then A112: LIN p,a,c by AFF_1:6; ( LIN p,a,b & LIN p,a,a ) by A94, AFF_1:6, AFF_1:7; hence contradiction by A91, A106, A112, AFF_1:8; ::_thesis: verum end; A113: not LIN p,a,a9 proof assume A114: LIN p,a,a9 ; ::_thesis: contradiction ( LIN p,a,b & LIN p,a,a ) by A94, AFF_1:6, AFF_1:7; then b in A by A78, A83, A84, A106, A108, A114, AFF_1:8, AFF_1:25; hence contradiction by A81, A85, A89, AFF_1:45; ::_thesis: verum end; set A9 = Line (a,c); set P9 = Line (p,q); set C9 = Line (a9,c9); A115: a <> c by A91, AFF_1:7; then A116: Line (a,c) is being_line by AFF_1:24; A117: ( c,c9 // a,a9 & LIN q,c,b ) by A83, A84, A87, A88, A90, A96, AFF_1:6, AFF_1:39; A118: LIN p,a9,b9 by A95, AFF_1:6; A119: ( a in Line (a,c) & c in Line (a,c) ) by A115, AFF_1:24; A120: b <> b9 proof assume b = b9 ; ::_thesis: contradiction then A121: LIN b,p,a9 by A95, AFF_1:6; ( LIN b,p,a & LIN b,p,b ) by A94, AFF_1:6, AFF_1:7; then A122: ( b = p or b in A ) by A78, A83, A84, A108, A121, AFF_1:8, AFF_1:25; then LIN p,q,c by A81, A85, A89, A96, AFF_1:6, AFF_1:45; then p,q // p,c by AFF_1:def_1; then a,c // p,c by A93, A98, AFF_1:5; then c,a // c,p by AFF_1:4; then LIN c,a,p by AFF_1:def_1; hence contradiction by A81, A85, A89, A91, A122, AFF_1:6, AFF_1:45; ::_thesis: verum end; A123: not LIN q,c,c9 proof assume A124: LIN q,c,c9 ; ::_thesis: contradiction ( LIN q,c,b & LIN q,c,c ) by A96, AFF_1:6, AFF_1:7; then ( c = c9 or b in C ) by A80, A87, A88, A102, A124, AFF_1:8, AFF_1:25; then A125: LIN q,c,b9 by A82, A85, A97, A99, AFF_1:6, AFF_1:45; ( LIN q,c,b & LIN q,c,c ) by A96, AFF_1:6, AFF_1:7; then c in P by A79, A85, A86, A102, A120, A125, AFF_1:8, AFF_1:25; hence contradiction by A82, A87, A99, AFF_1:45; ::_thesis: verum end; A126: ( LIN q,c9,b9 & LIN p,a,b ) by A94, A97, AFF_1:6; A127: a9 <> c9 by A92, AFF_1:7; then A128: Line (a9,c9) is being_line by AFF_1:24; A129: p in Line (p,q) by A93, AFF_1:24; A130: Line (a,c) <> Line (p,q) proof assume Line (a,c) = Line (p,q) ; ::_thesis: contradiction then A131: ( LIN p,a,c & LIN p,a,a ) by A116, A119, A129, AFF_1:21; LIN p,a,b by A94, AFF_1:6; hence contradiction by A91, A106, A131, AFF_1:8; ::_thesis: verum end; A132: ( Line (p,q) is being_line & q in Line (p,q) ) by A93, AFF_1:24; then A133: Line (a,c) // Line (p,q) by A93, A98, A115, A116, A119, A129, AFF_1:38; A134: ( a9 in Line (a9,c9) & c9 in Line (a9,c9) ) by A127, AFF_1:24; then Line (a,c) <> Line (a9,c9) by A101, A116, A119, AFF_1:51; then Line (a,c) // Line (a9,c9) by A77, A127, A116, A128, A119, A129, A132, A134, A100, A133, A130, A120, A123, A113, A117, A126, A118, Def8; hence contradiction by A101, A119, A134, AFF_1:39; ::_thesis: verum end; end; hence ( AP is satisfying_DES2_1 iff AP is satisfying_DES2_3 ) by A1; ::_thesis: verum end; theorem :: AFF_3:9 for AP being AffinPlane holds ( AP is satisfying_DES2 iff AP is satisfying_DES2_2 ) proof let AP be AffinPlane; ::_thesis: ( AP is satisfying_DES2 iff AP is satisfying_DES2_2 ) A1: ( AP is satisfying_DES2 implies AP is satisfying_DES2_2 ) proof assume A2: AP is satisfying_DES2 ; ::_thesis: AP is satisfying_DES2_2 thus AP is satisfying_DES2_2 ::_thesis: verum proof let A be Subset of AP; :: according to AFF_3:def_7 ::_thesis: for P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds A // P let P, C be Subset of AP; ::_thesis: for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q holds A // P let a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 & a,c // p,q implies A // P ) assume that A3: A is being_line and A4: P is being_line and A5: C is being_line and A6: A <> P and A7: A <> C and A8: P <> C and A9: ( a in A & a9 in A ) and A10: ( b in P & b9 in P ) and A11: c in C and A12: c9 in C and A13: A // C and A14: not LIN b,a,c and A15: not LIN b9,a9,c9 and A16: p <> q and A17: a <> a9 and A18: LIN b,a,p and A19: LIN b9,a9,p and A20: LIN b,c,q and A21: LIN b9,c9,q and A22: a,c // a9,c9 and A23: a,c // p,q ; ::_thesis: A // P A24: LIN q,c9,b9 by A21, AFF_1:6; A25: c <> c9 proof assume c = c9 ; ::_thesis: contradiction then c,a // c,a9 by A22, AFF_1:4; then LIN c,a,a9 by AFF_1:def_1; then LIN a,a9,c by AFF_1:6; then c in A by A3, A9, A17, AFF_1:25; hence contradiction by A7, A11, A13, AFF_1:45; ::_thesis: verum end; A26: b <> b9 proof A27: now__::_thesis:_(_b_=_p_implies_not_b_in_C_) assume that A28: b = p and b in C ; ::_thesis: contradiction LIN p,q,c by A20, A28, AFF_1:6; then p,q // p,c by AFF_1:def_1; then a,c // p,c by A16, A23, AFF_1:5; then c,a // c,p by AFF_1:4; then LIN c,a,p by AFF_1:def_1; hence contradiction by A14, A28, AFF_1:6; ::_thesis: verum end; A29: ( LIN b,p,a & LIN b,p,b ) by A18, AFF_1:6, AFF_1:7; assume A30: b = b9 ; ::_thesis: contradiction then LIN b,p,a9 by A19, AFF_1:6; then A31: ( b = p or b in A ) by A3, A9, A17, A29, AFF_1:8, AFF_1:25; A32: ( LIN b,q,c & LIN b,q,b ) by A20, AFF_1:6, AFF_1:7; LIN b,q,c9 by A21, A30, AFF_1:6; then A33: ( b = q or b in C ) by A5, A11, A12, A25, A32, AFF_1:8, AFF_1:25; then LIN q,p,a by A7, A13, A18, A31, A27, AFF_1:6, AFF_1:45; then q,p // q,a by AFF_1:def_1; then p,q // q,a by AFF_1:4; then a,c // q,a by A16, A23, AFF_1:5; then a,c // a,q by AFF_1:4; then LIN a,c,q by AFF_1:def_1; hence contradiction by A7, A13, A14, A31, A33, A27, AFF_1:6, AFF_1:45; ::_thesis: verum end; A34: a <> p proof assume A35: a = p ; ::_thesis: contradiction then LIN a,c,q by A23, AFF_1:def_1; then A36: LIN c,q,a by AFF_1:6; ( LIN c,q,b & LIN c,q,c ) by A20, AFF_1:6, AFF_1:7; then q = c by A14, A36, AFF_1:8; then LIN c,c9,b9 by A21, AFF_1:6; then A37: ( c = c9 or b9 in C ) by A5, A11, A12, AFF_1:25; LIN a,a9,b9 by A19, A35, AFF_1:6; then b9 in A by A3, A9, A17, AFF_1:25; then c,a // c,a9 by A7, A13, A22, A37, AFF_1:4, AFF_1:45; then LIN c,a,a9 by AFF_1:def_1; then LIN a,a9,c by AFF_1:6; then c in A by A3, A9, A17, AFF_1:25; hence contradiction by A7, A11, A13, AFF_1:45; ::_thesis: verum end; A38: q <> c proof assume q = c ; ::_thesis: contradiction then c,p // c,a by A23, AFF_1:4; then LIN c,p,a by AFF_1:def_1; then A39: LIN p,a,c by AFF_1:6; ( LIN p,a,b & LIN p,a,a ) by A18, AFF_1:6, AFF_1:7; hence contradiction by A14, A34, A39, AFF_1:8; ::_thesis: verum end; A40: LIN q,c,b by A20, AFF_1:6; set A9 = Line (a,c); set P9 = Line (p,q); set C9 = Line (a9,c9); A41: a <> c by A14, AFF_1:7; then A42: c in Line (a,c) by AFF_1:24; A43: a9 <> p proof assume A44: a9 = p ; ::_thesis: contradiction a9,c9 // p,q by A22, A23, A41, AFF_1:5; then LIN a9,c9,q by A44, AFF_1:def_1; then A45: LIN c9,q,a9 by AFF_1:6; ( LIN c9,q,b9 & LIN c9,q,c9 ) by A21, AFF_1:6, AFF_1:7; then q = c9 by A15, A45, AFF_1:8; then LIN c,c9,b by A20, AFF_1:6; then A46: b in C by A5, A11, A12, A25, AFF_1:25; LIN a,a9,b by A18, A44, AFF_1:6; then b in A by A3, A9, A17, AFF_1:25; hence contradiction by A7, A13, A46, AFF_1:45; ::_thesis: verum end; A47: c9 <> q proof assume c9 = q ; ::_thesis: contradiction then a9,c9 // p,c9 by A22, A23, A41, AFF_1:5; then c9,a9 // c9,p by AFF_1:4; then LIN c9,a9,p by AFF_1:def_1; then A48: LIN p,a9,c9 by AFF_1:6; ( LIN p,a9,b9 & LIN p,a9,a9 ) by A19, AFF_1:6, AFF_1:7; hence contradiction by A15, A43, A48, AFF_1:8; ::_thesis: verum end; A49: not LIN q,c9,c proof A50: LIN q,c,c by AFF_1:7; assume A51: LIN q,c9,c ; ::_thesis: contradiction LIN q,c9,c9 by AFF_1:7; then A52: b9 in C by A5, A11, A12, A25, A47, A24, A51, AFF_1:8, AFF_1:25; LIN q,c,c9 by A51, AFF_1:6; then b in C by A5, A11, A12, A38, A25, A40, A50, AFF_1:8, AFF_1:25; hence contradiction by A4, A5, A8, A10, A26, A52, AFF_1:18; ::_thesis: verum end; A53: LIN p,a,b by A18, AFF_1:6; A54: LIN p,a9,b9 by A19, AFF_1:6; A55: not LIN p,a9,a proof A56: LIN p,a,a by AFF_1:7; assume A57: LIN p,a9,a ; ::_thesis: contradiction LIN p,a9,a9 by AFF_1:7; then A58: b9 in A by A3, A9, A17, A43, A54, A57, AFF_1:8, AFF_1:25; LIN p,a,a9 by A57, AFF_1:6; then b in A by A3, A9, A17, A34, A53, A56, AFF_1:8, AFF_1:25; hence contradiction by A3, A4, A6, A10, A26, A58, AFF_1:18; ::_thesis: verum end; A59: a9,a // c9,c by A9, A11, A12, A13, AFF_1:39; A60: q in Line (p,q) by A16, AFF_1:24; A61: a9 <> c9 by A15, AFF_1:7; then A62: a9 in Line (a9,c9) by AFF_1:24; A63: ( Line (a,c) is being_line & a in Line (a,c) ) by A41, AFF_1:24; A64: Line (a9,c9) <> Line (a,c) proof assume Line (a9,c9) = Line (a,c) ; ::_thesis: contradiction then LIN a,a9,c by A63, A42, A62, AFF_1:21; then c in A by A3, A9, A17, AFF_1:25; hence contradiction by A7, A11, A13, AFF_1:45; ::_thesis: verum end; A65: p in Line (p,q) by A16, AFF_1:24; A66: Line (p,q) <> Line (a,c) proof assume Line (p,q) = Line (a,c) ; ::_thesis: contradiction then A67: ( LIN p,a,c & LIN p,a,a ) by A63, A42, A65, AFF_1:21; LIN p,a,b by A18, AFF_1:6; hence contradiction by A14, A34, A67, AFF_1:8; ::_thesis: verum end; A68: c9 in Line (a9,c9) by A61, AFF_1:24; A69: Line (p,q) is being_line by A16, AFF_1:24; A70: Line (a9,c9) <> Line (p,q) proof assume Line (a9,c9) = Line (p,q) ; ::_thesis: contradiction then A71: ( LIN p,a9,c9 & LIN p,a9,a9 ) by A69, A65, A62, A68, AFF_1:21; LIN p,a9,b9 by A19, AFF_1:6; hence contradiction by A15, A43, A71, AFF_1:8; ::_thesis: verum end; A72: Line (a9,c9) is being_line by A61, AFF_1:24; a9,c9 // p,q by A22, A23, A41, AFF_1:5; then A73: Line (a9,c9) // Line (p,q) by A16, A61, A69, A72, A65, A60, A62, A68, AFF_1:38; Line (a9,c9) // Line (a,c) by A22, A41, A61, A72, A63, A42, A62, A68, AFF_1:38; then a9,a // b9,b by A2, A61, A26, A69, A72, A63, A42, A65, A60, A62, A68, A73, A64, A70, A66, A54, A53, A24, A40, A55, A49, A59, Def5; hence A // P by A3, A4, A9, A10, A17, A26, AFF_1:38; ::_thesis: verum end; end; ( AP is satisfying_DES2_2 implies AP is satisfying_DES2 ) proof assume A74: AP is satisfying_DES2_2 ; ::_thesis: AP is satisfying_DES2 thus AP is satisfying_DES2 ::_thesis: verum proof let A be Subset of AP; :: according to AFF_3:def_5 ::_thesis: for P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds a,c // p,q let P, C be Subset of AP; ::_thesis: for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds a,c // p,q let a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 implies a,c // p,q ) assume that A75: A is being_line and P is being_line and A76: C is being_line and A77: A <> P and A78: A <> C and A79: P <> C and A80: ( a in A & a9 in A ) and A81: b in P and A82: b9 in P and A83: c in C and A84: c9 in C and A85: A // P and A86: A // C and A87: not LIN b,a,c and A88: not LIN b9,a9,c9 and A89: p <> q and A90: a <> a9 and A91: LIN b,a,p and A92: LIN b9,a9,p and A93: LIN b,c,q and A94: LIN b9,c9,q and A95: a,c // a9,c9 ; ::_thesis: a,c // p,q A96: LIN p,a,b by A91, AFF_1:6; set A9 = Line (a,c); set P9 = Line (p,q); set C9 = Line (a9,c9); A97: q in Line (p,q) by A89, AFF_1:24; A98: a <> p proof assume a = p ; ::_thesis: contradiction then LIN a,a9,b9 by A92, AFF_1:6; then b9 in A by A75, A80, A90, AFF_1:25; hence contradiction by A77, A82, A85, AFF_1:45; ::_thesis: verum end; A99: not LIN p,a,a9 proof A100: LIN p,a,a by AFF_1:7; assume LIN p,a,a9 ; ::_thesis: contradiction then b in A by A75, A80, A90, A98, A96, A100, AFF_1:8, AFF_1:25; hence contradiction by A77, A81, A85, AFF_1:45; ::_thesis: verum end; A101: ( LIN q,c9,b9 & LIN p,a9,b9 ) by A92, A94, AFF_1:6; A102: a <> c by A87, AFF_1:7; then A103: Line (a,c) is being_line by AFF_1:24; A104: C // P by A85, A86, AFF_1:44; then A105: c,c9 // b,b9 by A81, A82, A83, A84, AFF_1:39; A106: c <> c9 proof assume c = c9 ; ::_thesis: contradiction then c,a // c,a9 by A95, AFF_1:4; then LIN c,a,a9 by AFF_1:def_1; then LIN a,a9,c by AFF_1:6; then c in A by A75, A80, A90, AFF_1:25; hence contradiction by A78, A83, A86, AFF_1:45; ::_thesis: verum end; A107: b <> b9 proof A108: ( LIN b,p,a & LIN b,p,b ) by A91, AFF_1:6, AFF_1:7; assume A109: b = b9 ; ::_thesis: contradiction then LIN b,p,a9 by A92, AFF_1:6; then A110: ( b = p or b in A ) by A75, A80, A90, A108, AFF_1:8, AFF_1:25; A111: ( LIN b,q,c & LIN b,q,b ) by A93, AFF_1:6, AFF_1:7; LIN b,q,c9 by A94, A109, AFF_1:6; then ( b = q or b in C ) by A76, A83, A84, A106, A111, AFF_1:8, AFF_1:25; hence contradiction by A77, A79, A81, A85, A89, A104, A110, AFF_1:45; ::_thesis: verum end; A112: ( a in Line (a,c) & c in Line (a,c) ) by A102, AFF_1:24; A113: ( Line (p,q) is being_line & c,c9 // a,a9 ) by A80, A83, A84, A86, A89, AFF_1:24, AFF_1:39; A114: p in Line (p,q) by A89, AFF_1:24; A115: a9 <> c9 by A88, AFF_1:7; then A116: a9 in Line (a9,c9) by AFF_1:24; A117: Line (a,c) <> Line (a9,c9) proof assume Line (a,c) = Line (a9,c9) ; ::_thesis: contradiction then LIN a,a9,c by A103, A112, A116, AFF_1:21; then c in A by A75, A80, A90, AFF_1:25; hence contradiction by A78, A83, A86, AFF_1:45; ::_thesis: verum end; A118: q <> c proof assume q = c ; ::_thesis: contradiction then LIN c,c9,b9 by A94, AFF_1:6; then b9 in C by A76, A83, A84, A106, AFF_1:25; hence contradiction by A79, A82, A104, AFF_1:45; ::_thesis: verum end; A119: Line (a,c) <> Line (p,q) proof assume Line (a,c) = Line (p,q) ; ::_thesis: contradiction then A120: ( LIN c,q,a & LIN c,q,c ) by A103, A112, A97, AFF_1:21; LIN c,q,b by A93, AFF_1:6; hence contradiction by A87, A118, A120, AFF_1:8; ::_thesis: verum end; A121: LIN q,c,b by A93, AFF_1:6; A122: not LIN q,c,c9 proof A123: LIN q,c,c by AFF_1:7; assume LIN q,c,c9 ; ::_thesis: contradiction then b in C by A76, A83, A84, A106, A118, A121, A123, AFF_1:8, AFF_1:25; hence contradiction by A79, A81, A104, AFF_1:45; ::_thesis: verum end; A124: ( Line (a9,c9) is being_line & c9 in Line (a9,c9) ) by A115, AFF_1:24; then Line (a,c) // Line (a9,c9) by A95, A102, A115, A103, A112, A116, AFF_1:38; then Line (a,c) // Line (p,q) by A74, A102, A107, A103, A112, A114, A97, A116, A124, A113, A105, A121, A96, A101, A119, A117, A122, A99, Def7; hence a,c // p,q by A112, A114, A97, AFF_1:39; ::_thesis: verum end; end; hence ( AP is satisfying_DES2 iff AP is satisfying_DES2_2 ) by A1; ::_thesis: verum end; theorem :: AFF_3:10 for AP being AffinPlane st AP is satisfying_DES1_3 holds AP is satisfying_DES2_1 proof let AP be AffinPlane; ::_thesis: ( AP is satisfying_DES1_3 implies AP is satisfying_DES2_1 ) assume A1: AP is satisfying_DES1_3 ; ::_thesis: AP is satisfying_DES2_1 let A be Subset of AP; :: according to AFF_3:def_6 ::_thesis: for P, C being Subset of AP for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds a,c // a9,c9 let P, C be Subset of AP; ::_thesis: for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds a,c // a9,c9 let a, a9, b, b9, c, c9, p, q be Element of AP; ::_thesis: ( A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q implies a,c // a9,c9 ) assume that A2: A is being_line and A3: P is being_line and A4: C is being_line and A5: A <> P and A6: A <> C and A7: P <> C and A8: a in A and A9: a9 in A and A10: b in P and A11: b9 in P and A12: c in C and A13: c9 in C and A14: A // P and A15: A // C and A16: not LIN b,a,c and A17: not LIN b9,a9,c9 and A18: p <> q and A19: LIN b,a,p and A20: LIN b9,a9,p and A21: LIN b,c,q and A22: LIN b9,c9,q and A23: a,c // p,q ; ::_thesis: a,c // a9,c9 A24: P // C by A14, A15, AFF_1:44; set K = Line (p,q); set M = Line (a,c); set N = Line (a9,c9); A25: a <> c by A16, AFF_1:7; then A26: a in Line (a,c) by AFF_1:24; A27: ( c,c9 // a,a9 & LIN q,c,b ) by A8, A9, A12, A13, A15, A21, AFF_1:6, AFF_1:39; A28: LIN p,a9,b9 by A20, AFF_1:6; C // P by A14, A15, AFF_1:44; then A29: c,c9 // b,b9 by A10, A11, A12, A13, AFF_1:39; A30: ( LIN q,c9,b9 & LIN p,a,b ) by A19, A22, AFF_1:6; A31: c in Line (a,c) by A25, AFF_1:24; assume A32: not a,c // a9,c9 ; ::_thesis: contradiction A33: c <> q proof assume A34: c = q ; ::_thesis: contradiction then c,a // c,p by A23, AFF_1:4; then LIN c,a,p by AFF_1:def_1; then A35: LIN p,a,c by AFF_1:6; ( LIN p,a,b & LIN p,a,a ) by A19, AFF_1:6, AFF_1:7; then p = a by A16, A35, AFF_1:8; then LIN a,a9,b9 by A20, AFF_1:6; then A36: ( a = a9 or b9 in A ) by A2, A8, A9, AFF_1:25; LIN c,c9,b9 by A22, A34, AFF_1:6; then ( c = c9 or b9 in C ) by A4, A12, A13, AFF_1:25; hence contradiction by A5, A7, A11, A14, A32, A24, A36, AFF_1:2, AFF_1:45; ::_thesis: verum end; A37: c <> c9 proof A38: now__::_thesis:_not_p_=_b assume A39: p = b ; ::_thesis: contradiction LIN b,q,c by A21, AFF_1:6; then b,q // b,c by AFF_1:def_1; then ( a,c // b,c or b = q ) by A23, A39, AFF_1:5; then c,a // c,b by A18, A39, AFF_1:4; then LIN c,a,b by AFF_1:def_1; hence contradiction by A16, AFF_1:6; ::_thesis: verum end; A40: ( LIN q,c,b & LIN q,c,c ) by A21, AFF_1:6, AFF_1:7; assume A41: c = c9 ; ::_thesis: contradiction then LIN q,c,b9 by A22, AFF_1:6; then ( b = b9 or c in P ) by A3, A10, A11, A33, A40, AFF_1:8, AFF_1:25; then A42: LIN p,b,a9 by A7, A12, A20, A24, AFF_1:6, AFF_1:45; ( LIN p,b,a & LIN p,b,b ) by A19, AFF_1:6, AFF_1:7; then ( a = a9 or b in A ) by A2, A8, A9, A42, A38, AFF_1:8, AFF_1:25; hence contradiction by A5, A10, A14, A32, A41, AFF_1:2, AFF_1:45; ::_thesis: verum end; A43: b <> b9 proof assume b = b9 ; ::_thesis: contradiction then A44: LIN q,b,c9 by A22, AFF_1:6; ( LIN q,b,c & LIN q,b,b ) by A21, AFF_1:6, AFF_1:7; then A45: ( q = b or b in C ) by A4, A12, A13, A37, A44, AFF_1:8, AFF_1:25; b,a // b,p by A19, AFF_1:def_1; then a,b // p,b by AFF_1:4; then ( a,c // a,b or p = b ) by A7, A10, A23, A24, A45, AFF_1:5, AFF_1:45; then LIN a,c,b by A7, A10, A18, A24, A45, AFF_1:45, AFF_1:def_1; hence contradiction by A16, AFF_1:6; ::_thesis: verum end; A46: not LIN q,c,c9 proof assume A47: LIN q,c,c9 ; ::_thesis: contradiction ( LIN q,c,b & LIN q,c,c ) by A21, AFF_1:6, AFF_1:7; then b in C by A4, A12, A13, A33, A37, A47, AFF_1:8, AFF_1:25; hence contradiction by A7, A10, A24, AFF_1:45; ::_thesis: verum end; A48: a9 <> c9 by A17, AFF_1:7; then A49: Line (a9,c9) is being_line by AFF_1:24; A50: p <> a proof assume p = a ; ::_thesis: contradiction then LIN a,c,q by A23, AFF_1:def_1; then A51: LIN c,q,a by AFF_1:6; ( LIN c,q,b & LIN c,q,c ) by A21, AFF_1:6, AFF_1:7; hence contradiction by A16, A33, A51, AFF_1:8; ::_thesis: verum end; A52: not LIN p,a,a9 proof assume A53: LIN p,a,a9 ; ::_thesis: contradiction ( LIN p,a,b & LIN p,a,a ) by A19, AFF_1:6, AFF_1:7; then ( a = a9 or b in A ) by A2, A8, A9, A50, A53, AFF_1:8, AFF_1:25; then A54: LIN p,a,b9 by A5, A10, A14, A20, AFF_1:6, AFF_1:45; ( LIN p,a,b & LIN p,a,a ) by A19, AFF_1:6, AFF_1:7; then a in P by A3, A10, A11, A43, A50, A54, AFF_1:8, AFF_1:25; hence contradiction by A5, A8, A14, AFF_1:45; ::_thesis: verum end; A55: Line (a,c) is being_line by A25, AFF_1:24; A56: ( Line (p,q) is being_line & q in Line (p,q) ) by A18, AFF_1:24; A57: now__::_thesis:_not_Line_(a,c)_=_Line_(p,q) assume Line (a,c) = Line (p,q) ; ::_thesis: contradiction then A58: ( LIN q,c,a & LIN q,c,c ) by A56, A26, A31, AFF_1:21; LIN q,c,b by A21, AFF_1:6; hence contradiction by A16, A33, A58, AFF_1:8; ::_thesis: verum end; A59: c9 in Line (a9,c9) by A48, AFF_1:24; A60: a9 in Line (a9,c9) by A48, AFF_1:24; then consider x being Element of AP such that A61: x in Line (a,c) and A62: x in Line (a9,c9) by A32, A55, A49, A26, A31, A59, AFF_1:39, AFF_1:58; A63: now__::_thesis:_not_x_=_c assume x = c ; ::_thesis: contradiction then Line (a9,c9) = C by A4, A12, A13, A37, A49, A59, A62, AFF_1:18; hence contradiction by A6, A9, A15, A60, AFF_1:45; ::_thesis: verum end; A64: p in Line (p,q) by A18, AFF_1:24; then A65: Line (a,c) // Line (p,q) by A18, A23, A25, A55, A56, A26, A31, AFF_1:38; A66: now__::_thesis:_not_x_=_c9 assume x = c9 ; ::_thesis: contradiction then Line (a,c) = C by A4, A12, A13, A37, A55, A31, A61, AFF_1:18; hence contradiction by A6, A8, A15, A26, AFF_1:45; ::_thesis: verum end; Line (a,c) <> Line (a9,c9) by A32, A55, A26, A31, A60, A59, AFF_1:51; then x in Line (p,q) by A1, A18, A25, A55, A49, A64, A56, A26, A31, A60, A59, A61, A62, A29, A27, A30, A28, A43, A63, A66, A46, A52, Def4; hence contradiction by A65, A61, A57, AFF_1:45; ::_thesis: verum end;