let MS be OrtAfPl; ( MS is Moufangian iff MS is satisfying_TDES )
set AS = AffinStruct(# the carrier of MS, the CONGR of MS #);
A1:
now ( MS is satisfying_TDES implies MS is Moufangian )assume A2:
MS is
satisfying_TDES
;
MS is Moufangian now for K being Subset of AffinStruct(# the carrier of MS, the CONGR of MS #)
for o, a, b, c, a9, b9, c9 being Element of AffinStruct(# the carrier of MS, the CONGR of MS #) 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,c9let K be
Subset of
AffinStruct(# the
carrier of
MS, the
CONGR of
MS #);
for o, a, b, c, a9, b9, c9 being Element of AffinStruct(# the carrier of MS, the CONGR of MS #) 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,c9let o,
a,
b,
c,
a9,
b9,
c9 be
Element of
AffinStruct(# the
carrier of
MS, the
CONGR of
MS #);
( 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 A3:
K is
being_line
and A4:
o in K
and A5:
c in K
and A6:
c9 in K
and A7:
not
a in K
and A8:
o <> c
and A9:
a <> b
and A10:
LIN o,
a,
a9
and A11:
LIN o,
b,
b9
and A12:
a,
b // a9,
b9
and A13:
a,
c // a9,
c9
and A14:
a,
b // K
;
b,c // b9,c9reconsider o1 =
o,
a1 =
a,
b1 =
b,
c1 =
c,
a19 =
a9,
b19 =
b9,
c19 =
c9 as
Element of
MS ;
A15:
(
o1 <> b1 &
a1,
c1 // a19,
c19 )
by A4, A7, A13, A14, AFF_1:35, ANALMETR:36;
A16:
not
LIN o,
a,
c
A17:
not
LIN o,
a,
b
proof
set M =
Line (
a,
b);
assume
LIN o,
a,
b
;
contradiction
then
LIN a,
b,
o
by AFF_1:6;
then A18:
o in Line (
a,
b)
by AFF_1:def 2;
(
a in Line (
a,
b) &
Line (
a,
b)
// K )
by A9, A14, AFF_1:15, AFF_1:def 5;
then
a in K
by A4, A18, AFF_1:45;
hence
contradiction
by A3, A4, A5, A16, AFF_1:21;
verum
end;
a,
b // o,
c
by A3, A4, A5, A8, A14, AFF_1:27;
then
b,
a // o,
c
by AFF_1:4;
then A19:
b1,
a1 // o1,
c1
by ANALMETR:36;
A20:
(
LIN o1,
a1,
a19 &
LIN o1,
b1,
b19 )
by A10, A11, ANALMETR:40;
a1,
b1 // a19,
b19
by A12, ANALMETR:36;
then A21:
b1,
a1 // b19,
a19
by ANALMETR:59;
A22:
LIN o,
c,
c9
by A3, A4, A5, A6, AFF_1:21;
then A23:
LIN o1,
c1,
c19
by ANALMETR:40;
A24:
now ( a9 <> o implies b,c // b9,c9 )assume A25:
a9 <> o
;
b,c // b9,c9A26:
now ( a <> a9 implies b,c // b9,c9 )assume A27:
a <> a9
;
b,c // b9,c9A28:
not
LIN a1,
a19,
c1
proof
assume
LIN a1,
a19,
c1
;
contradiction
then A29:
LIN a,
a9,
c
by ANALMETR:40;
(
LIN a,
a9,
o &
LIN a,
a9,
a )
by A10, AFF_1:6, AFF_1:7;
hence
contradiction
by A16, A27, A29, AFF_1:8;
verum
end; A30:
not
LIN a1,
a19,
b1
proof
assume
LIN a1,
a19,
b1
;
contradiction
then A31:
LIN a,
a9,
b
by ANALMETR:40;
(
LIN a,
a9,
o &
LIN a,
a9,
a )
by A10, AFF_1:6, AFF_1:7;
hence
contradiction
by A17, A27, A31, AFF_1:8;
verum
end;
(
c,
a // c9,
a9 & not
LIN o,
c,
a )
by A13, A16, AFF_1:4, AFF_1:6;
then A32:
o1 <> c19
by A10, A25, AFF_1:55;
(
b,
a // b9,
a9 & not
LIN o,
b,
a )
by A12, A17, AFF_1:4, AFF_1:6;
then
o1 <> b19
by A10, A25, AFF_1:55;
then
b1,
c1 // b19,
c19
by A2, A4, A7, A8, A20, A23, A21, A19, A15, A25, A32, A28, A30, CONMETR:def 5;
hence
b,
c // b9,
c9
by ANALMETR:36;
verum end; now ( a = a9 implies b,c // b9,c9 )A33:
LIN o,
c,
c
by AFF_1:7;
assume A34:
a = a9
;
b,c // b9,c9then
a,
c // a9,
c
by AFF_1:2;
then A35:
c = c9
by A10, A13, A22, A16, A33, AFF_1:56;
A36:
LIN o,
b,
b
by AFF_1:7;
a,
b // a9,
b
by A34, AFF_1:2;
then
b = b9
by A10, A11, A12, A17, A36, AFF_1:56;
hence
b,
c // b9,
c9
by A35, AFF_1:2;
verum end; hence
b,
c // b9,
c9
by A26;
verum end; now ( a9 = o implies b,c // b9,c9 )assume
a9 = o
;
b,c // b9,c9then
(
b9 = o &
c9 = o )
by A11, A12, A13, A22, A16, A17, AFF_1:55;
hence
b,
c // b9,
c9
by AFF_1:3;
verum end; hence
b,
c // b9,
c9
by A24;
verum end; then
AffinStruct(# the
carrier of
MS, the
CONGR of
MS #) is
Moufangian
by AFF_2:def 7;
hence
MS is
Moufangian
;
verum end;
now ( MS is Moufangian implies MS is satisfying_TDES )assume
MS is
Moufangian
;
MS is satisfying_TDES then A37:
AffinStruct(# the
carrier of
MS, the
CONGR of
MS #) is
Moufangian
;
now for o, a, a1, b, b1, c, c1 being Element of MS st o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & not LIN b,b1,a & not LIN b,b1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,b // o,c & b,c // b1,c1 holds
a,c // a1,c1let o,
a,
a1,
b,
b1,
c,
c1 be
Element of
MS;
( o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & not LIN b,b1,a & not LIN b,b1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,b // o,c & b,c // b1,c1 implies a,c // a1,c1 )assume that
o <> a
and
o <> a1
and A38:
o <> b
and
o <> b1
and A39:
o <> c
and
o <> c1
and A40:
not
LIN b,
b1,
a
and A41:
not
LIN b,
b1,
c
and A42:
LIN o,
a,
a1
and A43:
LIN o,
b,
b1
and A44:
LIN o,
c,
c1
and A45:
a,
b // a1,
b1
and A46:
a,
b // o,
c
and A47:
b,
c // b1,
c1
;
a,c // a1,c1reconsider o9 =
o,
a9 =
a,
a19 =
a1,
b9 =
b,
b19 =
b1,
c9 =
c,
c19 =
c1 as
Element of
AffinStruct(# the
carrier of
MS, the
CONGR of
MS #) ;
set K =
Line (
o9,
c9);
A48:
Line (
o9,
c9) is
being_line
by A39, AFF_1:def 3;
a9,
b9 // o9,
c9
by A46, ANALMETR:36;
then
a9,
b9 // Line (
o9,
c9)
by A39, AFF_1:def 4;
then A49:
b9,
a9 // Line (
o9,
c9)
by AFF_1:34;
a9,
b9 // a19,
b19
by A45, ANALMETR:36;
then A50:
b9,
a9 // b19,
a19
by AFF_1:4;
A51:
c9 in Line (
o9,
c9)
by AFF_1:15;
A52:
(
LIN o9,
a9,
a19 &
b9,
c9 // b19,
c19 )
by A42, A47, ANALMETR:36, ANALMETR:40;
A53:
b9 <> a9
by A40, Th1;
A54:
o9 in Line (
o9,
c9)
by AFF_1:15;
A55:
LIN o9,
b9,
b19
by A43, ANALMETR:40;
A56:
not
b9 in Line (
o9,
c9)
proof
assume A57:
b9 in Line (
o9,
c9)
;
contradiction
then
b19 in Line (
o9,
c9)
by A38, A48, A54, A55, AFF_1:25;
then
LIN b9,
b19,
c9
by A48, A51, A57, AFF_1:21;
hence
contradiction
by A41, ANALMETR:40;
verum
end;
LIN o9,
c9,
c19
by A44, ANALMETR:40;
then
c19 in Line (
o9,
c9)
by A39, A48, A54, A51, AFF_1:25;
then
a9,
c9 // a19,
c19
by A37, A39, A48, A54, A51, A55, A56, A49, A50, A52, A53, AFF_2:def 7;
hence
a,
c // a1,
c1
by ANALMETR:36;
verum end; hence
MS is
satisfying_TDES
by CONMETR:def 5;
verum end;
hence
( MS is Moufangian iff MS is satisfying_TDES )
by A1; verum