let AP be AffinPlane; ( AP is satisfying_TDES_3 implies AP is Moufangian )
assume A1:
AP is satisfying_TDES_3
; AP is Moufangian
let K be Subset of AP; AFF_2:def 7 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; ( 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
; 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
; 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
assume
Line (
o,
a)
= Line (
o,
b)
;
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;
verum
end;
A27:
o in Line (o,b)
by A23, AFF_1:24;
then A28:
b9 in Line (o,b)
by A10, A23, A24, A25, AFF_1:25;
A29:
a9 <> b9
proof
A30:
a9,
c9 // c,
a
by A12, AFF_1:4;
assume A31:
a9 = b9
;
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;
verum
end;
A32:
a9 <> c9
proof
assume
a9 = c9
;
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;
verum
end;
then A34:
( Line (a9,c9) is being_line & c9 in Line (a9,c9) )
by AFF_1:24;
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
assume
LIN a,
b,
c
;
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;
verum
end;
not a9,c9 // N
proof
assume A40:
a9,
c9 // N
;
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;
verum
end;
then consider x being Element of AP such that
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; verum