let AP be AffinPlane; :: thesis: ( AP is Moufangian implies AP is satisfying_TDES_1 )

assume A1: AP is Moufangian ; :: thesis: AP is satisfying_TDES_1

let K be Subset of AP; :: according to AFF_2:def 8 :: thesis: for o, a, b, c, a9, b9, c9 being Element of AP 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 & 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 AP; :: 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 & 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: o <> c and

A8: a <> b and

A9: LIN o,a,a9 and

A10: a,b // a9,b9 and

A11: b,c // b9,c9 and

A12: a,c // a9,c9 and

A13: a,b // K ; :: thesis: LIN o,b,b9

consider P being Subset of AP such that

A14: a9 in P and

A15: K // P by A2, AFF_1:49;

A16: P is being_line by A15, AFF_1:36;

set A = Line (o,b);

set C = Line (o,a);

A17: ( o in Line (o,b) & 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, A13, AFF_1:35;

not Line (o,b) // P

A21: x in Line (o,b) and

A22: x in P by A19, A16, AFF_1:58;

A23: ( o in Line (o,a) & a in Line (o,a) ) by AFF_1:15;

A24: LIN o,b,x by A19, A17, A21, AFF_1:21;

a,b // P by A13, A15, AFF_1:43;

then a9,b9 // P by A8, A10, AFF_1:32;

then A25: b9 in P by A14, A16, AFF_1:23;

then A26: LIN b9,x,b9 by A16, A22, AFF_1:21;

A27: Line (o,a) is being_line by A3, A6, AFF_1:def 3;

then A28: a9 in Line (o,a) by A3, A6, A9, A23, AFF_1:25;

A29: b9 <> c9

a9,x // K by A14, A15, A22, AFF_1:40;

then a,b // a9,x by A2, A13, AFF_1:31;

then b,c // x,c9 by A1, A2, A3, A4, A5, A6, A7, A8, A9, A12, A13, A24;

then b9,c9 // x,c9 by A11, A32, AFF_1:5;

then c9,b9 // c9,x by AFF_1:4;

then LIN c9,b9,x by AFF_1:def 1;

then A33: LIN b9,x,c9 by AFF_1:6;

A34: a9 <> b9

then LIN b9,c9,a9 by A18, A24, A33, A26, 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 A11, A29, AFF_1:5;

then a,b // b,c by A10, A34, AFF_1:5;

then b,c // K by A8, A13, AFF_1:32;

then c,b // K by AFF_1:34;

hence contradiction by A2, A4, A20, AFF_1:23; :: thesis: verum

assume A1: AP is Moufangian ; :: thesis: AP is satisfying_TDES_1

let K be Subset of AP; :: according to AFF_2:def 8 :: thesis: for o, a, b, c, a9, b9, c9 being Element of AP 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 & 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 AP; :: 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 & 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: o <> c and

A8: a <> b and

A9: LIN o,a,a9 and

A10: a,b // a9,b9 and

A11: b,c // b9,c9 and

A12: a,c // a9,c9 and

A13: a,b // K ; :: thesis: LIN o,b,b9

consider P being Subset of AP such that

A14: a9 in P and

A15: K // P by A2, AFF_1:49;

A16: P is being_line by A15, AFF_1:36;

set A = Line (o,b);

set C = Line (o,a);

A17: ( o in Line (o,b) & 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, A13, AFF_1:35;

not Line (o,b) // P

proof

then consider x being Element of AP such that
assume
Line (o,b) // P
; :: thesis: contradiction

then Line (o,b) // K by A15, AFF_1:44;

hence contradiction by A3, A20, A17, AFF_1:45; :: thesis: verum

end;then Line (o,b) // K by A15, AFF_1:44;

hence contradiction by A3, A20, A17, AFF_1:45; :: thesis: verum

A21: x in Line (o,b) and

A22: x in P by A19, A16, AFF_1:58;

A23: ( o in Line (o,a) & a in Line (o,a) ) by AFF_1:15;

A24: LIN o,b,x by A19, A17, A21, AFF_1:21;

a,b // P by A13, A15, AFF_1:43;

then a9,b9 // P by A8, A10, AFF_1:32;

then A25: b9 in P by A14, A16, AFF_1:23;

then A26: LIN b9,x,b9 by A16, A22, AFF_1:21;

A27: Line (o,a) is being_line by A3, A6, AFF_1:def 3;

then A28: a9 in Line (o,a) by A3, A6, A9, A23, AFF_1:25;

A29: b9 <> c9

proof

A32:
b <> c
by A4, A6, A13, AFF_1:35;
A30:
a9,c9 // c,a
by A12, AFF_1:4;

assume A31: b9 = c9 ; :: thesis: contradiction

then P = K by A5, A15, A25, AFF_1:45;

then a9 = o by A2, A3, A6, A27, A23, A28, A14, AFF_1:18;

then b9 = o by A2, A3, A4, A5, A6, A31, A30, AFF_1:48;

hence contradiction by A18, AFF_1:7; :: thesis: verum

end;assume A31: b9 = c9 ; :: thesis: contradiction

then P = K by A5, A15, A25, AFF_1:45;

then a9 = o by A2, A3, A6, A27, A23, A28, A14, AFF_1:18;

then b9 = o by A2, A3, A4, A5, A6, A31, A30, AFF_1:48;

hence contradiction by A18, AFF_1:7; :: thesis: verum

a9,x // K by A14, A15, A22, AFF_1:40;

then a,b // a9,x by A2, A13, AFF_1:31;

then b,c // x,c9 by A1, A2, A3, A4, A5, A6, A7, A8, A9, A12, A13, A24;

then b9,c9 // x,c9 by A11, A32, AFF_1:5;

then c9,b9 // c9,x by AFF_1:4;

then LIN c9,b9,x by AFF_1:def 1;

then A33: LIN b9,x,c9 by AFF_1:6;

A34: a9 <> b9

proof

LIN b9,x,a9
by A14, A16, A22, A25, AFF_1:21;
assume A35:
a9 = b9
; :: thesis: contradiction

then c,a // c,b by A36, 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 A8, A13, AFF_1:32;

then c,a // K by AFF_1:34;

hence contradiction by A2, A4, A6, AFF_1:23; :: thesis: verum

end;A36: now :: thesis: not a9 = c9

( a,c // b,c or a9 = c9 )
by A11, A12, A35, AFF_1:5;assume
a9 = c9
; :: thesis: contradiction

then b9 = o by A2, A3, A5, A6, A27, A23, A28, A35, AFF_1:18;

hence contradiction by A18, AFF_1:7; :: thesis: verum

end;then b9 = o by A2, A3, A5, A6, A27, A23, A28, A35, AFF_1:18;

hence contradiction by A18, AFF_1:7; :: thesis: verum

then c,a // c,b by A36, 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 A8, A13, AFF_1:32;

then c,a // K by AFF_1:34;

hence contradiction by A2, A4, A6, AFF_1:23; :: thesis: verum

then LIN b9,c9,a9 by A18, A24, A33, A26, 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 A11, A29, AFF_1:5;

then a,b // b,c by A10, A34, AFF_1:5;

then b,c // K by A8, A13, AFF_1:32;

then c,b // K by AFF_1:34;

hence contradiction by A2, A4, A20, AFF_1:23; :: thesis: verum