:: HOMOTHET semantic presentation begin Lm1: for AFP being AffinPlane holds ( AFP is Desarguesian iff for o, a, a9, p, p9, q, q9 being Element of AFP st LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds p,q // p9,q9 ) proof let AFP be AffinPlane; ::_thesis: ( AFP is Desarguesian iff for o, a, a9, p, p9, q, q9 being Element of AFP st LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds p,q // p9,q9 ) thus ( AFP is Desarguesian implies for o, a, a9, p, p9, q, q9 being Element of AFP st LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds p,q // p9,q9 ) ::_thesis: ( ( for o, a, a9, p, p9, q, q9 being Element of AFP st LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds p,q // p9,q9 ) implies AFP is Desarguesian ) proof assume A1: AFP is Desarguesian ; ::_thesis: for o, a, a9, p, p9, q, q9 being Element of AFP st LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds p,q // p9,q9 let o, a, a9, p, p9, q, q9 be Element of AFP; ::_thesis: ( LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 implies p,q // p9,q9 ) assume that A2: LIN o,a,a9 and A3: LIN o,p,p9 and A4: LIN o,q,q9 and A5: not LIN o,a,p and A6: not LIN o,a,q and A7: a,p // a9,p9 and A8: a,q // a9,q9 ; ::_thesis: p,q // p9,q9 set A = Line (o,a); set P = Line (o,p); set C = Line (o,q); A9: a in Line (o,a) by AFF_1:15; A10: o <> a by A5, AFF_1:7; then A11: Line (o,a) is being_line by AFF_1:def_3; A12: o in Line (o,a) by AFF_1:15; then A13: a9 in Line (o,a) by A2, A10, A11, A9, AFF_1:25; A14: q in Line (o,q) by AFF_1:15; then A15: Line (o,a) <> Line (o,q) by A6, A11, A12, A9, AFF_1:21; A16: o in Line (o,p) by AFF_1:15; A17: p in Line (o,p) by AFF_1:15; A18: o <> p by A5, AFF_1:7; then A19: Line (o,p) is being_line by AFF_1:def_3; then A20: p9 in Line (o,p) by A3, A18, A16, A17, AFF_1:25; A21: o in Line (o,q) by AFF_1:15; A22: o <> q by A6, AFF_1:7; then A23: Line (o,q) is being_line by AFF_1:def_3; then A24: q9 in Line (o,q) by A4, A22, A21, A14, AFF_1:25; Line (o,a) <> Line (o,p) by A5, A11, A12, A9, A17, AFF_1:21; hence p,q // p9,q9 by A1, A7, A8, A10, A18, A22, A11, A19, A23, A12, A9, A16, A17, A21, A14, A13, A20, A24, A15, AFF_2:def_4; ::_thesis: verum end; assume A25: for o, a, a9, p, p9, q, q9 being Element of AFP st LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds p,q // p9,q9 ; ::_thesis: AFP is Desarguesian now__::_thesis:_for_A,_P,_C_being_Subset_of_AFP for_o,_a,_b,_c,_a9,_b9,_c9_being_Element_of_AFP_st_o_in_A_&_o_in_P_&_o_in_C_&_o_<>_a_&_o_<>_b_&_o_<>_c_&_a_in_A_&_a9_in_A_&_b_in_P_&_b9_in_P_&_c_in_C_&_c9_in_C_&_A_is_being_line_&_P_is_being_line_&_C_is_being_line_&_A_<>_P_&_A_<>_C_&_a,b_//_a9,b9_&_a,c_//_a9,c9_holds_ b,c_//_b9,c9 let A, P, C be Subset of AFP; ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AFP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9 let o, a, b, c, a9, b9, c9 be Element of AFP; ::_thesis: ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 ) assume that A26: o in A and A27: o in P and A28: o in C and A29: o <> a and A30: o <> b and A31: o <> c and A32: a in A and A33: a9 in A and A34: b in P and A35: b9 in P and A36: c in C and A37: c9 in C and A38: A is being_line and A39: P is being_line and A40: C is being_line and A41: A <> P and A42: A <> C and A43: a,b // a9,b9 and A44: a,c // a9,c9 ; ::_thesis: b,c // b9,c9 A45: LIN o,b,b9 by A27, A34, A35, A39, AFF_1:21; A46: not LIN o,a,c proof assume LIN o,a,c ; ::_thesis: contradiction then c in A by A26, A29, A32, A38, AFF_1:25; hence contradiction by A26, A28, A31, A36, A38, A40, A42, AFF_1:18; ::_thesis: verum end; A47: not LIN o,a,b proof assume LIN o,a,b ; ::_thesis: contradiction then b in A by A26, A29, A32, A38, AFF_1:25; hence contradiction by A26, A27, A30, A34, A38, A39, A41, AFF_1:18; ::_thesis: verum end; A48: LIN o,c,c9 by A28, A36, A37, A40, AFF_1:21; LIN o,a,a9 by A26, A32, A33, A38, AFF_1:21; hence b,c // b9,c9 by A25, A43, A44, A45, A48, A47, A46; ::_thesis: verum end; hence AFP is Desarguesian by AFF_2:def_4; ::_thesis: verum end; Lm2: for AFP being AffinPlane holds ( AFP is Moufangian iff for o being Element of AFP for K being Subset of AFP for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds b,c // b9,c9 ) proof let AFP be AffinPlane; ::_thesis: ( AFP is Moufangian iff for o being Element of AFP for K being Subset of AFP for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds b,c // b9,c9 ) thus ( AFP is Moufangian implies for o being Element of AFP for K being Subset of AFP for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds b,c // b9,c9 ) ::_thesis: ( ( for o being Element of AFP for K being Subset of AFP for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds b,c // b9,c9 ) implies AFP is Moufangian ) proof assume A1: AFP is Moufangian ; ::_thesis: for o being Element of AFP for K being Subset of AFP for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds b,c // b9,c9 let o be Element of AFP; ::_thesis: for K being Subset of AFP for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds b,c // b9,c9 let K be Subset of AFP; ::_thesis: for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds b,c // b9,c9 let c, c9, a, b, a9, b9 be Element of AFP; ::_thesis: ( o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 implies b,c // b9,c9 ) assume that A2: o in K and A3: c in K and A4: c9 in K and A5: K is being_line and A6: LIN o,a,a9 and A7: LIN o,b,b9 and A8: not a in K and A9: a,b // K and A10: a9,b9 // K and A11: a,c // a9,c9 ; ::_thesis: b,c // b9,c9 A12: a,b // a9,b9 by A5, A9, A10, AFF_1:31; A13: now__::_thesis:_(_o_<>_c_implies_b,c_//_b9,c9_) A14: now__::_thesis:_(_a_=_b_implies_b,c_//_b9,c9_) assume A15: a = b ; ::_thesis: b,c // b9,c9 A16: now__::_thesis:_(_a9,o_//_K_implies_not_a9_<>_b9_) A17: not o,a // K by A2, A8, AFF_1:34, AFF_1:35; A18: LIN o,b9,b by A7, AFF_1:6; assume that A19: a9,o // K and A20: a9 <> b9 ; ::_thesis: contradiction o,a // o,a9 by A6, AFF_1:def_1; then a9,o // o,a by AFF_1:4; then A21: ( o,a // K or a9 = o ) by A19, AFF_1:32; then b9 in K by A2, A5, A8, A10, AFF_1:23; hence contradiction by A2, A5, A8, A15, A20, A21, A17, A18, AFF_1:25; ::_thesis: verum end; LIN o,a,o by AFF_1:7; then LIN a9,b9,o by A2, A6, A7, A8, A15, AFF_1:8; then a9,b9 // a9,o by AFF_1:def_1; hence b,c // b9,c9 by A10, A11, A15, A16, AFF_1:32; ::_thesis: verum end; assume o <> c ; ::_thesis: b,c // b9,c9 hence b,c // b9,c9 by A1, A2, A3, A4, A5, A6, A7, A8, A9, A11, A12, A14, AFF_2:def_7; ::_thesis: verum end; now__::_thesis:_(_o_=_c_implies_b,c_//_b9,c9_) assume A22: o = c ; ::_thesis: b,c // b9,c9 then LIN b,b9,c by A7, AFF_1:6; then A23: b,b9 // b,c by AFF_1:def_1; LIN a,c,a9 by A6, A22, AFF_1:6; then LIN a,c,c9 by A3, A8, A11, AFF_1:9; then A24: LIN c,c9,a by AFF_1:6; then LIN c9,b,b9 by A2, A4, A5, A7, A8, A22, AFF_1:25; then LIN b9,b,c9 by AFF_1:6; then b9,b // b9,c9 by AFF_1:def_1; then A25: b,b9 // b9,c9 by AFF_1:4; c = c9 by A3, A4, A5, A8, A24, AFF_1:25; then ( b = b9 implies b,c // b9,c9 ) by AFF_1:2; hence b,c // b9,c9 by A23, A25, AFF_1:5; ::_thesis: verum end; hence b,c // b9,c9 by A13; ::_thesis: verum end; assume A26: for o being Element of AFP for K being Subset of AFP for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds b,c // b9,c9 ; ::_thesis: AFP is Moufangian now__::_thesis:_for_K_being_Subset_of_AFP for_o,_a,_b,_c,_a9,_b9,_c9_being_Element_of_AFP_st_K_is_being_line_&_o_in_K_&_c_in_K_&_c9_in_K_&_not_a_in_K_&_o_<>_c_&_a_<>_b_&_LIN_o,a,a9_&_LIN_o,b,b9_&_a,b_//_a9,b9_&_a,c_//_a9,c9_&_a,b_//_K_holds_ b,c_//_b9,c9 let K be Subset of AFP; ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AFP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K holds b,c // b9,c9 let o, a, b, c, a9, b9, c9 be Element of AFP; ::_thesis: ( K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K implies b,c // b9,c9 ) assume that A27: K is being_line and A28: o in K and A29: c in K and A30: c9 in K and A31: not a in K and o <> c and A32: a <> b and A33: LIN o,a,a9 and A34: LIN o,b,b9 and A35: a,b // a9,b9 and A36: a,c // a9,c9 and A37: a,b // K ; ::_thesis: b,c // b9,c9 a9,b9 // K by A32, A35, A37, AFF_1:32; hence b,c // b9,c9 by A26, A27, A28, A29, A30, A31, A33, A34, A36, A37; ::_thesis: verum end; hence AFP is Moufangian by AFF_2:def_7; ::_thesis: verum end; Lm3: for AFP being AffinPlane st AFP is Moufangian holds for K being Subset of AFP for o, a, b, c, a9, b9, c9 being Element of AFP st K is being_line & o in K & c in K & c9 in K & not a in K & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds LIN o,b,b9 proof let AFP be AffinPlane; ::_thesis: ( AFP is Moufangian implies for K being Subset of AFP for o, a, b, c, a9, b9, c9 being Element of AFP st K is being_line & o in K & c in K & c9 in K & not a in K & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds LIN o,b,b9 ) assume A1: AFP is Moufangian ; ::_thesis: for K being Subset of AFP for o, a, b, c, a9, b9, c9 being Element of AFP st K is being_line & o in K & c in K & c9 in K & not a in K & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds LIN o,b,b9 thus for K being Subset of AFP for o, a, b, c, a9, b9, c9 being Element of AFP st K is being_line & o in K & c in K & c9 in K & not a in K & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds LIN o,b,b9 ::_thesis: verum proof let K be Subset of AFP; ::_thesis: for o, a, b, c, a9, b9, c9 being Element of AFP st K is being_line & o in K & c in K & c9 in K & not a in K & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds LIN o,b,b9 let o, a, b, c, a9, b9, c9 be Element of AFP; ::_thesis: ( K is being_line & o in K & c in K & c9 in K & not a in K & a <> b & LIN o,a,a9 & a,b // a9,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K implies LIN o,b,b9 ) assume that A2: K is being_line and A3: o in K and A4: c in K and A5: c9 in K and A6: not a in K and A7: a <> b and A8: LIN o,a,a9 and A9: a,b // a9,b9 and A10: b,c // b9,c9 and A11: a,c // a9,c9 and A12: a,b // K ; ::_thesis: LIN o,b,b9 consider P being Subset of AFP such that A13: a9 in P and A14: K // P by A2, AFF_1:49; A15: P is being_line by A14, AFF_1:36; set A = Line (o,b); set C = Line (o,a); A16: o in Line (o,b) by AFF_1:15; A17: b in Line (o,b) by AFF_1:15; assume A18: not LIN o,b,b9 ; ::_thesis: contradiction then o <> b by AFF_1:7; then A19: Line (o,b) is being_line by AFF_1:def_3; A20: not b in K by A6, A12, AFF_1:35; not Line (o,b) // P proof assume Line (o,b) // P ; ::_thesis: contradiction then Line (o,b) // K by A14, AFF_1:44; hence contradiction by A3, A20, A16, A17, AFF_1:45; ::_thesis: verum end; then consider x being Element of AFP such that A21: x in Line (o,b) and A22: x in P by A19, A15, AFF_1:58; A23: o in Line (o,a) by AFF_1:15; a,b // P by A12, A14, AFF_1:43; then a9,b9 // P by A7, A9, AFF_1:32; then A24: b9 in P by A13, A15, AFF_1:23; then A25: LIN b9,x,b9 by A15, A22, AFF_1:21; A26: a in Line (o,a) by AFF_1:15; A27: LIN o,b,x by A19, A16, A17, A21, AFF_1:21; A28: Line (o,a) is being_line by A3, A6, AFF_1:def_3; then A29: a9 in Line (o,a) by A3, A6, A8, A23, A26, AFF_1:25; A30: b9 <> c9 proof A31: a9,c9 // c,a by A11, AFF_1:4; assume A32: b9 = c9 ; ::_thesis: contradiction then P = K by A5, A14, A24, AFF_1:45; then a9 = o by A2, A3, A6, A28, A23, A26, A29, A13, AFF_1:18; then b9 = o by A2, A3, A4, A5, A6, A32, A31, AFF_1:48; hence contradiction by A18, AFF_1:7; ::_thesis: verum end; A33: a9 <> b9 proof assume A34: a9 = b9 ; ::_thesis: contradiction A35: now__::_thesis:_not_a9_=_c9 assume a9 = c9 ; ::_thesis: contradiction then b9 = o by A2, A3, A5, A6, A28, A23, A26, A29, A34, AFF_1:18; hence contradiction by A18, AFF_1:7; ::_thesis: verum end; ( a,c // b,c or a9 = c9 ) by A10, A11, A34, AFF_1:5; then c,a // c,b by A35, AFF_1:4; then LIN c,a,b by AFF_1:def_1; then LIN a,c,b by AFF_1:6; then a,c // a,b by AFF_1:def_1; then a,b // a,c by AFF_1:4; then a,c // K by A7, A12, AFF_1:32; then c,a // K by AFF_1:34; hence contradiction by A2, A4, A6, AFF_1:23; ::_thesis: verum end; A36: b <> c by A4, A6, A12, AFF_1:35; a9,x // K by A13, A14, A22, AFF_1:40; then b,c // x,c9 by A1, A2, A3, A4, A5, A6, A8, A11, A12, A27, Lm2; then b9,c9 // x,c9 by A10, A36, AFF_1:5; then c9,b9 // c9,x by AFF_1:4; then LIN c9,b9,x by AFF_1:def_1; then A37: LIN b9,x,c9 by AFF_1:6; LIN b9,x,a9 by A13, A15, A22, A24, AFF_1:21; then LIN b9,c9,a9 by A18, A27, A37, A25, AFF_1:8; then b9,c9 // b9,a9 by AFF_1:def_1; then b9,c9 // a9,b9 by AFF_1:4; then b,c // a9,b9 by A10, A30, AFF_1:5; then a,b // b,c by A9, A33, AFF_1:5; then b,c // K by A7, A12, AFF_1:32; then c,b // K by AFF_1:34; hence contradiction by A2, A4, A20, AFF_1:23; ::_thesis: verum end; end; Lm4: for AFP being AffinPlane st AFP is Moufangian holds for K, A, C being Subset of AFP for p, q, a, a9, b, b9 being Element of AFP st K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a9 in A & b in C & b9 in C & p,a // q,a9 & p,b // q,b9 holds a,b // a9,b9 proof let AFP be AffinPlane; ::_thesis: ( AFP is Moufangian implies for K, A, C being Subset of AFP for p, q, a, a9, b, b9 being Element of AFP st K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a9 in A & b in C & b9 in C & p,a // q,a9 & p,b // q,b9 holds a,b // a9,b9 ) assume AFP is Moufangian ; ::_thesis: for K, A, C being Subset of AFP for p, q, a, a9, b, b9 being Element of AFP st K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a9 in A & b in C & b9 in C & p,a // q,a9 & p,b // q,b9 holds a,b // a9,b9 then A1: AFP is translational by AFF_2:14; let K, A, C be Subset of AFP; ::_thesis: for p, q, a, a9, b, b9 being Element of AFP st K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a9 in A & b in C & b9 in C & p,a // q,a9 & p,b // q,b9 holds a,b // a9,b9 let p, q, a, a9, b, b9 be Element of AFP; ::_thesis: ( K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a9 in A & b in C & b9 in C & p,a // q,a9 & p,b // q,b9 implies a,b // a9,b9 ) assume that A2: K // A and A3: K // C and A4: K <> A and A5: K <> C and A6: p in K and A7: q in K and A8: a in A and A9: a9 in A and A10: b in C and A11: b9 in C and A12: p,a // q,a9 and A13: p,b // q,b9 ; ::_thesis: a,b // a9,b9 A14: A is being_line by A2, AFF_1:36; A15: C is being_line by A3, AFF_1:36; K is being_line by A2, AFF_1:36; hence a,b // a9,b9 by A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A1, A14, A15, AFF_2:def_11; ::_thesis: verum end; theorem Th1: :: HOMOTHET:1 for AFP being AffinPlane for o, a, p, b, x, y, p9, q, q9 being Element of AFP st not LIN o,a,p & LIN o,a,b & LIN o,a,x & LIN o,a,y & LIN o,p,p9 & LIN o,p,q & LIN o,p,q9 & p <> q & o <> q & o <> x & a,p // b,p9 & a,q // b,q9 & x,p // y,p9 & AFP is Desarguesian holds x,q // y,q9 proof let AFP be AffinPlane; ::_thesis: for o, a, p, b, x, y, p9, q, q9 being Element of AFP st not LIN o,a,p & LIN o,a,b & LIN o,a,x & LIN o,a,y & LIN o,p,p9 & LIN o,p,q & LIN o,p,q9 & p <> q & o <> q & o <> x & a,p // b,p9 & a,q // b,q9 & x,p // y,p9 & AFP is Desarguesian holds x,q // y,q9 let o, a, p, b, x, y, p9, q, q9 be Element of AFP; ::_thesis: ( not LIN o,a,p & LIN o,a,b & LIN o,a,x & LIN o,a,y & LIN o,p,p9 & LIN o,p,q & LIN o,p,q9 & p <> q & o <> q & o <> x & a,p // b,p9 & a,q // b,q9 & x,p // y,p9 & AFP is Desarguesian implies x,q // y,q9 ) assume that A1: not LIN o,a,p and A2: LIN o,a,b and A3: LIN o,a,x and A4: LIN o,a,y and A5: LIN o,p,p9 and A6: LIN o,p,q and A7: LIN o,p,q9 and A8: p <> q and A9: o <> q and A10: o <> x and A11: a,p // b,p9 and A12: a,q // b,q9 and A13: x,p // y,p9 and A14: AFP is Desarguesian ; ::_thesis: x,q // y,q9 set B9 = Line (o,p); A15: o in Line (o,p) by AFF_1:15; A16: o <> p by A1, AFF_1:7; then consider d being Element of AFP such that A17: LIN x,p,d and A18: d <> x and A19: d <> p by A6, A8, A9, TRANSLAC:1; A20: Line (o,p) is being_line by A16, AFF_1:def_3; A21: q9 in Line (o,p) by A7, AFF_1:def_2; q in Line (o,p) by A6, AFF_1:def_2; then A22: LIN o,q,q9 by A20, A15, A21, AFF_1:21; set A = Line (o,a); o <> a by A1, AFF_1:7; then A23: Line (o,a) is being_line by AFF_1:def_3; A24: y in Line (o,a) by A4, AFF_1:def_2; A25: p,a // p9,b by A11, AFF_1:4; A26: not LIN o,p,a by A1, AFF_1:6; set K = Line (x,p); A27: Line (x,p) is being_line by A1, A3, AFF_1:def_3; then consider M being Subset of AFP such that A28: y in M and A29: Line (x,p) // M by AFF_1:49; A30: x in Line (x,p) by AFF_1:15; A31: M is being_line by A29, AFF_1:36; A32: p in Line (x,p) by AFF_1:15; A33: d in Line (x,p) by A17, AFF_1:def_2; A34: x in Line (o,a) by A3, AFF_1:def_2; A35: not LIN o,a,d proof assume LIN o,a,d ; ::_thesis: contradiction then d in Line (o,a) by AFF_1:def_2; then Line (o,a) = Line (x,p) by A18, A27, A30, A33, A23, A34, AFF_1:18; hence contradiction by A1, A32, AFF_1:def_2; ::_thesis: verum end; A36: o in Line (o,a) by AFF_1:15; not o,d // M proof assume o,d // M ; ::_thesis: contradiction then o,d // Line (x,p) by A29, AFF_1:43; then d,o // Line (x,p) by AFF_1:34; then o in Line (x,p) by A27, A33, AFF_1:23; then Line (o,a) = Line (x,p) by A10, A27, A30, A23, A36, A34, AFF_1:18; hence contradiction by A1, A32, AFF_1:def_2; ::_thesis: verum end; then consider d9 being Element of AFP such that A37: d9 in M and A38: LIN o,d,d9 by A31, AFF_1:59; A39: d,x // d9,y by A30, A33, A28, A29, A37, AFF_1:39; A40: p in Line (o,p) by AFF_1:15; A41: not LIN o,d,q proof assume LIN o,d,q ; ::_thesis: contradiction then A42: LIN o,q,d by AFF_1:6; A43: LIN o,q,o by AFF_1:7; LIN o,q,p by A6, AFF_1:6; then LIN o,p,d by A9, A43, A42, AFF_1:8; then d in Line (o,p) by AFF_1:def_2; then Line (o,p) = Line (x,p) by A19, A27, A32, A33, A20, A40, AFF_1:18; then Line (o,a) = Line (o,p) by A10, A27, A30, A23, A36, A34, A15, AFF_1:18; hence contradiction by A1, A40, AFF_1:def_2; ::_thesis: verum end; A44: not LIN o,d,x proof assume LIN o,d,x ; ::_thesis: contradiction then LIN o,x,d by AFF_1:6; then d in Line (o,a) by A10, A23, A36, A34, AFF_1:25; then Line (o,a) = Line (x,p) by A18, A27, A30, A33, A23, A34, AFF_1:18; hence contradiction by A1, A32, AFF_1:def_2; ::_thesis: verum end; A45: not LIN o,p,d proof assume LIN o,p,d ; ::_thesis: contradiction then d in Line (o,p) by AFF_1:def_2; then Line (x,p) = Line (o,p) by A19, A27, A32, A33, A20, A40, AFF_1:18; hence contradiction by A27, A30, A33, A15, A44, AFF_1:21; ::_thesis: verum end; A46: q in Line (o,p) by A6, AFF_1:def_2; A47: not LIN o,a,q proof assume LIN o,a,q ; ::_thesis: contradiction then q in Line (o,a) by AFF_1:def_2; then Line (o,a) = Line (o,p) by A9, A23, A36, A20, A15, A46, AFF_1:18; hence contradiction by A1, A40, AFF_1:def_2; ::_thesis: verum end; x in Line (o,a) by A3, AFF_1:def_2; then A48: LIN o,x,y by A23, A36, A24, AFF_1:21; x,p // Line (x,p) by A27, A30, A32, AFF_1:23; then x,p // M by A29, AFF_1:43; then y,p9 // M by A1, A3, A13, AFF_1:32; then p9 in M by A28, A31, AFF_1:23; then p,d // p9,d9 by A32, A33, A29, A37, AFF_1:39; then a,d // b,d9 by A2, A5, A14, A38, A45, A26, A25, Lm1; then d,q // d9,q9 by A2, A12, A14, A38, A47, A35, A22, Lm1; hence x,q // y,q9 by A14, A38, A39, A41, A44, A22, A48, Lm1; ::_thesis: verum end; theorem Th2: :: HOMOTHET:2 for AFP being AffinPlane st ( for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds ex f being Permutation of the carrier of AFP st ( f is dilatation & f . o = o & f . a = b ) ) holds AFP is Desarguesian proof let AFP be AffinPlane; ::_thesis: ( ( for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds ex f being Permutation of the carrier of AFP st ( f is dilatation & f . o = o & f . a = b ) ) implies AFP is Desarguesian ) assume A1: for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds ex f being Permutation of the carrier of AFP st ( f is dilatation & f . o = o & f . a = b ) ; ::_thesis: AFP is Desarguesian now__::_thesis:_for_o,_a,_a9,_p,_p9,_q,_q9_being_Element_of_AFP_st_LIN_o,a,a9_&_LIN_o,p,p9_&_LIN_o,q,q9_&_not_LIN_o,a,p_&_not_LIN_o,a,q_&_a,p_//_a9,p9_&_a,q_//_a9,q9_holds_ p,q_//_p9,q9 let o, a, a9, p, p9, q, q9 be Element of AFP; ::_thesis: ( LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 implies p,q // p9,q9 ) assume that A2: LIN o,a,a9 and A3: LIN o,p,p9 and A4: LIN o,q,q9 and A5: not LIN o,a,p and A6: not LIN o,a,q and A7: a,p // a9,p9 and A8: a,q // a9,q9 ; ::_thesis: p,q // p9,q9 A9: now__::_thesis:_(_o_<>_a9_implies_p,q_//_p9,q9_) assume A10: o <> a9 ; ::_thesis: p,q // p9,q9 o <> a by A5, AFF_1:7; then consider f being Permutation of the carrier of AFP such that A11: f is dilatation and A12: f . o = o and A13: f . a = a9 by A1, A2, A10; set s = f . q; o,q // o,f . q by A11, A12, TRANSGEO:64; then A14: LIN o,q,f . q by AFF_1:def_1; set r = f . p; o,p // o,f . p by A11, A12, TRANSGEO:64; then A15: LIN o,p,f . p by AFF_1:def_1; a,q // a9,f . q by A11, A13, TRANSGEO:64; then A16: f . q = q9 by A2, A4, A6, A8, A14, AFF_1:56; a,p // a9,f . p by A11, A13, TRANSGEO:64; then f . p = p9 by A2, A3, A5, A7, A15, AFF_1:56; hence p,q // p9,q9 by A11, A16, TRANSGEO:64; ::_thesis: verum end; now__::_thesis:_(_o_=_a9_implies_p,q_//_p9,q9_) assume A17: o = a9 ; ::_thesis: p,q // p9,q9 then o = p9 by A3, A5, A7, AFF_1:55; then p9 = q9 by A4, A6, A8, A17, AFF_1:55; hence p,q // p9,q9 by AFF_1:3; ::_thesis: verum end; hence p,q // p9,q9 by A9; ::_thesis: verum end; hence AFP is Desarguesian by Lm1; ::_thesis: verum end; Lm5: for AFP being AffinPlane for o, a, b, y, x being Element of AFP st o <> a & o <> b & LIN o,a,b & LIN o,a,y & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) holds LIN o,a,x proof let AFP be AffinPlane; ::_thesis: for o, a, b, y, x being Element of AFP st o <> a & o <> b & LIN o,a,b & LIN o,a,y & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) holds LIN o,a,x let o, a, b, y, x be Element of AFP; ::_thesis: ( o <> a & o <> b & LIN o,a,b & LIN o,a,y & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) implies LIN o,a,x ) assume that A1: o <> a and A2: o <> b and A3: LIN o,a,b and A4: LIN o,a,y and A5: ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ; ::_thesis: LIN o,a,x assume A6: not LIN o,a,x ; ::_thesis: contradiction then A7: b <> y by A2, A3, A5, AFF_1:54; set A = Line (o,a); A8: Line (o,a) is being_line by A1, AFF_1:def_3; A9: b,y // a,x by A5, A6, AFF_1:4; A10: a in Line (o,a) by AFF_1:15; A11: y in Line (o,a) by A4, AFF_1:def_2; A12: o in Line (o,a) by AFF_1:15; b in Line (o,a) by A3, AFF_1:def_2; then Line (o,a) = Line (b,y) by A8, A7, A11, AFF_1:24; then x in Line (o,a) by A7, A10, A9, AFF_1:22; hence contradiction by A6, A8, A12, A10, AFF_1:21; ::_thesis: verum end; Lm6: for AFP being AffinPlane for o, a, b, x, y being Element of AFP st o <> a & o <> b & LIN o,a,b & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) holds ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st ( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) ) proof let AFP be AffinPlane; ::_thesis: for o, a, b, x, y being Element of AFP st o <> a & o <> b & LIN o,a,b & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) holds ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st ( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) ) let o, a, b, x, y be Element of AFP; ::_thesis: ( o <> a & o <> b & LIN o,a,b & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) implies ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st ( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) ) ) assume that A1: o <> a and A2: o <> b and A3: LIN o,a,b and A4: ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ; ::_thesis: ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st ( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) ) A5: LIN o,b,a by A3, AFF_1:6; A6: now__::_thesis:_(_LIN_o,a,x_implies_(_o_<>_b_&_o_<>_a_&_LIN_o,b,a_&_(_(_not_LIN_o,b,y_&_LIN_o,y,x_&_b,y_//_a,x_)_or_(_LIN_o,b,y_&_ex_p,_p9_being_Element_of_AFP_st_ (_not_LIN_o,b,p_&_LIN_o,p,p9_&_b,p_//_a,p9_&_p,y_//_p9,x_&_LIN_o,b,x_)_)_)_)_) assume A7: LIN o,a,x ; ::_thesis: ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st ( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) ) then consider p, q being Element of AFP such that A8: not LIN o,a,p and A9: LIN o,p,q and A10: a,p // b,q and A11: p,x // q,y and A12: LIN o,a,y by A4; A13: not LIN o,p,a by A8, AFF_1:6; A14: q,y // p,x by A11, AFF_1:4; A15: b,q // a,p by A10, AFF_1:4; A16: LIN o,q,p by A9, AFF_1:6; LIN o,a,o by AFF_1:7; then A17: LIN o,b,x by A1, A3, A7, AFF_1:8; set A = Line (o,b); A18: o in Line (o,b) by AFF_1:15; A19: a in Line (o,b) by A5, AFF_1:def_2; A20: Line (o,b) is being_line by A2, AFF_1:def_3; p,a // q,b by A10, AFF_1:4; then A21: q <> o by A2, A3, A13, AFF_1:55; A22: not LIN o,b,q proof assume LIN o,b,q ; ::_thesis: contradiction then q in Line (o,b) by AFF_1:def_2; then p in Line (o,b) by A21, A20, A18, A16, AFF_1:25; hence contradiction by A8, A20, A18, A19, AFF_1:21; ::_thesis: verum end; y in Line (o,b) by A1, A12, A20, A18, A19, AFF_1:25; hence ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st ( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) ) by A1, A2, A3, A15, A14, A16, A22, A17, AFF_1:6, AFF_1:def_2; ::_thesis: verum end; now__::_thesis:_(_not_LIN_o,a,x_implies_(_o_<>_b_&_o_<>_a_&_LIN_o,b,a_&_(_(_not_LIN_o,b,y_&_LIN_o,y,x_&_b,y_//_a,x_)_or_(_LIN_o,b,y_&_ex_p,_p9_being_Element_of_AFP_st_ (_not_LIN_o,b,p_&_LIN_o,p,p9_&_b,p_//_a,p9_&_p,y_//_p9,x_&_LIN_o,b,x_)_)_)_)_) assume A23: not LIN o,a,x ; ::_thesis: ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st ( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) ) then A24: not LIN o,a,y by A1, A2, A3, A4, Lm5; not LIN o,b,y proof A25: LIN o,b,o by AFF_1:7; assume A26: LIN o,b,y ; ::_thesis: contradiction LIN o,b,a by A3, AFF_1:6; hence contradiction by A2, A24, A26, A25, AFF_1:8; ::_thesis: verum end; hence ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st ( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) ) by A1, A2, A3, A4, A23, AFF_1:4, AFF_1:6; ::_thesis: verum end; hence ( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st ( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) ) by A6; ::_thesis: verum end; Lm7: for AFP being AffinPlane for o, a, x, y, b being Element of AFP st o <> a & x = o & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) holds y = o proof let AFP be AffinPlane; ::_thesis: for o, a, x, y, b being Element of AFP st o <> a & x = o & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) holds y = o let o, a, x, y, b be Element of AFP; ::_thesis: ( o <> a & x = o & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) implies y = o ) assume that A1: o <> a and A2: x = o and A3: ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ; ::_thesis: y = o consider p, p9 being Element of AFP such that A4: not LIN o,a,p and A5: LIN o,p,p9 and a,p // b,p9 and A6: p,x // p9,y and A7: LIN o,a,y by A2, A3, AFF_1:7; set K = Line (o,p); A8: o <> p by A4, AFF_1:7; p9 in Line (o,p) by A5, AFF_1:def_2; then A9: y in Line (o,p) by A2, A6, A8, AFF_1:22; assume A10: y <> o ; ::_thesis: contradiction A11: o in Line (o,p) by AFF_1:15; A12: p in Line (o,p) by AFF_1:15; set A = Line (o,a); A13: Line (o,a) is being_line by A1, AFF_1:def_3; A14: a in Line (o,a) by AFF_1:15; A15: y in Line (o,a) by A7, AFF_1:def_2; A16: o in Line (o,a) by AFF_1:15; Line (o,p) is being_line by A8, AFF_1:def_3; then p in Line (o,a) by A10, A13, A16, A12, A9, A11, A15, AFF_1:18; hence contradiction by A4, A13, A16, A14, AFF_1:21; ::_thesis: verum end; Lm8: for AFP being AffinPlane for o, a, b, x being Element of AFP st o <> a & LIN o,a,b holds ex y being Element of AFP st ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) proof let AFP be AffinPlane; ::_thesis: for o, a, b, x being Element of AFP st o <> a & LIN o,a,b holds ex y being Element of AFP st ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) let o, a, b, x be Element of AFP; ::_thesis: ( o <> a & LIN o,a,b implies ex y being Element of AFP st ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) assume that A1: o <> a and A2: LIN o,a,b ; ::_thesis: ex y being Element of AFP st ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) A3: now__::_thesis:_(_LIN_o,a,x_implies_ex_y_being_Element_of_AFP_st_ (_(_not_LIN_o,a,x_&_LIN_o,x,y_&_a,x_//_b,y_)_or_(_LIN_o,a,x_&_ex_p,_p9_being_Element_of_AFP_st_ (_not_LIN_o,a,p_&_LIN_o,p,p9_&_a,p_//_b,p9_&_p,x_//_p9,y_&_LIN_o,a,y_)_)_)_) consider p being Element of AFP such that A4: not LIN o,a,p by A1, AFF_1:13; set K = Line (o,p); o <> p by A4, AFF_1:7; then A5: Line (o,p) is being_line by AFF_1:def_3; set A = Line (a,p); a <> p by A4, AFF_1:7; then Line (a,p) is being_line by AFF_1:def_3; then consider B9 being Subset of AFP such that A6: b in B9 and A7: Line (a,p) // B9 by AFF_1:49; A8: B9 is being_line by A7, AFF_1:36; A9: a in Line (a,p) by AFF_1:15; A10: p in Line (o,p) by AFF_1:15; A11: p in Line (a,p) by AFF_1:15; A12: o in Line (o,p) by AFF_1:15; not B9 // Line (o,p) proof assume B9 // Line (o,p) ; ::_thesis: contradiction then Line (a,p) // Line (o,p) by A7, AFF_1:44; then Line (a,p) = Line (o,p) by A10, A11, AFF_1:45; hence contradiction by A4, A12, A10, A9, A5, AFF_1:21; ::_thesis: verum end; then consider p9 being Element of AFP such that A13: p9 in B9 and A14: p9 in Line (o,p) by A5, A8, AFF_1:58; A15: a,p // b,p9 by A9, A11, A6, A7, A13, AFF_1:39; set M = Line (o,a); A16: o in Line (o,a) by AFF_1:15; o <> a by A4, AFF_1:7; then A17: Line (o,a) is being_line by AFF_1:def_3; set C = Line (p,x); assume A18: LIN o,a,x ; ::_thesis: ex y being Element of AFP st ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) then A19: Line (p,x) is being_line by A4, AFF_1:def_3; then consider D being Subset of AFP such that A20: p9 in D and A21: Line (p,x) // D by AFF_1:49; A22: p in Line (p,x) by AFF_1:15; A23: LIN o,p,p9 by A12, A10, A5, A14, AFF_1:21; A24: a in Line (o,a) by AFF_1:15; A25: x in Line (p,x) by AFF_1:15; A26: x in Line (o,a) by A18, AFF_1:def_2; A27: not D // Line (o,a) proof assume D // Line (o,a) ; ::_thesis: contradiction then Line (p,x) // Line (o,a) by A21, AFF_1:44; then Line (p,x) = Line (o,a) by A26, A25, AFF_1:45; hence contradiction by A4, A16, A24, A22, A19, AFF_1:21; ::_thesis: verum end; D is being_line by A21, AFF_1:36; then consider y being Element of AFP such that A28: y in D and A29: y in Line (o,a) by A17, A27, AFF_1:58; A30: LIN o,a,y by A16, A24, A17, A29, AFF_1:21; p,x // p9,y by A22, A25, A20, A21, A28, AFF_1:39; hence ex y being Element of AFP st ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) by A18, A4, A23, A15, A30; ::_thesis: verum end; now__::_thesis:_(_not_LIN_o,a,x_implies_ex_y_being_Element_of_AFP_st_ (_(_not_LIN_o,a,x_&_LIN_o,x,y_&_a,x_//_b,y_)_or_(_LIN_o,a,x_&_ex_p,_p9_being_Element_of_AFP_st_ (_not_LIN_o,a,p_&_LIN_o,p,p9_&_a,p_//_b,p9_&_p,x_//_p9,y_&_LIN_o,a,y_)_)_)_) o,a // o,b by A2, AFF_1:def_1; then a,o // o,b by AFF_1:4; then consider y being Element of AFP such that A31: x,o // o,y and A32: x,a // b,y by A1, DIRAF:40; o,x // o,y by A31, AFF_1:4; then A33: LIN o,x,y by AFF_1:def_1; assume A34: not LIN o,a,x ; ::_thesis: ex y being Element of AFP st ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) a,x // b,y by A32, AFF_1:4; hence ex y being Element of AFP st ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) by A34, A33; ::_thesis: verum end; hence ex y being Element of AFP st ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) by A3; ::_thesis: verum end; Lm9: for AFP being AffinPlane for o, a, b, y being Element of AFP st o <> a & o <> b & LIN o,a,b holds ex x being Element of AFP st ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) proof let AFP be AffinPlane; ::_thesis: for o, a, b, y being Element of AFP st o <> a & o <> b & LIN o,a,b holds ex x being Element of AFP st ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) let o, a, b, y be Element of AFP; ::_thesis: ( o <> a & o <> b & LIN o,a,b implies ex x being Element of AFP st ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) assume that A1: o <> a and A2: o <> b and A3: LIN o,a,b ; ::_thesis: ex x being Element of AFP st ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) A4: LIN o,b,a by A3, AFF_1:6; then consider x being Element of AFP such that A5: ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st ( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) by A2, Lm8; ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) by A1, A2, A4, A5, Lm6; hence ex x being Element of AFP st ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ; ::_thesis: verum end; Lm10: for AFP being AffinPlane for o, a, b, x, y being Element of AFP st o <> a & a = b & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) holds x = y proof let AFP be AffinPlane; ::_thesis: for o, a, b, x, y being Element of AFP st o <> a & a = b & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) holds x = y let o, a, b, x, y be Element of AFP; ::_thesis: ( o <> a & a = b & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) implies x = y ) assume that A1: o <> a and A2: a = b and A3: ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ; ::_thesis: x = y A4: now__::_thesis:_(_LIN_o,a,x_&_x_<>_o_implies_x_=_y_) A5: LIN o,x,x by AFF_1:7; A6: LIN o,a,a by AFF_1:7; assume that A7: LIN o,a,x and A8: x <> o ; ::_thesis: x = y consider p, q being Element of AFP such that A9: not LIN o,a,p and A10: LIN o,p,q and A11: a,p // b,q and A12: p,x // q,y and A13: LIN o,a,y by A3, A7; A14: LIN o,p,p by AFF_1:7; A15: not LIN o,p,x proof assume LIN o,p,x ; ::_thesis: contradiction then A16: LIN o,x,p by AFF_1:6; A17: LIN o,x,o by AFF_1:7; LIN o,x,a by A7, AFF_1:6; hence contradiction by A8, A9, A17, A16, AFF_1:8; ::_thesis: verum end; LIN o,a,o by AFF_1:7; then A18: LIN o,x,y by A1, A7, A13, AFF_1:8; a,p // a,p by AFF_1:2; then A19: p,x // p,y by A2, A9, A10, A11, A12, A6, A14, AFF_1:56; p,x // p,x by AFF_1:2; hence x = y by A14, A15, A18, A19, A5, AFF_1:56; ::_thesis: verum end; now__::_thesis:_(_not_LIN_o,a,x_implies_x_=_y_) A20: LIN o,x,x by AFF_1:7; A21: LIN o,a,a by AFF_1:7; A22: a,x // a,x by AFF_1:2; assume not LIN o,a,x ; ::_thesis: x = y hence x = y by A2, A3, A22, A21, A20, AFF_1:56; ::_thesis: verum end; hence x = y by A1, A3, A4, Lm7; ::_thesis: verum end; Lm11: for AFP being AffinPlane for o, a, b, x, y, r being Element of AFP st o <> a & LIN o,a,b & AFP is Desarguesian & LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,r & LIN o,a,r ) holds y = r proof let AFP be AffinPlane; ::_thesis: for o, a, b, x, y, r being Element of AFP st o <> a & LIN o,a,b & AFP is Desarguesian & LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,r & LIN o,a,r ) holds y = r let o, a, b, x, y, r be Element of AFP; ::_thesis: ( o <> a & LIN o,a,b & AFP is Desarguesian & LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,r & LIN o,a,r ) implies y = r ) assume that A1: o <> a and A2: LIN o,a,b and A3: AFP is Desarguesian and A4: LIN o,a,x and A5: ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) and A6: ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,r & LIN o,a,r ) ; ::_thesis: y = r consider q, q9 being Element of AFP such that A7: not LIN o,a,q and A8: LIN o,q,q9 and A9: a,q // b,q9 and A10: q,x // q9,r and A11: LIN o,a,r by A6; A12: o <> q by A7, AFF_1:7; consider p, p9 being Element of AFP such that A13: not LIN o,a,p and A14: LIN o,p,p9 and A15: a,p // b,p9 and A16: p,x // p9,y and A17: LIN o,a,y by A5; A18: ( a = x implies y = r ) proof A19: q,a // q9,b by A9, AFF_1:4; A20: not LIN o,q,a by A7, AFF_1:6; A21: p,a // p9,b by A15, AFF_1:4; assume A22: a = x ; ::_thesis: y = r not LIN o,p,a by A13, AFF_1:6; then b = y by A2, A14, A16, A17, A22, A21, AFF_1:56; hence y = r by A2, A8, A10, A11, A22, A20, A19, AFF_1:56; ::_thesis: verum end; A23: o <> p by A13, AFF_1:7; A24: ( a <> b & a <> x & p <> q & o <> x implies y = r ) proof assume that a <> b and a <> x and A25: p <> q and A26: o <> x ; ::_thesis: y = r A27: now__::_thesis:_(_LIN_o,p,q_implies_y_=_r_) set K = Line (o,p); set A = Line (o,a); A28: LIN o,q,o by AFF_1:7; A29: o in Line (o,a) by AFF_1:15; A30: p in Line (o,p) by AFF_1:15; A31: o in Line (o,p) by AFF_1:15; A32: Line (o,a) is being_line by A1, AFF_1:def_3; A33: x in Line (o,a) by A4, AFF_1:def_2; r in Line (o,a) by A11, AFF_1:def_2; then A34: LIN o,x,r by A32, A29, A33, AFF_1:21; A35: x,p // y,p9 by A16, AFF_1:4; assume A36: LIN o,p,q ; ::_thesis: y = r then LIN o,q,p by AFF_1:6; then LIN o,p,q9 by A8, A12, A28, AFF_1:8; then x,q // y,q9 by A2, A3, A4, A13, A14, A15, A17, A9, A12, A25, A26, A36, A35, Th1; then A37: q,x // q9,y by AFF_1:4; A38: Line (o,p) is being_line by A23, AFF_1:def_3; A39: q in Line (o,p) by A36, AFF_1:def_2; A40: not LIN o,q,x proof assume A41: LIN o,q,x ; ::_thesis: contradiction Line (o,p) = Line (o,q) by A12, A38, A31, A39, AFF_1:24; then x in Line (o,p) by A41, AFF_1:def_2; then A42: p in Line (o,a) by A26, A32, A29, A33, A38, A31, A30, AFF_1:18; A43: a in Line (o,a) by AFF_1:15; Line (o,a) is being_line by A1, AFF_1:def_3; hence contradiction by A13, A29, A43, A42, AFF_1:21; ::_thesis: verum end; y in Line (o,a) by A17, AFF_1:def_2; then LIN o,x,y by A32, A29, A33, AFF_1:21; hence y = r by A8, A10, A37, A40, A34, AFF_1:56; ::_thesis: verum end; now__::_thesis:_(_not_LIN_o,p,q_implies_y_=_r_) A44: not LIN o,p,x proof assume LIN o,p,x ; ::_thesis: contradiction then A45: LIN o,x,p by AFF_1:6; LIN o,a,o by AFF_1:7; hence contradiction by A4, A13, A26, A45, AFF_1:11; ::_thesis: verum end; set K = Line (o,q); set A = Line (o,a); assume A46: not LIN o,p,q ; ::_thesis: y = r A47: o in Line (o,a) by AFF_1:15; A48: q in Line (o,q) by AFF_1:15; A49: o in Line (o,q) by AFF_1:15; A50: Line (o,a) is being_line by A1, AFF_1:def_3; A51: x in Line (o,a) by A4, AFF_1:def_2; A52: y in Line (o,a) by A17, AFF_1:def_2; then A53: LIN o,x,y by A50, A47, A51, AFF_1:21; A54: Line (o,q) is being_line by A12, AFF_1:def_3; A55: not LIN o,q,x proof assume LIN o,q,x ; ::_thesis: contradiction then x in Line (o,q) by AFF_1:def_2; then A56: q in Line (o,a) by A26, A50, A47, A51, A54, A49, A48, AFF_1:18; A57: a in Line (o,a) by AFF_1:15; Line (o,a) is being_line by A1, AFF_1:def_3; hence contradiction by A7, A47, A57, A56, AFF_1:21; ::_thesis: verum end; r in Line (o,a) by A11, AFF_1:def_2; then A58: LIN o,x,r by A50, A47, A51, AFF_1:21; A59: LIN o,x,y by A50, A47, A51, A52, AFF_1:21; p,q // p9,q9 by A2, A3, A13, A14, A15, A7, A8, A9, Lm1; then q,x // q9,y by A3, A14, A16, A8, A46, A44, A53, Lm1; hence y = r by A8, A10, A55, A59, A58, AFF_1:56; ::_thesis: verum end; hence y = r by A27; ::_thesis: verum end; A60: o <> a by A13, AFF_1:7; A61: ( p = q & o <> x implies y = r ) proof assume that A62: p = q and A63: o <> x ; ::_thesis: y = r A64: not LIN o,p,x proof assume LIN o,p,x ; ::_thesis: contradiction then A65: LIN o,x,p by AFF_1:6; A66: LIN o,x,o by AFF_1:7; LIN o,x,a by A4, AFF_1:6; hence contradiction by A13, A63, A66, A65, AFF_1:8; ::_thesis: verum end; A67: LIN o,a,o by AFF_1:7; then A68: LIN o,x,y by A4, A17, A60, AFF_1:8; A69: LIN o,x,r by A4, A11, A60, A67, AFF_1:8; p9 = q9 by A2, A13, A14, A15, A8, A9, A62, AFF_1:56; hence y = r by A14, A16, A10, A62, A68, A69, A64, AFF_1:56; ::_thesis: verum end; A70: ( o = x implies y = r ) proof assume A71: o = x ; ::_thesis: y = r then y = o by A1, A4, A5, Lm7; hence y = r by A1, A4, A6, A71, Lm7; ::_thesis: verum end; ( a = b implies y = r ) proof assume A72: a = b ; ::_thesis: y = r then x = y by A1, A4, A5, Lm10; hence y = r by A1, A4, A6, A72, Lm10; ::_thesis: verum end; hence y = r by A70, A61, A18, A24; ::_thesis: verum end; Lm12: for AFP being AffinPlane for o, a, b, x, y, r being Element of AFP st o <> a & o <> b & LIN o,a,b & AFP is Desarguesian & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) & ( ( not LIN o,a,r & LIN o,r,y & a,r // b,y ) or ( LIN o,a,r & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,r // p9,y & LIN o,a,y ) ) ) holds x = r proof let AFP be AffinPlane; ::_thesis: for o, a, b, x, y, r being Element of AFP st o <> a & o <> b & LIN o,a,b & AFP is Desarguesian & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) & ( ( not LIN o,a,r & LIN o,r,y & a,r // b,y ) or ( LIN o,a,r & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,r // p9,y & LIN o,a,y ) ) ) holds x = r let o, a, b, x, y, r be Element of AFP; ::_thesis: ( o <> a & o <> b & LIN o,a,b & AFP is Desarguesian & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) & ( ( not LIN o,a,r & LIN o,r,y & a,r // b,y ) or ( LIN o,a,r & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,r // p9,y & LIN o,a,y ) ) ) implies x = r ) assume that A1: o <> a and A2: o <> b and A3: LIN o,a,b and A4: AFP is Desarguesian and A5: ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) and A6: ( ( not LIN o,a,r & LIN o,r,y & a,r // b,y ) or ( LIN o,a,r & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,r // p9,y & LIN o,a,y ) ) ) ; ::_thesis: x = r A7: ( ( not LIN o,b,y & LIN o,y,r & b,y // a,r ) or ( LIN o,b,y & ex p, p9 being Element of AFP st ( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,r & LIN o,b,r ) ) ) by A1, A2, A3, A6, Lm6; A8: LIN o,b,a by A3, AFF_1:6; ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p9 being Element of AFP st ( not LIN o,b,p & LIN o,p,p9 & b,p // a,p9 & p,y // p9,x & LIN o,b,x ) ) ) by A1, A2, A3, A5, Lm6; hence x = r by A2, A4, A8, A7, Lm11, AFF_1:56; ::_thesis: verum end; Lm13: for AFP being AffinPlane for o, a, b being Element of AFP st AFP is Desarguesian & o <> a & o <> b & LIN o,a,b holds ex f being Permutation of the carrier of AFP st for x, y being Element of AFP holds ( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) proof let AFP be AffinPlane; ::_thesis: for o, a, b being Element of AFP st AFP is Desarguesian & o <> a & o <> b & LIN o,a,b holds ex f being Permutation of the carrier of AFP st for x, y being Element of AFP holds ( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) let o, a, b be Element of AFP; ::_thesis: ( AFP is Desarguesian & o <> a & o <> b & LIN o,a,b implies ex f being Permutation of the carrier of AFP st for x, y being Element of AFP holds ( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) ) defpred S1[ Element of AFP, Element of AFP] means ( ( not LIN o,a,$1 & LIN o,$1,$2 & a,$1 // b,$2 ) or ( LIN o,a,$1 & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,$1 // p9,$2 & LIN o,a,$2 ) ) ); assume that A1: AFP is Desarguesian and A2: o <> a and A3: o <> b and A4: LIN o,a,b ; ::_thesis: ex f being Permutation of the carrier of AFP st for x, y being Element of AFP holds ( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) A5: for y being Element of AFP ex x being Element of AFP st S1[x,y] by A2, A3, A4, Lm9; A6: for x being Element of AFP ex y being Element of AFP st S1[x,y] by A2, A4, Lm8; A7: for x, y, s being Element of AFP st S1[x,y] & S1[x,s] holds y = s by A1, A2, A4, Lm11, AFF_1:56; A8: for x, y, r being Element of AFP st S1[x,y] & S1[r,y] holds x = r by A1, A2, A3, A4, Lm12; ex f being Permutation of the carrier of AFP st for x, y being Element of AFP holds ( f . x = y iff S1[x,y] ) from TRANSGEO:sch_1(A6, A5, A8, A7); hence ex f being Permutation of the carrier of AFP st for x, y being Element of AFP holds ( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) ; ::_thesis: verum end; Lm14: for AFP being AffinPlane for o, a, b, x, y, z, t being Element of AFP st AFP is Desarguesian & o <> a & LIN o,a,b & not LIN o,a,x & LIN o,x,y & a,x // b,y & LIN o,a,z & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,t ) holds x,z // y,t proof let AFP be AffinPlane; ::_thesis: for o, a, b, x, y, z, t being Element of AFP st AFP is Desarguesian & o <> a & LIN o,a,b & not LIN o,a,x & LIN o,x,y & a,x // b,y & LIN o,a,z & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,t ) holds x,z // y,t let o, a, b, x, y, z, t be Element of AFP; ::_thesis: ( AFP is Desarguesian & o <> a & LIN o,a,b & not LIN o,a,x & LIN o,x,y & a,x // b,y & LIN o,a,z & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,t ) implies x,z // y,t ) assume that A1: AFP is Desarguesian and A2: o <> a and A3: LIN o,a,b and A4: not LIN o,a,x and A5: LIN o,x,y and A6: a,x // b,y and A7: LIN o,a,z and A8: ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,t ) ; ::_thesis: x,z // y,t consider p, p9 being Element of AFP such that A9: not LIN o,a,p and A10: LIN o,p,p9 and A11: a,p // b,p9 and A12: p,z // p9,t and A13: LIN o,a,t by A8; A14: now__::_thesis:_(_a_=_z_implies_x,z_//_y,t_) A15: p,a // p9,b by A11, AFF_1:4; assume A16: a = z ; ::_thesis: x,z // y,t not LIN o,p,a by A9, AFF_1:6; then z,x // t,y by A3, A6, A10, A12, A13, A16, A15, AFF_1:56; hence x,z // y,t by AFF_1:4; ::_thesis: verum end; A17: p,x // p9,y by A1, A3, A4, A5, A6, A9, A10, A11, Lm1; A18: now__::_thesis:_(_z_<>_o_&_not_LIN_o,p,x_implies_x,z_//_y,t_) assume that A19: z <> o and A20: not LIN o,p,x ; ::_thesis: x,z // y,t A21: not LIN o,p,z proof A22: LIN o,p,o by AFF_1:7; assume A23: LIN o,p,z ; ::_thesis: contradiction LIN o,z,a by A7, AFF_1:6; then LIN o,p,a by A19, A23, A22, AFF_1:11; hence contradiction by A9, AFF_1:6; ::_thesis: verum end; LIN o,a,o by AFF_1:7; then LIN o,z,t by A2, A7, A13, AFF_1:8; hence x,z // y,t by A1, A5, A10, A12, A17, A20, A21, Lm1; ::_thesis: verum end; A24: o <> x by A4, AFF_1:7; A25: now__::_thesis:_(_z_<>_o_&_LIN_o,p,x_&_a_<>_z_implies_x,z_//_y,t_) assume that A26: z <> o and A27: LIN o,p,x and a <> z ; ::_thesis: x,z // y,t now__::_thesis:_(_x_<>_p_implies_x,z_//_y,t_) A28: LIN o,x,o by AFF_1:7; LIN o,x,p by A27, AFF_1:6; then A29: LIN o,p,y by A5, A24, A28, AFF_1:8; assume A30: x <> p ; ::_thesis: x,z // y,t z,p // t,p9 by A12, AFF_1:4; then z,x // t,y by A1, A3, A6, A7, A9, A10, A11, A13, A24, A26, A27, A30, A29, Th1; hence x,z // y,t by AFF_1:4; ::_thesis: verum end; hence x,z // y,t by A3, A4, A5, A6, A10, A11, A12, AFF_1:56; ::_thesis: verum end; now__::_thesis:_(_z_=_o_implies_x,z_//_y,t_) A31: o,x // o,y by A5, AFF_1:def_1; assume A32: z = o ; ::_thesis: x,z // y,t then t = o by A2, A7, A8, Lm7; hence x,z // y,t by A32, A31, AFF_1:4; ::_thesis: verum end; hence x,z // y,t by A18, A14, A25; ::_thesis: verum end; Lm15: for AFP being AffinPlane for o, a, b, x, y, z, t being Element of AFP st AFP is Desarguesian & o <> a & LIN o,a,b & LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & not LIN o,a,z & LIN o,z,t & a,z // b,t holds x,z // y,t proof let AFP be AffinPlane; ::_thesis: for o, a, b, x, y, z, t being Element of AFP st AFP is Desarguesian & o <> a & LIN o,a,b & LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & not LIN o,a,z & LIN o,z,t & a,z // b,t holds x,z // y,t let o, a, b, x, y, z, t be Element of AFP; ::_thesis: ( AFP is Desarguesian & o <> a & LIN o,a,b & LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & not LIN o,a,z & LIN o,z,t & a,z // b,t implies x,z // y,t ) assume that A1: AFP is Desarguesian and A2: o <> a and A3: LIN o,a,b and A4: LIN o,a,x and A5: ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) and A6: not LIN o,a,z and A7: LIN o,z,t and A8: a,z // b,t ; ::_thesis: x,z // y,t z,x // t,y by A1, A2, A3, A4, A5, A6, A7, A8, Lm14; hence x,z // y,t by AFF_1:4; ::_thesis: verum end; Lm16: for AFP being AffinPlane for o, a, x, b, y, z, t being Element of AFP st o <> a & LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & LIN o,a,z & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,t ) holds x,z // y,t proof let AFP be AffinPlane; ::_thesis: for o, a, x, b, y, z, t being Element of AFP st o <> a & LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & LIN o,a,z & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,t ) holds x,z // y,t let o, a, x, b, y, z, t be Element of AFP; ::_thesis: ( o <> a & LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) & LIN o,a,z & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,t ) implies x,z // y,t ) assume that A1: o <> a and A2: LIN o,a,x and A3: ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) and A4: LIN o,a,z and A5: ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,z // p9,t & LIN o,a,t ) ; ::_thesis: x,z // y,t set A = Line (o,a); A6: x in Line (o,a) by A2, AFF_1:def_2; A7: z in Line (o,a) by A4, AFF_1:def_2; A8: y in Line (o,a) by A3, AFF_1:def_2; A9: t in Line (o,a) by A5, AFF_1:def_2; A10: Line (o,a) is being_line by A1, AFF_1:def_3; now__::_thesis:_(_x_<>_z_implies_x,z_//_y,t_) assume A11: x <> z ; ::_thesis: x,z // y,t then Line (o,a) = Line (x,z) by A10, A6, A7, AFF_1:24; hence x,z // y,t by A8, A9, A11, AFF_1:22; ::_thesis: verum end; hence x,z // y,t by AFF_1:3; ::_thesis: verum end; Lm17: for AFP being AffinPlane for o, a, b being Element of AFP for f being Permutation of the carrier of AFP st o <> a & LIN o,a,b & AFP is Desarguesian & ( for x, y being Element of AFP holds ( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) ) holds ( f is dilatation & f . o = o & f . a = b ) proof let AFP be AffinPlane; ::_thesis: for o, a, b being Element of AFP for f being Permutation of the carrier of AFP st o <> a & LIN o,a,b & AFP is Desarguesian & ( for x, y being Element of AFP holds ( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) ) holds ( f is dilatation & f . o = o & f . a = b ) let o, a, b be Element of AFP; ::_thesis: for f being Permutation of the carrier of AFP st o <> a & LIN o,a,b & AFP is Desarguesian & ( for x, y being Element of AFP holds ( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) ) holds ( f is dilatation & f . o = o & f . a = b ) let f be Permutation of the carrier of AFP; ::_thesis: ( o <> a & LIN o,a,b & AFP is Desarguesian & ( for x, y being Element of AFP holds ( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) ) implies ( f is dilatation & f . o = o & f . a = b ) ) assume that A1: o <> a and A2: LIN o,a,b and A3: AFP is Desarguesian ; ::_thesis: ( ex x, y being Element of AFP st ( ( not f . x = y or ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) implies ( ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) & not f . x = y ) ) or ( f is dilatation & f . o = o & f . a = b ) ) assume A4: for x, y being Element of AFP holds ( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) ; ::_thesis: ( f is dilatation & f . o = o & f . a = b ) for x, r being Element of AFP holds x,r // f . x,f . r proof let x, r be Element of AFP; ::_thesis: x,r // f . x,f . r set y = f . x; set s = f . r; A5: ( ( not LIN o,a,r & LIN o,r,f . r & a,r // b,f . r ) or ( LIN o,a,r & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,r // p9,f . r & LIN o,a,f . r ) ) ) by A4; ( ( not LIN o,a,x & LIN o,x,f . x & a,x // b,f . x ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,f . x & LIN o,a,f . x ) ) ) by A4; hence x,r // f . x,f . r by A1, A2, A3, A5, Lm1, Lm14, Lm15, Lm16; ::_thesis: verum end; hence f is dilatation by TRANSGEO:64; ::_thesis: ( f . o = o & f . a = b ) thus f . o = o ::_thesis: f . a = b proof set y = f . o; ( ( not LIN o,a,o & LIN o,o,f . o & a,o // b,f . o ) or ( LIN o,a,o & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,o // p9,f . o & LIN o,a,f . o ) ) ) by A4; hence f . o = o by A1, Lm7; ::_thesis: verum end; thus f . a = b ::_thesis: verum proof set y = f . a; LIN o,a,a by AFF_1:7; then consider p, p9 being Element of AFP such that A6: not LIN o,a,p and A7: LIN o,p,p9 and A8: a,p // b,p9 and A9: p,a // p9,f . a and A10: LIN o,a,f . a by A4; A11: p,a // p9,b by A8, AFF_1:4; not LIN o,p,a by A6, AFF_1:6; hence f . a = b by A2, A7, A9, A10, A11, AFF_1:56; ::_thesis: verum end; end; theorem Th3: :: HOMOTHET:3 for AFP being AffinPlane st AFP is Desarguesian holds for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds ex f being Permutation of the carrier of AFP st ( f is dilatation & f . o = o & f . a = b ) proof let AFP be AffinPlane; ::_thesis: ( AFP is Desarguesian implies for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds ex f being Permutation of the carrier of AFP st ( f is dilatation & f . o = o & f . a = b ) ) assume A1: AFP is Desarguesian ; ::_thesis: for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds ex f being Permutation of the carrier of AFP st ( f is dilatation & f . o = o & f . a = b ) let o, a, b be Element of AFP; ::_thesis: ( o <> a & o <> b & LIN o,a,b implies ex f being Permutation of the carrier of AFP st ( f is dilatation & f . o = o & f . a = b ) ) assume that A2: o <> a and A3: o <> b and A4: LIN o,a,b ; ::_thesis: ex f being Permutation of the carrier of AFP st ( f is dilatation & f . o = o & f . a = b ) consider f being Permutation of the carrier of AFP such that A5: for x, y being Element of AFP holds ( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p9 being Element of AFP st ( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) by A1, A2, A3, A4, Lm13; A6: f . a = b by A1, A2, A4, A5, Lm17; A7: f . o = o by A1, A2, A4, A5, Lm17; f is dilatation by A1, A2, A4, A5, Lm17; hence ex f being Permutation of the carrier of AFP st ( f is dilatation & f . o = o & f . a = b ) by A7, A6; ::_thesis: verum end; theorem :: HOMOTHET:4 for AFP being AffinPlane holds ( AFP is Desarguesian iff for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds ex f being Permutation of the carrier of AFP st ( f is dilatation & f . o = o & f . a = b ) ) by Th2, Th3; definition let AFP be AffinPlane; let f be Permutation of the carrier of AFP; let K be Subset of AFP; predf is_Sc K means :Def1: :: HOMOTHET:def 1 ( f is collineation & K is being_line & ( for x being Element of AFP st x in K holds f . x = x ) & ( for x being Element of AFP holds x,f . x // K ) ); end; :: deftheorem Def1 defines is_Sc HOMOTHET:def_1_:_ for AFP being AffinPlane for f being Permutation of the carrier of AFP for K being Subset of AFP holds ( f is_Sc K iff ( f is collineation & K is being_line & ( for x being Element of AFP st x in K holds f . x = x ) & ( for x being Element of AFP holds x,f . x // K ) ) ); theorem Th5: :: HOMOTHET:5 for AFP being AffinPlane for p being Element of AFP for K being Subset of AFP for f being Permutation of the carrier of AFP st f is_Sc K & f . p = p & not p in K holds f = id the carrier of AFP proof let AFP be AffinPlane; ::_thesis: for p being Element of AFP for K being Subset of AFP for f being Permutation of the carrier of AFP st f is_Sc K & f . p = p & not p in K holds f = id the carrier of AFP let p be Element of AFP; ::_thesis: for K being Subset of AFP for f being Permutation of the carrier of AFP st f is_Sc K & f . p = p & not p in K holds f = id the carrier of AFP let K be Subset of AFP; ::_thesis: for f being Permutation of the carrier of AFP st f is_Sc K & f . p = p & not p in K holds f = id the carrier of AFP let f be Permutation of the carrier of AFP; ::_thesis: ( f is_Sc K & f . p = p & not p in K implies f = id the carrier of AFP ) assume that A1: f is_Sc K and A2: f . p = p and A3: not p in K ; ::_thesis: f = id the carrier of AFP A4: K is being_line by A1, Def1; A5: for x being Element of AFP st x in K holds f . x = x by A1, Def1; f is collineation by A1, Def1; hence f = id the carrier of AFP by A2, A3, A4, A5, TRANSGEO:93; ::_thesis: verum end; theorem Th6: :: HOMOTHET:6 for AFP being AffinPlane st ( for a, b being Element of AFP for K being Subset of AFP st a,b // K & not a in K holds ex f being Permutation of the carrier of AFP st ( f is_Sc K & f . a = b ) ) holds AFP is Moufangian proof let AFP be AffinPlane; ::_thesis: ( ( for a, b being Element of AFP for K being Subset of AFP st a,b // K & not a in K holds ex f being Permutation of the carrier of AFP st ( f is_Sc K & f . a = b ) ) implies AFP is Moufangian ) assume A1: for a, b being Element of AFP for K being Subset of AFP st a,b // K & not a in K holds ex f being Permutation of the carrier of AFP st ( f is_Sc K & f . a = b ) ; ::_thesis: AFP is Moufangian now__::_thesis:_for_o_being_Element_of_AFP for_K_being_Subset_of_AFP for_c,_c9,_a,_b,_a9,_b9_being_Element_of_AFP_st_o_in_K_&_c_in_K_&_c9_in_K_&_K_is_being_line_&_LIN_o,a,a9_&_LIN_o,b,b9_&_not_a_in_K_&_a,b_//_K_&_a9,b9_//_K_&_a,c_//_a9,c9_holds_ b,c_//_b9,c9 let o be Element of AFP; ::_thesis: for K being Subset of AFP for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds b,c // b9,c9 let K be Subset of AFP; ::_thesis: for c, c9, a, b, a9, b9 being Element of AFP st o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 holds b,c // b9,c9 let c, c9, a, b, a9, b9 be Element of AFP; ::_thesis: ( o in K & c in K & c9 in K & K is being_line & LIN o,a,a9 & LIN o,b,b9 & not a in K & a,b // K & a9,b9 // K & a,c // a9,c9 implies b,c // b9,c9 ) assume that A2: o in K and A3: c in K and A4: c9 in K and A5: K is being_line and A6: LIN o,a,a9 and A7: LIN o,b,b9 and A8: not a in K and A9: a,b // K and A10: a9,b9 // K and A11: a,c // a9,c9 ; ::_thesis: b,c // b9,c9 consider f being Permutation of the carrier of AFP such that A12: f is_Sc K and A13: f . a = b by A1, A8, A9; A14: f is collineation by A12, Def1; A15: a,b // a9,b9 by A5, A9, A10, AFF_1:31; A16: f . a9 = b9 proof set x = f . a9; A17: now__::_thesis:_(_a_<>_b_implies_f_._a9_=_b9_) f . o = o by A2, A12, Def1; then A18: LIN o,b,f . a9 by A6, A13, A14, TRANSGEO:84; a9,f . a9 // K by A12, Def1; then A19: a,b // a9,f . a9 by A5, A9, AFF_1:31; assume a <> b ; ::_thesis: f . a9 = b9 hence f . a9 = b9 by A2, A6, A7, A8, A9, A15, A19, A18, AFF_1:46, AFF_1:56; ::_thesis: verum end; now__::_thesis:_(_a_=_b_implies_f_._a9_=_b9_) assume A20: a = b ; ::_thesis: f . a9 = b9 then f = id the carrier of AFP by A8, A12, A13, Th5; then f . a9 = a9 by FUNCT_1:18; hence f . a9 = b9 by A2, A6, A7, A8, A10, A20, AFF_1:47; ::_thesis: verum end; hence f . a9 = b9 by A17; ::_thesis: verum end; A21: f . c9 = c9 by A4, A12, Def1; f . c = c by A3, A12, Def1; hence b,c // b9,c9 by A11, A13, A14, A21, A16, TRANSGEO:83; ::_thesis: verum end; hence AFP is Moufangian by Lm2; ::_thesis: verum end; Lm18: for AFP being AffinPlane for a, b, x, y being Element of AFP for K being Subset of AFP st a,b // K & not a in K & ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) holds ( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,b // p9,y & p,a // p9,x & y,x // K ) ) ) ) proof let AFP be AffinPlane; ::_thesis: for a, b, x, y being Element of AFP for K being Subset of AFP st a,b // K & not a in K & ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) holds ( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,b // p9,y & p,a // p9,x & y,x // K ) ) ) ) let a, b, x, y be Element of AFP; ::_thesis: for K being Subset of AFP st a,b // K & not a in K & ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) holds ( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,b // p9,y & p,a // p9,x & y,x // K ) ) ) ) let K be Subset of AFP; ::_thesis: ( a,b // K & not a in K & ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) implies ( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,b // p9,y & p,a // p9,x & y,x // K ) ) ) ) ) assume that A1: a,b // K and A2: not a in K and A3: ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ; ::_thesis: ( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,b // p9,y & p,a // p9,x & y,x // K ) ) ) ) thus ( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,b // p9,y & p,a // p9,x & y,x // K ) ) ) ) by A1, A2, A3, AFF_1:34, AFF_1:35; ::_thesis: verum end; Lm19: for AFP being AffinPlane for a, b being Element of AFP for K being Subset of AFP st a,b // K & not a in K holds for x being Element of AFP ex y being Element of AFP st ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) proof let AFP be AffinPlane; ::_thesis: for a, b being Element of AFP for K being Subset of AFP st a,b // K & not a in K holds for x being Element of AFP ex y being Element of AFP st ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) let a, b be Element of AFP; ::_thesis: for K being Subset of AFP st a,b // K & not a in K holds for x being Element of AFP ex y being Element of AFP st ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) let K be Subset of AFP; ::_thesis: ( a,b // K & not a in K implies for x being Element of AFP ex y being Element of AFP st ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) assume that A1: a,b // K and A2: not a in K ; ::_thesis: for x being Element of AFP ex y being Element of AFP st ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) A3: not b in K by A1, A2, AFF_1:35; A4: K is being_line by A1, AFF_1:26; let x be Element of AFP; ::_thesis: ex y being Element of AFP st ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) consider p, q being Element of AFP such that A5: p in K and q in K and p <> q by A1, AFF_1:19, AFF_1:26; A6: p <> b by A1, A2, A5, AFF_1:35; now__::_thesis:_(_not_x_in_K_implies_ex_y_being_Element_of_AFP_st_ (_(_x_in_K_&_x_=_y_)_or_(_not_x_in_K_&_ex_p,_p9_being_Element_of_AFP_st_ (_p_in_K_&_p9_in_K_&_p,a_//_p9,x_&_p,b_//_p9,y_&_x,y_//_K_)_)_)_) set B9 = Line (p,b); set A = Line (p,a); assume A7: not x in K ; ::_thesis: ex y being Element of AFP st ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) A8: a in Line (p,a) by AFF_1:15; Line (p,a) is being_line by A2, A5, AFF_1:def_3; then consider C being Subset of AFP such that A9: x in C and A10: Line (p,a) // C by AFF_1:49; A11: C is being_line by A10, AFF_1:36; A12: p in Line (p,a) by AFF_1:15; then not Line (p,a) // K by A2, A5, A8, AFF_1:45; then not C // K by A10, AFF_1:44; then consider p9 being Element of AFP such that A13: p9 in C and A14: p9 in K by A4, A11, AFF_1:58; Line (p,b) is being_line by A6, AFF_1:def_3; then consider D being Subset of AFP such that A15: p9 in D and A16: Line (p,b) // D by AFF_1:49; A17: b in Line (p,b) by AFF_1:15; K is being_line by A1, AFF_1:26; then consider M being Subset of AFP such that A18: x in M and A19: K // M by AFF_1:49; A20: M is being_line by A19, AFF_1:36; A21: p in Line (p,b) by AFF_1:15; then A22: not Line (p,b) // K by A5, A3, A17, AFF_1:45; A23: not D // M proof assume D // M ; ::_thesis: contradiction then Line (p,b) // M by A16, AFF_1:44; hence contradiction by A22, A19, AFF_1:44; ::_thesis: verum end; D is being_line by A16, AFF_1:36; then consider y being Element of AFP such that A24: y in D and A25: y in M by A20, A23, AFF_1:58; A26: p,b // p9,y by A21, A17, A15, A16, A24, AFF_1:39; A27: x,y // K by A18, A19, A25, AFF_1:40; p,a // p9,x by A12, A8, A9, A10, A13, AFF_1:39; hence ex y being Element of AFP st ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) by A5, A7, A14, A27, A26; ::_thesis: verum end; hence ex y being Element of AFP st ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ; ::_thesis: verum end; Lm20: for AFP being AffinPlane for a, b being Element of AFP for K being Subset of AFP st a,b // K & not a in K holds for y being Element of AFP ex x being Element of AFP st ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) proof let AFP be AffinPlane; ::_thesis: for a, b being Element of AFP for K being Subset of AFP st a,b // K & not a in K holds for y being Element of AFP ex x being Element of AFP st ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) let a, b be Element of AFP; ::_thesis: for K being Subset of AFP st a,b // K & not a in K holds for y being Element of AFP ex x being Element of AFP st ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) let K be Subset of AFP; ::_thesis: ( a,b // K & not a in K implies for y being Element of AFP ex x being Element of AFP st ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) assume that A1: a,b // K and A2: not a in K ; ::_thesis: for y being Element of AFP ex x being Element of AFP st ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) let y be Element of AFP; ::_thesis: ex x being Element of AFP st ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) A3: b,a // K by A1, AFF_1:34; A4: not b in K by A1, A2, AFF_1:35; then consider x being Element of AFP such that A5: ( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,b // p9,y & p,a // p9,x & y,x // K ) ) ) by A3, Lm19; ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) by A3, A4, A5, Lm18; hence ex x being Element of AFP st ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ; ::_thesis: verum end; theorem Th7: :: HOMOTHET:7 for AFP being AffinPlane for p, q, p9, q9, a, b, x, y being Element of AFP for K, M being Subset of AFP st K // M & p in K & q in K & p9 in K & q9 in K & AFP is Moufangian & a in M & b in M & x in M & y in M & a <> b & q <> p & p,a // p9,x & p,b // p9,y & q,a // q9,x holds q,b // q9,y proof let AFP be AffinPlane; ::_thesis: for p, q, p9, q9, a, b, x, y being Element of AFP for K, M being Subset of AFP st K // M & p in K & q in K & p9 in K & q9 in K & AFP is Moufangian & a in M & b in M & x in M & y in M & a <> b & q <> p & p,a // p9,x & p,b // p9,y & q,a // q9,x holds q,b // q9,y let p, q, p9, q9, a, b, x, y be Element of AFP; ::_thesis: for K, M being Subset of AFP st K // M & p in K & q in K & p9 in K & q9 in K & AFP is Moufangian & a in M & b in M & x in M & y in M & a <> b & q <> p & p,a // p9,x & p,b // p9,y & q,a // q9,x holds q,b // q9,y let K, M be Subset of AFP; ::_thesis: ( K // M & p in K & q in K & p9 in K & q9 in K & AFP is Moufangian & a in M & b in M & x in M & y in M & a <> b & q <> p & p,a // p9,x & p,b // p9,y & q,a // q9,x implies q,b // q9,y ) assume that A1: K // M and A2: p in K and A3: q in K and A4: p9 in K and A5: q9 in K and A6: AFP is Moufangian and A7: a in M and A8: b in M and A9: x in M and A10: y in M and A11: a <> b and A12: q <> p and A13: p,a // p9,x and A14: p,b // p9,y and A15: q,a // q9,x ; ::_thesis: q,b // q9,y A16: K is being_line by A1, AFF_1:36; A17: M is being_line by A1, AFF_1:36; now__::_thesis:_(_K_<>_M_implies_q,b_//_q9,y_) set D9 = Line (q9,x); set B99 = Line (p9,y); set D = Line (q,a); set B9 = Line (p,b); A18: q in Line (q,a) by AFF_1:15; A19: a in Line (q,a) by AFF_1:15; A20: x in Line (q9,x) by AFF_1:15; A21: q9 in Line (q9,x) by AFF_1:15; A22: LIN p,q,q9 by A2, A3, A5, A16, AFF_1:21; A23: LIN p,q,p9 by A2, A3, A4, A16, AFF_1:21; assume A24: K <> M ; ::_thesis: q,b // q9,y then A25: q9 <> x by A1, A5, A9, AFF_1:45; A26: not a in K by A1, A7, A24, AFF_1:45; A27: b <> p by A1, A2, A8, A24, AFF_1:45; then A28: Line (p,b) is being_line by AFF_1:def_3; A29: not q in M by A1, A3, A24, AFF_1:45; A30: not p in M by A1, A2, A24, AFF_1:45; A31: LIN a,b,x by A7, A8, A9, A17, AFF_1:21; A32: now__::_thesis:_(_(_for_a,_b,_c_being_Element_of_AFP_holds_ (_not_LIN_a,b,c_or_not_a_<>_b_or_not_a_<>_c_or_not_b_<>_c_)_)_implies_q,b_//_q9,y_) A33: now__::_thesis:_(_q_=_p9_implies_not_q_=_q9_) assume that A34: q = p9 and A35: q = q9 ; ::_thesis: contradiction LIN q,a,x by A15, A35, AFF_1:def_1; then LIN a,x,q by AFF_1:6; then a = x by A7, A9, A17, A29, AFF_1:25; then a,q // a,p by A13, A34, AFF_1:4; then LIN a,q,p by AFF_1:def_1; then LIN p,q,a by AFF_1:6; hence contradiction by A2, A3, A12, A16, A26, AFF_1:25; ::_thesis: verum end; A36: now__::_thesis:_(_p_=_p9_implies_not_p_=_q9_) assume that A37: p = p9 and A38: p = q9 ; ::_thesis: contradiction LIN p,a,x by A13, A37, AFF_1:def_1; then LIN a,x,p by AFF_1:6; then a = x by A7, A9, A17, A30, AFF_1:25; then a,q // a,q9 by A15, AFF_1:4; then LIN a,q,q9 by AFF_1:def_1; then LIN p,q,a by A38, AFF_1:6; hence contradiction by A2, A3, A12, A16, A26, AFF_1:25; ::_thesis: verum end; assume A39: for a, b, c being Element of AFP holds ( not LIN a,b,c or not a <> b or not a <> c or not b <> c ) ; ::_thesis: q,b // q9,y A40: now__::_thesis:_(_q_=_p9_&_p_=_q9_implies_q,b_//_q9,y_) assume that A41: q = p9 and A42: p = q9 ; ::_thesis: q,b // q9,y A43: now__::_thesis:_(_b_=_x_implies_q,b_//_q9,y_) assume A44: b = x ; ::_thesis: q,b // q9,y then q,y // q,a by A14, A15, A27, A41, A42, AFF_1:5; then LIN q,y,a by AFF_1:def_1; then LIN a,y,q by AFF_1:6; then q9,y // q,b by A7, A10, A13, A17, A29, A41, A42, A44, AFF_1:25; hence q,b // q9,y by AFF_1:4; ::_thesis: verum end; now__::_thesis:_not_a_=_x assume a = x ; ::_thesis: contradiction then a,p // a,q by A13, A41, AFF_1:4; then LIN a,p,q by AFF_1:def_1; then LIN p,q,a by AFF_1:6; hence contradiction by A2, A3, A12, A16, A26, AFF_1:25; ::_thesis: verum end; hence q,b // q9,y by A11, A31, A39, A43; ::_thesis: verum end; now__::_thesis:_(_p_=_p9_&_q_=_q9_implies_q,b_//_q9,y_) assume that A45: p = p9 and A46: q = q9 ; ::_thesis: q,b // q9,y LIN p,b,y by A14, A45, AFF_1:def_1; then LIN b,y,p by AFF_1:6; then b = y by A8, A10, A17, A30, AFF_1:25; hence q,b // q9,y by A46, AFF_1:2; ::_thesis: verum end; hence q,b // q9,y by A12, A23, A22, A39, A36, A33, A40; ::_thesis: verum end; A47: y in Line (p9,y) by AFF_1:15; A48: p9 in Line (p9,y) by AFF_1:15; A49: b in Line (p,b) by AFF_1:15; then A50: Line (p,b) <> K by A1, A8, A24, AFF_1:45; a <> q by A1, A3, A7, A24, AFF_1:45; then A51: Line (q,a) // Line (q9,x) by A15, A25, AFF_1:37; A52: p in Line (p,b) by AFF_1:15; then A53: Line (p,b) <> M by A1, A2, A24, AFF_1:45; A54: p9 <> y by A1, A4, A10, A24, AFF_1:45; then A55: Line (p,b) // Line (p9,y) by A14, A27, AFF_1:37; A56: Line (p9,y) is being_line by A54, AFF_1:def_3; now__::_thesis:_(_ex_a,_b,_c_being_Element_of_AFP_st_ (_LIN_a,b,c_&_a_<>_b_&_a_<>_c_&_b_<>_c_)_implies_q,b_//_q9,y_) A57: a,q // x,q9 by A18, A19, A21, A20, A51, AFF_1:39; assume ex a, b, c being Element of AFP st ( LIN a,b,c & a <> b & a <> c & b <> c ) ; ::_thesis: q,b // q9,y then consider d being Element of AFP such that A58: LIN p,b,d and A59: d <> p and A60: d <> b by TRANSLAC:1; consider N being Subset of AFP such that A61: d in N and A62: K // N by A16, AFF_1:49; A63: d in Line (p,b) by A58, AFF_1:def_2; then A64: N <> M by A8, A17, A28, A49, A53, A60, A61, AFF_1:18; A65: not Line (p9,y) // N proof assume Line (p9,y) // N ; ::_thesis: contradiction then Line (p,b) // N by A55, AFF_1:44; then Line (p,b) // K by A62, AFF_1:44; hence contradiction by A2, A52, A50, AFF_1:45; ::_thesis: verum end; N is being_line by A62, AFF_1:36; then consider z being Element of AFP such that A66: z in Line (p9,y) and A67: z in N by A56, A65, AFF_1:58; A68: d,b // z,y by A49, A47, A55, A63, A66, AFF_1:39; A69: N <> K by A2, A16, A28, A52, A50, A59, A63, A61, AFF_1:18; A70: M // N by A1, A62, AFF_1:44; A71: K <> N by A2, A16, A28, A52, A50, A59, A63, A61, AFF_1:18; A72: N // M by A1, A62, AFF_1:44; p,d // p9,z by A52, A48, A55, A63, A66, AFF_1:39; then A73: a,d // x,z by A1, A2, A4, A6, A7, A9, A13, A24, A61, A62, A67, A71, Lm4; M <> N by A8, A17, A28, A49, A53, A60, A63, A61, AFF_1:18; then d,q // z,q9 by A1, A3, A5, A6, A7, A9, A24, A61, A67, A73, A57, A70, Lm4; hence q,b // q9,y by A3, A5, A6, A8, A10, A61, A62, A67, A68, A72, A64, A69, Lm4; ::_thesis: verum end; hence q,b // q9,y by A32; ::_thesis: verum end; hence q,b // q9,y by A1, A3, A5, A8, A10, AFF_1:39; ::_thesis: verum end; Lm21: for AFP being AffinPlane for a, b, x, p, p9, y, q, q9 being Element of AFP for K being Subset of AFP st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x holds q,b // q9,y proof let AFP be AffinPlane; ::_thesis: for a, b, x, p, p9, y, q, q9 being Element of AFP for K being Subset of AFP st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x holds q,b // q9,y let a, b, x, p, p9, y, q, q9 be Element of AFP; ::_thesis: for K being Subset of AFP st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x holds q,b // q9,y let K be Subset of AFP; ::_thesis: ( a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x implies q,b // q9,y ) assume that A1: a,b // K and A2: not a in K and A3: not x in K and A4: AFP is Moufangian and A5: p in K and A6: p9 in K and A7: p,a // p9,x and A8: p,b // p9,y and A9: x,y // K and A10: q in K and A11: q9 in K and A12: q,a // q9,x ; ::_thesis: q,b // q9,y A13: K is being_line by A1, AFF_1:26; A14: now__::_thesis:_(_not_a,x_//_K_&_a_<>_b_implies_q,b_//_q9,y_) A15: a,q // x,q9 by A12, AFF_1:4; A16: b,p // y,p9 by A8, AFF_1:4; A17: a,p // x,p9 by A7, AFF_1:4; set A = Line (a,x); assume that A18: not a,x // K and A19: a <> b ; ::_thesis: q,b // q9,y a <> x by A13, A18, AFF_1:33; then A20: Line (a,x) is being_line by AFF_1:def_3; A21: x in Line (a,x) by AFF_1:15; A22: a in Line (a,x) by AFF_1:15; then consider o being Element of AFP such that A23: o in Line (a,x) and A24: o in K by A13, A18, A21, A20, AFF_1:40, AFF_1:58; A25: LIN o,a,x by A22, A21, A20, A23, AFF_1:21; K is being_line by A1, AFF_1:26; then a,b // x,y by A1, A9, AFF_1:31; then LIN o,b,y by A1, A2, A4, A5, A6, A19, A24, A25, A17, A16, Lm3, AFF_1:26; then b,q // y,q9 by A1, A2, A4, A9, A10, A11, A13, A24, A25, A15, Lm2; hence q,b // q9,y by AFF_1:4; ::_thesis: verum end; A26: now__::_thesis:_(_a,x_//_K_&_a_<>_b_&_p_<>_q_implies_q,b_//_q9,y_) set M = Line (a,b); assume that A27: a,x // K and A28: a <> b and A29: p <> q ; ::_thesis: q,b // q9,y A30: Line (a,b) is being_line by A28, AFF_1:def_3; K is being_line by A1, AFF_1:26; then a,b // a,x by A1, A27, AFF_1:31; then LIN a,b,x by AFF_1:def_1; then A31: x in Line (a,b) by AFF_1:def_2; A32: b in Line (a,b) by AFF_1:15; A33: a in Line (a,b) by AFF_1:15; A34: Line (a,b) // K by A1, A28, AFF_1:def_5; then x,y // Line (a,b) by A9, AFF_1:43; then y in Line (a,b) by A30, A31, AFF_1:23; hence q,b // q9,y by A4, A5, A6, A7, A8, A10, A11, A12, A28, A29, A33, A32, A34, A31, Th7; ::_thesis: verum end; A35: ( a = b implies x = y ) proof set M = Line (x,y); A36: x in Line (x,y) by AFF_1:15; assume a = b ; ::_thesis: x = y then p9,x // p9,y by A2, A5, A7, A8, AFF_1:5; then LIN p9,x,y by AFF_1:def_1; then LIN x,y,p9 by AFF_1:6; then A37: p9 in Line (x,y) by AFF_1:def_2; assume x <> y ; ::_thesis: contradiction then Line (x,y) // K by A9, AFF_1:def_5; hence contradiction by A3, A6, A36, A37, AFF_1:45; ::_thesis: verum end; now__::_thesis:_(_p_=_q_implies_q,b_//_q9,y_) assume A38: p = q ; ::_thesis: q,b // q9,y p9 = q9 proof p9,x // q9,x by A2, A5, A7, A12, A38, AFF_1:5; then x,p9 // x,q9 by AFF_1:4; then LIN x,p9,q9 by AFF_1:def_1; then A39: LIN p9,q9,x by AFF_1:6; assume p9 <> q9 ; ::_thesis: contradiction hence contradiction by A1, A3, A6, A11, A39, AFF_1:25, AFF_1:26; ::_thesis: verum end; hence q,b // q9,y by A8, A38; ::_thesis: verum end; hence q,b // q9,y by A12, A35, A14, A26; ::_thesis: verum end; Lm22: for AFP being AffinPlane for a, b, x, p, p9, y, q, q9, s being Element of AFP for K being Subset of AFP st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x & x,s // K & q,b // q9,s holds s = y proof let AFP be AffinPlane; ::_thesis: for a, b, x, p, p9, y, q, q9, s being Element of AFP for K being Subset of AFP st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x & x,s // K & q,b // q9,s holds s = y let a, b, x, p, p9, y, q, q9, s be Element of AFP; ::_thesis: for K being Subset of AFP st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x & x,s // K & q,b // q9,s holds s = y let K be Subset of AFP; ::_thesis: ( a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K & q in K & q9 in K & q,a // q9,x & x,s // K & q,b // q9,s implies s = y ) assume that A1: a,b // K and A2: not a in K and A3: not x in K and A4: AFP is Moufangian and A5: p in K and A6: p9 in K and A7: p,a // p9,x and A8: p,b // p9,y and A9: x,y // K and A10: q in K and A11: q9 in K and A12: q,a // q9,x and A13: x,s // K and A14: q,b // q9,s ; ::_thesis: s = y A15: not b in K by A1, A2, AFF_1:35; q,b // q9,y by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, Lm21; then q9,s // q9,y by A10, A14, A15, AFF_1:5; then LIN q9,s,y by AFF_1:def_1; then A16: LIN y,s,q9 by AFF_1:6; assume A17: not s = y ; ::_thesis: contradiction K is being_line by A1, AFF_1:26; then consider M being Subset of AFP such that A18: x in M and A19: K // M by AFF_1:49; A20: M is being_line by A19, AFF_1:36; x,s // M by A13, A19, AFF_1:43; then A21: s in M by A18, A20, AFF_1:23; x,y // M by A9, A19, AFF_1:43; then y in M by A18, A20, AFF_1:23; then M = Line (y,s) by A17, A20, A21, AFF_1:24; then q9 in M by A16, AFF_1:def_2; hence contradiction by A3, A11, A18, A19, AFF_1:45; ::_thesis: verum end; Lm23: for AFP being AffinPlane for a, b, x, y, r being Element of AFP for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian & ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) & ( ( r in K & r = y ) or ( not r in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,r & p,b // p9,y & r,y // K ) ) ) holds x = r proof let AFP be AffinPlane; ::_thesis: for a, b, x, y, r being Element of AFP for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian & ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) & ( ( r in K & r = y ) or ( not r in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,r & p,b // p9,y & r,y // K ) ) ) holds x = r let a, b, x, y, r be Element of AFP; ::_thesis: for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian & ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) & ( ( r in K & r = y ) or ( not r in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,r & p,b // p9,y & r,y // K ) ) ) holds x = r let K be Subset of AFP; ::_thesis: ( a,b // K & not a in K & AFP is Moufangian & ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) & ( ( r in K & r = y ) or ( not r in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,r & p,b // p9,y & r,y // K ) ) ) implies x = r ) assume that A1: a,b // K and A2: not a in K and A3: AFP is Moufangian and A4: ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) and A5: ( ( r in K & r = y ) or ( not r in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,r & p,b // p9,y & r,y // K ) ) ) ; ::_thesis: x = r A6: ( ( y in K & y = r ) or ( not y in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,b // p9,y & p,a // p9,r & y,r // K ) ) ) by A1, A2, A5, Lm18; A7: b,a // K by A1, AFF_1:34; A8: not b in K by A1, A2, AFF_1:35; ( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,b // p9,y & p,a // p9,x & y,x // K ) ) ) by A1, A2, A4, Lm18; hence x = r by A3, A7, A8, A6, Lm22; ::_thesis: verum end; Lm24: for AFP being AffinPlane for a, b being Element of AFP for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian holds ex f being Permutation of the carrier of AFP st for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) proof let AFP be AffinPlane; ::_thesis: for a, b being Element of AFP for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian holds ex f being Permutation of the carrier of AFP st for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) let a, b be Element of AFP; ::_thesis: for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian holds ex f being Permutation of the carrier of AFP st for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) let K be Subset of AFP; ::_thesis: ( a,b // K & not a in K & AFP is Moufangian implies ex f being Permutation of the carrier of AFP st for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) defpred S1[ Element of AFP, Element of AFP] means ( ( $1 in K & $1 = $2 ) or ( not $1 in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,$1 & p,b // p9,$2 & $1,$2 // K ) ) ); assume that A1: a,b // K and A2: not a in K and A3: AFP is Moufangian ; ::_thesis: ex f being Permutation of the carrier of AFP st for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) A4: for x, y, s being Element of AFP st S1[x,y] & S1[x,s] holds y = s by A1, A2, A3, Lm22; A5: for y being Element of AFP ex x being Element of AFP st S1[x,y] by A1, A2, Lm20; A6: for x being Element of AFP ex y being Element of AFP st S1[x,y] by A1, A2, Lm19; A7: for x, y, r being Element of AFP st S1[x,y] & S1[r,y] holds x = r by A1, A2, A3, Lm23; ex f being Permutation of the carrier of AFP st for x, y being Element of AFP holds ( f . x = y iff S1[x,y] ) from TRANSGEO:sch_1(A6, A5, A7, A4); hence ex f being Permutation of the carrier of AFP st for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ; ::_thesis: verum end; Lm25: for AFP being AffinPlane for a, b being Element of AFP for K being Subset of AFP for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds f . a = b proof let AFP be AffinPlane; ::_thesis: for a, b being Element of AFP for K being Subset of AFP for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds f . a = b let a, b be Element of AFP; ::_thesis: for K being Subset of AFP for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds f . a = b let K be Subset of AFP; ::_thesis: for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds f . a = b let f be Permutation of the carrier of AFP; ::_thesis: ( a,b // K & not a in K & ( for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) implies f . a = b ) assume that A1: a,b // K and A2: not a in K ; ::_thesis: ( ex x, y being Element of AFP st ( ( not f . x = y or ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) implies ( ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) & not f . x = y ) ) or f . a = b ) consider p, q being Element of AFP such that A3: p in K and q in K and p <> q by A1, AFF_1:19, AFF_1:26; A4: p,b // p,b by AFF_1:2; assume A5: for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ; ::_thesis: f . a = b p,a // p,a by AFF_1:2; hence f . a = b by A1, A2, A5, A3, A4; ::_thesis: verum end; Lm26: for AFP being AffinPlane for a, b being Element of AFP for K being Subset of AFP for f being Permutation of the carrier of AFP st a,b // K & ( for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds for x being Element of AFP holds x,f . x // K proof let AFP be AffinPlane; ::_thesis: for a, b being Element of AFP for K being Subset of AFP for f being Permutation of the carrier of AFP st a,b // K & ( for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds for x being Element of AFP holds x,f . x // K let a, b be Element of AFP; ::_thesis: for K being Subset of AFP for f being Permutation of the carrier of AFP st a,b // K & ( for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds for x being Element of AFP holds x,f . x // K let K be Subset of AFP; ::_thesis: for f being Permutation of the carrier of AFP st a,b // K & ( for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds for x being Element of AFP holds x,f . x // K let f be Permutation of the carrier of AFP; ::_thesis: ( a,b // K & ( for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) implies for x being Element of AFP holds x,f . x // K ) assume that A1: a,b // K and A2: for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ; ::_thesis: for x being Element of AFP holds x,f . x // K let x be Element of AFP; ::_thesis: x,f . x // K set y = f . x; A3: K is being_line by A1, AFF_1:26; A4: now__::_thesis:_(_x_in_K_implies_x,f_._x_//_K_) assume x in K ; ::_thesis: x,f . x // K then f . x = x by A2; hence x,f . x // K by A3, AFF_1:33; ::_thesis: verum end; now__::_thesis:_(_not_x_in_K_implies_x,f_._x_//_K_) assume not x in K ; ::_thesis: x,f . x // K then ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,f . x & x,f . x // K ) by A2; hence x,f . x // K ; ::_thesis: verum end; hence x,f . x // K by A4; ::_thesis: verum end; Lm27: for AFP being AffinPlane for a, b being Element of AFP for K being Subset of AFP for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds f is collineation proof let AFP be AffinPlane; ::_thesis: for a, b being Element of AFP for K being Subset of AFP for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds f is collineation let a, b be Element of AFP; ::_thesis: for K being Subset of AFP for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds f is collineation let K be Subset of AFP; ::_thesis: for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds f is collineation let f be Permutation of the carrier of AFP; ::_thesis: ( a,b // K & not a in K & ( for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) implies f is collineation ) assume that A1: a,b // K and A2: not a in K and A3: for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ; ::_thesis: f is collineation A4: K is being_line by A1, AFF_1:26; A5: not b in K by A1, A2, AFF_1:35; for A being Subset of AFP st A is being_line holds f .: A is being_line proof let A be Subset of AFP; ::_thesis: ( A is being_line implies f .: A is being_line ) assume A6: A is being_line ; ::_thesis: f .: A is being_line set B9 = f .: A; A7: now__::_thesis:_(_A_//_K_&_A_<>_K_implies_f_.:_A_is_being_line_) assume that A8: A // K and A9: A <> K ; ::_thesis: f .: A is being_line now__::_thesis:_for_x_being_Element_of_AFP_st_x_in_A_holds_ x_in_f_.:_A let x be Element of AFP; ::_thesis: ( x in A implies x in f .: A ) assume A10: x in A ; ::_thesis: x in f .: A consider y being Element of AFP such that A11: f . y = x by TRANSGEO:1; ( ( y in K & y = x ) or ( not y in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,y & p,b // p9,x & y,x // K ) ) ) by A3, A11; then x,y // K by A8, A9, A10, AFF_1:34, AFF_1:45; then x,y // A by A8, AFF_1:43; then y in A by A6, A10, AFF_1:23; hence x in f .: A by A11, TRANSGEO:87; ::_thesis: verum end; then A12: A c= f .: A by SUBSET_1:2; now__::_thesis:_for_y_being_Element_of_AFP_st_y_in_f_.:_A_holds_ y_in_A let y be Element of AFP; ::_thesis: ( y in f .: A implies y in A ) assume y in f .: A ; ::_thesis: y in A then consider x being Element of AFP such that A13: x in A and A14: y = f . x by TRANSGEO:87; not x in K by A8, A9, A13, AFF_1:45; then ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) by A3, A14; then x,y // A by A8, AFF_1:43; hence y in A by A6, A13, AFF_1:23; ::_thesis: verum end; then f .: A c= A by SUBSET_1:2; hence f .: A is being_line by A6, A12, XBOOLE_0:def_10; ::_thesis: verum end; A15: now__::_thesis:_(_not_A_//_K_&_A_<>_K_implies_f_.:_A_is_being_line_) K is being_line by A1, AFF_1:26; then consider M being Subset of AFP such that A16: a in M and A17: K // M by AFF_1:49; A18: M is being_line by A17, AFF_1:36; consider A9 being Subset of AFP such that A19: a in A9 and A20: A // A9 by A6, AFF_1:49; A21: A9 is being_line by A20, AFF_1:36; assume that A22: not A // K and A23: A <> K ; ::_thesis: f .: A is being_line consider p being Element of AFP such that A24: p in A and A25: p in K by A4, A6, A22, AFF_1:58; not A9 // K by A22, A20, AFF_1:44; then consider q being Element of AFP such that A26: q in A9 and A27: q in K by A4, A21, AFF_1:58; set C9 = Line (q,b); A28: q in Line (q,b) by AFF_1:15; a,b // M by A1, A17, AFF_1:43; then b in M by A16, A18, AFF_1:23; then q <> b by A2, A16, A17, A27, AFF_1:45; then Line (q,b) is being_line by AFF_1:def_3; then consider C being Subset of AFP such that A29: p in C and A30: Line (q,b) // C by AFF_1:49; A31: b in Line (q,b) by AFF_1:15; A32: C is being_line by A30, AFF_1:36; now__::_thesis:_for_y_being_Element_of_AFP_st_y_in_C_holds_ y_in_f_.:_A let y be Element of AFP; ::_thesis: ( y in C implies y in f .: A ) assume A33: y in C ; ::_thesis: y in f .: A A34: now__::_thesis:_(_y_<>_p_implies_y_in_f_.:_A_) A35: q,b // p,y by A28, A31, A29, A30, A33, AFF_1:39; K is being_line by A1, AFF_1:26; then consider N being Subset of AFP such that A36: y in N and A37: K // N by AFF_1:49; A38: N is being_line by A37, AFF_1:36; not N // A by A22, A37, AFF_1:44; then consider x being Element of AFP such that A39: x in N and A40: x in A by A6, A38, AFF_1:58; A41: x,y // K by A36, A37, A39, AFF_1:40; assume A42: y <> p ; ::_thesis: y in f .: A A43: not x in K proof assume x in K ; ::_thesis: contradiction then y in K by A36, A37, A39, AFF_1:45; then Line (q,b) // K by A4, A25, A29, A30, A32, A33, A42, AFF_1:18; hence contradiction by A5, A27, A28, A31, AFF_1:45; ::_thesis: verum end; q,a // p,x by A24, A19, A20, A26, A40, AFF_1:39; then y = f . x by A3, A25, A27, A43, A35, A41; hence y in f .: A by A40, TRANSGEO:87; ::_thesis: verum end; now__::_thesis:_(_y_=_p_implies_y_in_f_.:_A_) assume A44: y = p ; ::_thesis: y in f .: A f . p = p by A3, A25; hence y in f .: A by A24, A44, TRANSGEO:87; ::_thesis: verum end; hence y in f .: A by A34; ::_thesis: verum end; then A45: C c= f .: A by SUBSET_1:2; now__::_thesis:_for_y_being_Element_of_AFP_st_y_in_f_.:_A_holds_ y_in_C let y be Element of AFP; ::_thesis: ( y in f .: A implies y in C ) assume y in f .: A ; ::_thesis: y in C then consider x being Element of AFP such that A46: x in A and A47: y = f . x by TRANSGEO:87; now__::_thesis:_(_x_<>_p_implies_y_in_C_) K is being_line by A1, AFF_1:26; then consider N being Subset of AFP such that A48: x in N and A49: K // N by AFF_1:49; A50: not C // N proof assume C // N ; ::_thesis: contradiction then Line (q,b) // N by A30, AFF_1:44; then A51: Line (q,b) // K by A49, AFF_1:44; q in Line (q,b) by AFF_1:15; then Line (q,b) = K by A27, A51, AFF_1:45; hence contradiction by A5, AFF_1:15; ::_thesis: verum end; N is being_line by A49, AFF_1:36; then consider z being Element of AFP such that A52: z in C and A53: z in N by A32, A50, AFF_1:58; A54: x,z // K by A48, A49, A53, AFF_1:40; assume x <> p ; ::_thesis: y in C then A55: not x in K by A4, A6, A23, A24, A25, A46, AFF_1:18; A56: q,a // p,x by A24, A19, A20, A26, A46, AFF_1:39; q,b // p,z by A28, A31, A29, A30, A52, AFF_1:39; hence y in C by A3, A25, A27, A47, A55, A52, A56, A54; ::_thesis: verum end; hence y in C by A3, A25, A29, A47; ::_thesis: verum end; then f .: A c= C by SUBSET_1:2; hence f .: A is being_line by A32, A45, XBOOLE_0:def_10; ::_thesis: verum end; now__::_thesis:_(_A_=_K_implies_f_.:_A_is_being_line_) assume A57: A = K ; ::_thesis: f .: A is being_line now__::_thesis:_for_y_being_Element_of_AFP_st_y_in_f_.:_A_holds_ y_in_A let y be Element of AFP; ::_thesis: ( y in f .: A implies y in A ) assume y in f .: A ; ::_thesis: y in A then ex x being Element of AFP st ( x in A & y = f . x ) by TRANSGEO:87; hence y in A by A3, A57; ::_thesis: verum end; then A58: f .: A c= A by SUBSET_1:2; now__::_thesis:_for_x_being_Element_of_AFP_st_x_in_A_holds_ x_in_f_.:_A let x be Element of AFP; ::_thesis: ( x in A implies x in f .: A ) assume A59: x in A ; ::_thesis: x in f .: A set y = f . x; f . x in f .: A by A59, TRANSGEO:86; hence x in f .: A by A3, A57, A59; ::_thesis: verum end; then A c= f .: A by SUBSET_1:2; hence f .: A is being_line by A6, A58, XBOOLE_0:def_10; ::_thesis: verum end; hence f .: A is being_line by A7, A15; ::_thesis: verum end; hence f is collineation by TRANSGEO:92; ::_thesis: verum end; Lm28: for AFP being AffinPlane for a, b being Element of AFP for K being Subset of AFP for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds f is_Sc K proof let AFP be AffinPlane; ::_thesis: for a, b being Element of AFP for K being Subset of AFP for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds f is_Sc K let a, b be Element of AFP; ::_thesis: for K being Subset of AFP for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds f is_Sc K let K be Subset of AFP; ::_thesis: for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds f is_Sc K let f be Permutation of the carrier of AFP; ::_thesis: ( a,b // K & not a in K & ( for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) implies f is_Sc K ) assume that A1: a,b // K and A2: not a in K and A3: for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ; ::_thesis: f is_Sc K A4: for x being Element of AFP holds x,f . x // K by A1, A3, Lm26; A5: for x being Element of AFP st x in K holds f . x = x by A3; A6: K is being_line by A1, AFF_1:26; f is collineation by A1, A2, A3, Lm27; hence f is_Sc K by A6, A5, A4, Def1; ::_thesis: verum end; theorem Th8: :: HOMOTHET:8 for AFP being AffinPlane for a, b being Element of AFP for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian holds ex f being Permutation of the carrier of AFP st ( f is_Sc K & f . a = b ) proof let AFP be AffinPlane; ::_thesis: for a, b being Element of AFP for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian holds ex f being Permutation of the carrier of AFP st ( f is_Sc K & f . a = b ) let a, b be Element of AFP; ::_thesis: for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian holds ex f being Permutation of the carrier of AFP st ( f is_Sc K & f . a = b ) let K be Subset of AFP; ::_thesis: ( a,b // K & not a in K & AFP is Moufangian implies ex f being Permutation of the carrier of AFP st ( f is_Sc K & f . a = b ) ) assume that A1: a,b // K and A2: not a in K and A3: AFP is Moufangian ; ::_thesis: ex f being Permutation of the carrier of AFP st ( f is_Sc K & f . a = b ) consider f being Permutation of the carrier of AFP such that A4: for x, y being Element of AFP holds ( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st ( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) by A1, A2, A3, Lm24; A5: f . a = b by A1, A2, A4, Lm25; f is_Sc K by A1, A2, A4, Lm28; hence ex f being Permutation of the carrier of AFP st ( f is_Sc K & f . a = b ) by A5; ::_thesis: verum end; theorem :: HOMOTHET:9 for AFP being AffinPlane holds ( AFP is Moufangian iff for a, b being Element of AFP for K being Subset of AFP st a,b // K & not a in K holds ex f being Permutation of the carrier of AFP st ( f is_Sc K & f . a = b ) ) by Th6, Th8;