let MS be OrtAfPl; :: thesis: ( MS is Moufangian iff MS is satisfying_TDES )
set AS = Af MS;
A1:
now assume A2:
MS is
satisfying_TDES
;
:: thesis: MS is Moufangian now let K be
Subset of
(Af MS);
:: thesis: for o, a, b, c, a', b', c' being Element of (Af MS) st K is being_line & o in K & c in K & c' in K & not a in K & o <> c & a <> b & LIN o,a,a' & LIN o,b,b' & a,b // a',b' & a,c // a',c' & a,b // K holds
b,c // b',c'let o,
a,
b,
c,
a',
b',
c' be
Element of
(Af MS);
:: thesis: ( K is being_line & o in K & c in K & c' in K & not a in K & o <> c & a <> b & LIN o,a,a' & LIN o,b,b' & a,b // a',b' & a,c // a',c' & a,b // K implies b,c // b',c' )assume that A3:
K is
being_line
and A4:
o in K
and A5:
c in K
and A6:
c' in K
and A7:
not
a in K
and A8:
o <> c
and A9:
a <> b
and A10:
LIN o,
a,
a'
and A11:
LIN o,
b,
b'
and A12:
a,
b // a',
b'
and A13:
a,
c // a',
c'
and A14:
a,
b // K
;
:: thesis: b,c // b',c'reconsider o1 =
o,
a1 =
a,
b1 =
b,
c1 =
c,
a1' =
a',
b1' =
b',
c1' =
c' as
Element of
MS by ANALMETR:47;
A15:
(
o1 <> b1 &
a1,
c1 // a1',
c1' )
by A4, A7, A13, A14, AFF_1:49, ANALMETR:48;
A16:
not
LIN o,
a,
c
A17:
not
LIN o,
a,
b
proof
set M =
Line a,
b;
assume
LIN o,
a,
b
;
:: thesis: contradiction
then
LIN a,
b,
o
by AFF_1:15;
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:26, AFF_1:def 5;
then
a in K
by A4, A18, AFF_1:59;
hence
contradiction
by A3, A4, A5, A16, AFF_1:33;
:: thesis: verum
end;
a,
b // o,
c
by A3, A4, A5, A8, A14, AFF_1:41;
then
b,
a // o,
c
by AFF_1:13;
then A19:
b1,
a1 // o1,
c1
by ANALMETR:48;
A20:
(
LIN o1,
a1,
a1' &
LIN o1,
b1,
b1' )
by A10, A11, ANALMETR:55;
a1,
b1 // a1',
b1'
by A12, ANALMETR:48;
then A21:
b1,
a1 // b1',
a1'
by ANALMETR:81;
A22:
LIN o,
c,
c'
by A3, A4, A5, A6, AFF_1:33;
then A23:
LIN o1,
c1,
c1'
by ANALMETR:55;
A24:
now assume A25:
a' <> o
;
:: thesis: b,c // b',c'A26:
now assume A27:
a <> a'
;
:: thesis: b,c // b',c'A28:
not
LIN a1,
a1',
c1
proof
assume
LIN a1,
a1',
c1
;
:: thesis: contradiction
then A29:
LIN a,
a',
c
by ANALMETR:55;
(
LIN a,
a',
o &
LIN a,
a',
a )
by A10, AFF_1:15, AFF_1:16;
hence
contradiction
by A16, A27, A29, AFF_1:17;
:: thesis: verum
end; A30:
not
LIN a1,
a1',
b1
proof
assume
LIN a1,
a1',
b1
;
:: thesis: contradiction
then A31:
LIN a,
a',
b
by ANALMETR:55;
(
LIN a,
a',
o &
LIN a,
a',
a )
by A10, AFF_1:15, AFF_1:16;
hence
contradiction
by A17, A27, A31, AFF_1:17;
:: thesis: verum
end;
(
c,
a // c',
a' & not
LIN o,
c,
a )
by A13, A16, AFF_1:13, AFF_1:15;
then A32:
o1 <> c1'
by A10, A25, AFF_1:69;
(
b,
a // b',
a' & not
LIN o,
b,
a )
by A12, A17, AFF_1:13, AFF_1:15;
then
o1 <> b1'
by A10, A25, AFF_1:69;
then
b1,
c1 // b1',
c1'
by A2, A4, A7, A8, A20, A23, A21, A19, A15, A25, A32, A28, A30, CONMETR:def 5;
hence
b,
c // b',
c'
by ANALMETR:48;
:: thesis: verum end; now A33:
LIN o,
c,
c
by AFF_1:16;
assume A34:
a = a'
;
:: thesis: b,c // b',c'then
a,
c // a',
c
by AFF_1:11;
then A35:
c = c'
by A10, A13, A22, A16, A33, AFF_1:70;
A36:
LIN o,
b,
b
by AFF_1:16;
a,
b // a',
b
by A34, AFF_1:11;
then
b = b'
by A10, A11, A12, A17, A36, AFF_1:70;
hence
b,
c // b',
c'
by A35, AFF_1:11;
:: thesis: verum end; hence
b,
c // b',
c'
by A26;
:: thesis: verum end; now assume
a' = o
;
:: thesis: b,c // b',c'then
(
b' = o &
c' = o )
by A11, A12, A13, A22, A16, A17, AFF_1:69;
hence
b,
c // b',
c'
by AFF_1:12;
:: thesis: verum end; hence
b,
c // b',
c'
by A24;
:: thesis: verum end; then
Af MS is
Moufangian
by AFF_2:def 7;
hence
MS is
Moufangian
by Def5;
:: thesis: verum end;
now assume
MS is
Moufangian
;
:: thesis: MS is satisfying_TDES then A37:
Af MS is
Moufangian
by Def5;
now let o,
a,
a1,
b,
b1,
c,
c1 be
Element of
MS;
:: 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 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
;
:: thesis: a,c // a1,c1reconsider o' =
o,
a' =
a,
a1' =
a1,
b' =
b,
b1' =
b1,
c' =
c,
c1' =
c1 as
Element of
(Af MS) by ANALMETR:47;
set K =
Line o',
c';
A48:
Line o',
c' is
being_line
by A39, AFF_1:def 3;
a',
b' // o',
c'
by A46, ANALMETR:48;
then
a',
b' // Line o',
c'
by A39, AFF_1:def 4;
then A49:
b',
a' // Line o',
c'
by AFF_1:48;
a',
b' // a1',
b1'
by A45, ANALMETR:48;
then A50:
b',
a' // b1',
a1'
by AFF_1:13;
A51:
c' in Line o',
c'
by AFF_1:26;
A52:
(
LIN o',
a',
a1' &
b',
c' // b1',
c1' )
by A42, A47, ANALMETR:48, ANALMETR:55;
A53:
b' <> a'
by A40, Th1;
A54:
o' in Line o',
c'
by AFF_1:26;
A55:
LIN o',
b',
b1'
by A43, ANALMETR:55;
A56:
not
b' in Line o',
c'
proof
assume A57:
b' in Line o',
c'
;
:: thesis: contradiction
then
b1' in Line o',
c'
by A38, A48, A54, A55, AFF_1:39;
then
LIN b',
b1',
c'
by A48, A51, A57, AFF_1:33;
hence
contradiction
by A41, ANALMETR:55;
:: thesis: verum
end;
LIN o',
c',
c1'
by A44, ANALMETR:55;
then
c1' in Line o',
c'
by A39, A48, A54, A51, AFF_1:39;
then
a',
c' // a1',
c1'
by A37, A39, A48, A54, A51, A55, A56, A49, A50, A52, A53, AFF_2:def 7;
hence
a,
c // a1,
c1
by ANALMETR:48;
:: thesis: verum end; hence
MS is
satisfying_TDES
by CONMETR:def 5;
:: thesis: verum end;
hence
( MS is Moufangian iff MS is satisfying_TDES )
by A1; :: thesis: verum