let X be OrtAfPl; ( X is satisfying_TDES iff AffinStruct(# the U1 of X, the CONGR of X #) is Moufangian )
( AffinStruct(# the U1 of X, the CONGR of X #) is Moufangian implies X is satisfying_TDES )
proof
assume A1:
AffinStruct(# the
U1 of
X, the
CONGR of
X #) is
Moufangian
;
X is satisfying_TDES
now for o9, a9, a19, b9, b19, c9, c19 being Element of X st o9 <> a9 & o9 <> a19 & o9 <> b9 & o9 <> b19 & o9 <> c9 & o9 <> c19 & not LIN b9,b19,a9 & not LIN b9,b19,c9 & LIN o9,a9,a19 & LIN o9,b9,b19 & LIN o9,c9,c19 & a9,b9 // a19,b19 & a9,b9 // o9,c9 & b9,c9 // b19,c19 holds
a9,c9 // a19,c19let o9,
a9,
a19,
b9,
b19,
c9,
c19 be
Element of
X;
( o9 <> a9 & o9 <> a19 & o9 <> b9 & o9 <> b19 & o9 <> c9 & o9 <> c19 & not LIN b9,b19,a9 & not LIN b9,b19,c9 & LIN o9,a9,a19 & LIN o9,b9,b19 & LIN o9,c9,c19 & a9,b9 // a19,b19 & a9,b9 // o9,c9 & b9,c9 // b19,c19 implies a9,c9 // a19,c19 )assume that
o9 <> a9
and
o9 <> a19
and A2:
o9 <> b9
and
o9 <> b19
and A3:
o9 <> c9
and
o9 <> c19
and A4:
not
LIN b9,
b19,
a9
and A5:
not
LIN b9,
b19,
c9
and A6:
LIN o9,
a9,
a19
and A7:
LIN o9,
b9,
b19
and A8:
LIN o9,
c9,
c19
and A9:
a9,
b9 // a19,
b19
and A10:
a9,
b9 // o9,
c9
and A11:
b9,
c9 // b19,
c19
;
a9,c9 // a19,c19reconsider o =
o9,
a =
a9,
a1 =
a19,
b =
b9,
b1 =
b19,
c =
c9,
c1 =
c19 as
Element of
AffinStruct(# the
U1 of
X, the
CONGR of
X #) ;
A12:
LIN o,
b,
b1
by A7, ANALMETR:40;
LIN o,
c,
c1
by A8, ANALMETR:40;
then consider M being
Subset of
AffinStruct(# the
U1 of
X, the
CONGR of
X #)
such that A13:
M is
being_line
and A14:
o in M
and A15:
c in M
and A16:
c1 in M
by AFF_1:21;
A17:
not
LIN b,
b1,
c
by A5, ANALMETR:40;
A18:
not
b in M
proof
LIN b,
b1,
o
by A12, AFF_1:6;
then
b,
b1 // b,
o
by AFF_1:def 1;
then A19:
b,
b1 // o,
b
by AFF_1:4;
assume
b in M
;
contradiction
then
o,
b // b,
c
by A13, A14, A15, AFF_1:39, AFF_1:41;
then
b,
b1 // b,
c
by A2, A19, AFF_1:5;
hence
contradiction
by A17, AFF_1:def 1;
verum
end;
a,
b // a1,
b1
by A9, ANALMETR:36;
then A20:
b,
a // b1,
a1
by AFF_1:4;
not
LIN b,
b1,
a
by A4, ANALMETR:40;
then A21:
b <> a
by AFF_1:7;
A22:
b,
c // b1,
c1
by A11, ANALMETR:36;
A23:
LIN o,
a,
a1
by A6, ANALMETR:40;
a,
b // o,
c
by A10, ANALMETR:36;
then
b,
a // o,
c
by AFF_1:4;
then
b,
a // M
by A3, A13, A14, A15, AFF_1:27;
then
a,
c // a1,
c1
by A1, A3, A23, A12, A13, A14, A15, A16, A18, A21, A20, A22, AFF_2:def 7;
hence
a9,
c9 // a19,
c19
by ANALMETR:36;
verum end;
hence
X is
satisfying_TDES
by CONMETR:def 5;
verum
end;
hence
( X is satisfying_TDES iff AffinStruct(# the U1 of X, the CONGR of X #) is Moufangian )
by CONMETR:7; verum