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

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

let K be Subset of AP; :: according to AFF_2:def 7 :: 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 & 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 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 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K implies b,c // b9,c9 )

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: LIN o,b,b9 and

A11: a,b // a9,b9 and

A12: a,c // a9,c9 and

A13: a,b // K ; :: thesis: b,c // b9,c9

set A = Line (o,a);

set P = Line (o,b);

set M = Line (b,c);

set T = Line (a9,c9);

A14: o in Line (o,a) by A3, A6, AFF_1:24;

assume A15: not b,c // b9,c9 ; :: thesis: contradiction

then A16: b <> c by AFF_1:3;

then A17: b in Line (b,c) by AFF_1:24;

A18: a9,b9 // b,a by A11, AFF_1:4;

A19: c in Line (b,c) by A16, AFF_1:24;

A20: a in Line (o,a) by A3, A6, AFF_1:24;

A21: Line (o,a) is being_line by A3, A6, AFF_1:24;

then A22: a9 in Line (o,a) by A3, A6, A9, A14, A20, AFF_1:25;

A23: o <> b by A3, A6, A13, AFF_1:35;

then A24: Line (o,b) is being_line by AFF_1:24;

A25: b in Line (o,b) by A23, AFF_1:24;

A26: Line (o,a) <> Line (o,b)

then A28: b9 in Line (o,b) by A10, A23, A24, A25, AFF_1:25;

A29: a9 <> b9

A35: Line (b,c) is being_line by A16, AFF_1:24;

then consider N being Subset of AP such that

A36: b9 in N and

A37: Line (b,c) // N by AFF_1:49;

A38: N is being_line by A37, AFF_1:36;

A39: not LIN a,b,c

A41: x in N and

A42: LIN a9,c9,x by A38, AFF_1:59;

A43: b,c // b9,x by A17, A19, A36, A37, A41, AFF_1:39;

a9,c9 // a9,x by A42, AFF_1:def 1;

then a,c // a9,x by A12, A32, AFF_1:5;

then A44: x in K by A1, A2, A3, A4, A6, A7, A8, A9, A10, A11, A13, A43;

A45: a9 in Line (a9,c9) by A32, AFF_1:24;

then x in Line (a9,c9) by A32, A34, A42, AFF_1:25;

then K = Line (a9,c9) by A2, A5, A15, A34, A43, A44, AFF_1:18;

then a9 in Line (o,b) by A2, A3, A6, A21, A14, A20, A27, A22, A45, AFF_1:18;

then a in Line (o,b) by A24, A25, A28, A29, A18, AFF_1:48;

hence contradiction by A3, A6, A24, A27, A26, AFF_1:24; :: thesis: verum

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

let K be Subset of AP; :: according to AFF_2:def 7 :: 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 & 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 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 & LIN o,b,b9 & a,b // a9,b9 & a,c // a9,c9 & a,b // K implies b,c // b9,c9 )

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: LIN o,b,b9 and

A11: a,b // a9,b9 and

A12: a,c // a9,c9 and

A13: a,b // K ; :: thesis: b,c // b9,c9

set A = Line (o,a);

set P = Line (o,b);

set M = Line (b,c);

set T = Line (a9,c9);

A14: o in Line (o,a) by A3, A6, AFF_1:24;

assume A15: not b,c // b9,c9 ; :: thesis: contradiction

then A16: b <> c by AFF_1:3;

then A17: b in Line (b,c) by AFF_1:24;

A18: a9,b9 // b,a by A11, AFF_1:4;

A19: c in Line (b,c) by A16, AFF_1:24;

A20: a in Line (o,a) by A3, A6, AFF_1:24;

A21: Line (o,a) is being_line by A3, A6, AFF_1:24;

then A22: a9 in Line (o,a) by A3, A6, A9, A14, A20, AFF_1:25;

A23: o <> b by A3, A6, A13, AFF_1:35;

then A24: Line (o,b) is being_line by AFF_1:24;

A25: b in Line (o,b) by A23, AFF_1:24;

A26: Line (o,a) <> Line (o,b)

proof

A27:
o in Line (o,b)
by A23, AFF_1:24;
assume
Line (o,a) = Line (o,b)
; :: thesis: contradiction

then a,b // Line (o,a) by A21, A20, A25, AFF_1:40, AFF_1:41;

