let X be OrtAfPl; ( X is satisfying_TDES implies Af X is Moufangian )
assume A1:
X is satisfying_TDES
; Af X is Moufangian
let K' be Subset of ; AFF_2:def 7 for b1, b2, b3, b4, b5, b6, b7 being Element of the carrier of (Af X) holds
( not K' is being_line or not b1 in K' or not b4 in K' or not b7 in K' or b2 in K' or b1 = b4 or b2 = b3 or not LIN b1,b2,b5 or not LIN b1,b3,b6 or not b2,b3 // b5,b6 or not b2,b4 // b5,b7 or not b2,b3 // K' or b3,b4 // b6,b7 )
let o', a', b', c', a1', b1', c1' be Element of ; ( not K' is being_line or not o' in K' or not c' in K' or not c1' in K' or a' in K' or o' = c' or a' = b' or not LIN o',a',a1' or not LIN o',b',b1' or not a',b' // a1',b1' or not a',c' // a1',c1' or not a',b' // K' or b',c' // b1',c1' )
assume that
A2:
K' is being_line
and
A3:
o' in K'
and
A4:
c' in K'
and
A5:
c1' in K'
and
A6:
not a' in K'
and
A7:
o' <> c'
and
A8:
a' <> b'
and
A9:
LIN o',a',a1'
and
A10:
LIN o',b',b1'
and
A11:
a',b' // a1',b1'
and
A12:
a',c' // a1',c1'
and
A13:
a',b' // K'
; b',c' // b1',c1'
reconsider K = K' as Subset of by ANALMETR:57;
reconsider o = o', a = a', a1 = a1', b = b', b1 = b1', c = c', c1 = c1' as Element of by ANALMETR:47;
A14:
a,c // a1,c1
by A12, ANALMETR:48;
A15:
a,b // a1,b1
by A11, ANALMETR:48;
now A16:
now assume A17:
o <> a1
;
b',c' // b1',c1'A18:
(
o <> a &
o <> b &
o <> c &
o <> c1 &
o <> b1 )
proof
A19:
now
o',
c' // K'
by A2, A3, A4, AFF_1:37;
then A20:
a',
b' // o',
c'
by A2, A13, AFF_1:45;
assume
o = b1
;
contradictionthen
a1',
o' // o',
c'
by A8, A11, A20, DIRAF:47;
then
o',
c' // o',
a1'
by AFF_1:13;
then
LIN o',
c',
a1'
by AFF_1:def 1;
then A21:
a1' in K'
by A2, A3, A4, A7, AFF_1:39;
LIN o',
a1',
a'
by A9, AFF_1:15;
hence
contradiction
by A2, A3, A6, A17, A21, AFF_1:39;
verum end;
A22:
now
o',
a' // o',
a1'
by A9, AFF_1:def 1;
then A23:
o',
a1' // a',
o'
by AFF_1:13;
assume
o = c1
;
contradictionthen
o',
a1' // a',
c'
by A12, AFF_1:13;
then
a',
c' // a',
o'
by A17, A23, DIRAF:47;
then
LIN a',
c',
o'
by AFF_1:def 1;
then
LIN o',
c',
a'
by AFF_1:15;
hence
contradiction
by A2, A3, A4, A6, A7, AFF_1:39;
verum end;
assume
(
o = a or
o = b or
o = c or
o = c1 or
o = b1 )
;
contradiction
hence
contradiction
by A3, A6, A7, A13, A22, A19, AFF_1:49;
verum
end; A24:
now assume A25:
a <> a1'
;
b',c' // b1',c1'A26:
( not
LIN a,
a1,
b & not
LIN a,
a1,
c )
proof
A27:
now
LIN a',
a1',
o'
by A9, AFF_1:15;
then
a',
a1' // a',
o'
by AFF_1:def 1;
then A28:
a,
a1 // a,
o
by ANALMETR:48;
assume
LIN a,
a1,
b
;
contradictionthen
a,
a1 // a,
b
by ANALMETR:def 11;
then
a,
b // a,
o
by A25, A28, ANALMETR:82;
then A29:
a,
b // o,
a
by ANALMETR:81;
a',
b' // o',
c'
by A2, A3, A4, A7, A13, AFF_1:41;
then
a,
b // o,
c
by ANALMETR:48;
then
o,
c // o,
a
by A8, A29, ANALMETR:82;
then
LIN o,
c,
a
by ANALMETR:def 11;
then
LIN o',
c',
a'
by ANALMETR:55;
hence
contradiction
by A2, A3, A4, A6, A7, AFF_1:39;
verum end;
A30:
now
LIN a',
a1',
o'
by A9, AFF_1:15;
then
a',
a1' // a',
o'
by AFF_1:def 1;
then A31:
a,
a1 // a,
o
by ANALMETR:48;
assume
LIN a,
a1,
c
;
contradictionthen
a,
a1 // a,
c
by ANALMETR:def 11;
then
a,
c // a,
o
by A25, A31, ANALMETR:82;
then
LIN a,
c,
o
by ANALMETR:def 11;
then
LIN a',
c',
o'
by ANALMETR:55;
then
LIN c',
o',
a'
by AFF_1:15;
hence
contradiction
by A2, A3, A4, A6, A7, AFF_1:39;
verum end;
assume
(
LIN a,
a1,
b or
LIN a,
a1,
c )
;
contradiction
hence
contradiction
by A27, A30;
verum
end; A32:
LIN o,
b,
b1
by A10, ANALMETR:55;
o',
c' // o',
c1'
by A2, A3, A4, A5, AFF_1:53, AFF_1:55;
then
o,
c // o,
c1
by ANALMETR:48;
then A33:
LIN o,
c,
c1
by ANALMETR:def 11;
o',
c' // K'
by A2, A3, A4, AFF_1:54, AFF_1:55;
then
a',
b' // o',
c'
by A2, A13, AFF_1:45;
then
b',
a' // o',
c'
by AFF_1:13;
then A34:
b,
a // o,
c
by ANALMETR:48;
A35:
b,
a // b1,
a1
by A15, ANALMETR:81;
LIN o,
a,
a1
by A9, ANALMETR:55;
then
b,
c // b1,
c1
by A1, A14, A17, A18, A26, A32, A33, A35, A34, Def5;
hence
b',
c' // b1',
c1'
by ANALMETR:48;
verum end; now A36:
not
LIN o',
a',
c'
assume A37:
a = a1
;
b',c' // b1',c1'
o',
c' // o',
c1'
by A2, A3, A4, A5, AFF_1:53, AFF_1:55;
then
LIN o',
c',
c1'
by AFF_1:def 1;
then A38:
c' = c1'
by A12, A37, A36, AFF_1:23;
not
LIN o',
a',
b'
proof
assume
LIN o',
a',
b'
;
contradiction
then
LIN a',
b',
o'
by AFF_1:15;
then A39:
a',
b' // a',
o'
by AFF_1:def 1;
o',
c' // K'
by A2, A3, A4, AFF_1:37;
then
a',
b' // o',
c'
by A2, A13, AFF_1:45;
then
a',
o' // o',
c'
by A8, A39, DIRAF:47;
then
o',
c' // o',
a'
by AFF_1:13;
then
LIN o',
c',
a'
by AFF_1:def 1;
hence
contradiction
by A2, A3, A4, A6, A7, AFF_1:39;
verum
end; then
b' = b1'
by A10, A11, A37, AFF_1:23;
hence
b',
c' // b1',
c1'
by A38, AFF_1:11;
verum end; hence
b',
c' // b1',
c1'
by A24;
verum end; assume A40:
not
b in K
;
b',c' // b1',c1'A41:
(
o = a1 implies (
o = b1 &
o = c1 ) )
proof
assume that A42:
o = a1
and A43:
(
o <> b1 or
o <> c1 )
;
contradiction
A44:
now A45:
o',
c1' // a',
c'
by A12, A42, AFF_1:13;
assume A46:
o <> c1
;
contradiction
o',
c1' // o',
c'
by A2, A3, A4, A5, AFF_1:53, AFF_1:55;
then
a',
c' // o',
c'
by A46, A45, DIRAF:47;
then
c',
a' // c',
o'
by AFF_1:13;
then
LIN c',
a',
o'
by AFF_1:def 1;
then
LIN o',
c',
a'
by AFF_1:15;
hence
contradiction
by A2, A3, A4, A6, A7, AFF_1:39;
verum end;
now
o',
c' // K'
by A2, A3, A4, AFF_1:37;
then
a',
b' // o',
c'
by A2, A13, AFF_1:45;
then
o',
c' // o',
b1'
by A8, A11, A42, DIRAF:47;
then
LIN o',
c',
b1'
by AFF_1:def 1;
then A47:
b1' in K'
by A2, A3, A4, A7, AFF_1:39;
assume A48:
o <> b1
;
contradiction
LIN o',
b1',
b'
by A10, AFF_1:15;
hence
contradiction
by A2, A3, A40, A48, A47, AFF_1:39;
verum end;
hence
contradiction
by A43, A44;
verum
end; hence
b',
c' // b1',
c1'
by A16;
verum
hence
b',c' // b1',c1'
by A6, A13, AFF_1:49; verum