let X be OrtAfPl; :: thesis: ( X is satisfying_TDES iff Af X is Moufangian )
( Af X is Moufangian implies X is satisfying_TDES )
proof
assume A1:
Af X is
Moufangian
;
:: thesis: X is satisfying_TDES
now let o',
a',
a1',
b',
b1',
c',
c1' be
Element of
X;
:: thesis: ( 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 A2:
o' <> b'
and
o' <> b1'
and A3:
o' <> c'
and
o' <> c1'
and A4:
not
LIN b',
b1',
a'
and A5:
not
LIN b',
b1',
c'
and A6:
LIN o',
a',
a1'
and A7:
LIN o',
b',
b1'
and A8:
LIN o',
c',
c1'
and A9:
a',
b' // a1',
b1'
and A10:
a',
b' // o',
c'
and A11:
b',
c' // b1',
c1'
;
:: thesis: a',c' // a1',c1'reconsider o =
o',
a =
a',
a1 =
a1',
b =
b',
b1 =
b1',
c =
c',
c1 =
c1' as
Element of
(Af X) by ANALMETR:47;
A12:
LIN o,
b,
b1
by A7, ANALMETR:55;
LIN o,
c,
c1
by A8, ANALMETR:55;
then consider M being
Subset of
(Af 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:33;
A17:
not
LIN b,
b1,
c
by A5, ANALMETR:55;
A18:
not
b in M
proof
LIN b,
b1,
o
by A12, AFF_1:15;
then
b,
b1 // b,
o
by AFF_1:def 1;
then A19:
b,
b1 // o,
b
by AFF_1:13;
assume
b in M
;
:: thesis: contradiction
then
o,
b // b,
c
by A13, A14, A15, AFF_1:53, AFF_1:55;
then
b,
b1 // b,
c
by A2, A19, AFF_1:14;
hence
contradiction
by A17, AFF_1:def 1;
:: thesis: verum
end;
a,
b // a1,
b1
by A9, ANALMETR:48;
then A20:
b,
a // b1,
a1
by AFF_1:13;
not
LIN b,
b1,
a
by A4, ANALMETR:55;
then A21:
b <> a
by AFF_1:16;
A22:
b,
c // b1,
c1
by A11, ANALMETR:48;
A23:
LIN o,
a,
a1
by A6, ANALMETR:55;
a,
b // o,
c
by A10, ANALMETR:48;
then
b,
a // o,
c
by AFF_1:13;
then
b,
a // M
by A3, A13, A14, A15, AFF_1:41;
then
a,
c // a1,
c1
by A1, A3, A23, A12, A13, A14, A15, A16, A18, A21, A20, A22, AFF_2:def 7;
hence
a',
c' // a1',
c1'
by ANALMETR:48;
:: thesis: verum end;
hence
X is
satisfying_TDES
by CONMETR:def 5;
:: thesis: verum
end;
hence
( X is satisfying_TDES iff Af X is Moufangian )
by CONMETR:7; :: thesis: verum