hence contradiction by A3, A6, A8, A13, A14, A20, AFF_1:45, AFF_1:53; :: thesis: verum

end;then a,b // Line (o,a) by A21, A20, A25, AFF_1:40, AFF_1:41;

hence contradiction by A3, A6, A8, A13, A14, A20, AFF_1:45, AFF_1:53; :: thesis: verum

then A28: b9 in Line (o,b) by A10, A23, A24, A25, AFF_1:25;

A29: a9 <> b9

proof

A32:
a9 <> c9
A30:
a9,c9 // c,a
by A12, AFF_1:4;

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

then a9 in K by A3, A21, A24, A14, A27, A22, A28, A26, AFF_1:18;

then a9 = c9 by A2, A4, A5, A6, A30, AFF_1:48;

hence contradiction by A15, A31, AFF_1:3; :: thesis: verum

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

then a9 in K by A3, A21, A24, A14, A27, A22, A28, A26, AFF_1:18;

then a9 = c9 by A2, A4, A5, A6, A30, AFF_1:48;

hence contradiction by A15, A31, AFF_1:3; :: thesis: verum

proof

then A34:
( Line (a9,c9) is being_line & c9 in Line (a9,c9) )
by AFF_1:24;
assume
a9 = c9
; :: thesis: contradiction

then A33: a9 in Line (o,b) by A2, A3, A5, A6, A21, A14, A20, A27, A22, AFF_1:18;

a9,b9 // b,a by A11, AFF_1:4;

then a in Line (o,b) by A24, A25, A28, A29, A33, AFF_1:48;

hence contradiction by A3, A6, A24, A27, A26, AFF_1:24; :: thesis: verum

end;then A33: a9 in Line (o,b) by A2, A3, A5, A6, A21, A14, A20, A27, A22, AFF_1:18;

a9,b9 // b,a by A11, AFF_1:4;

then a in Line (o,b) by A24, A25, A28, A29, A33, AFF_1:48;

hence contradiction by A3, A6, A24, A27, A26, AFF_1:24; :: thesis: verum

A35: Line (b,c) is being_line by A16, AFF_1:24;

then consider N being Subset of AP such that

A36: b9 in N and

A37: Line (b,c) // N by AFF_1:49;

A38: N is being_line by A37, AFF_1:36;

A39: not LIN a,b,c

proof

not a9,c9 // N
assume
LIN a,b,c
; :: thesis: contradiction

then a,b // a,c by AFF_1:def 1;

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;then a,b // a,c by AFF_1:def 1;

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

proof

then consider x being Element of AP such that
assume A40:
a9,c9 // N
; :: thesis: contradiction

a9,c9 // a,c by A12, AFF_1:4;

then a,c // N by A32, A40, AFF_1:32;

then a,c // Line (b,c) by A37, AFF_1:43;

then c,a // Line (b,c) by AFF_1:34;

then a in Line (b,c) by A35, A19, AFF_1:23;

hence contradiction by A39, A35, A17, A19, AFF_1:21; :: thesis: verum

end;a9,c9 // a,c by A12, AFF_1:4;

then a,c // N by A32, A40, AFF_1:32;

then a,c // Line (b,c) by A37, AFF_1:43;

then c,a // Line (b,c) by AFF_1:34;

then a in Line (b,c) by A35, A19, AFF_1:23;

hence contradiction by A39, A35, A17, A19, AFF_1:21; :: thesis: verum

A41: x in N and

A42: LIN a9,c9,x by A38, AFF_1:59;

A43: b,c // b9,x by A17, A19, A36, A37, A41, AFF_1:39;

a9,c9 // a9,x by A42, AFF_1:def 1;

then a,c // a9,x by A12, A32, AFF_1:5;

then A44: x in K by A1, A2, A3, A4, A6, A7, A8, A9, A10, A11, A13, A43;

A45: a9 in Line (a9,c9) by A32, AFF_1:24;

then x in Line (a9,c9) by A32, A34, A42, AFF_1:25;

then K = Line (a9,c9) by A2, A5, A15, A34, A43, A44, AFF_1:18;

then a9 in Line (o,b) by A2, A3, A6, A21, A14, A20, A27, A22, A45, AFF_1:18;

then a in Line (o,b) by A24, A25, A28, A29, A18, AFF_1:48;

hence contradiction by A3, A6, A24, A27, A26, AFF_1:24; :: thesis: verum