let X be OrtAfPl; :: thesis: ( X is satisfying_TDES implies AffinStruct(# the carrier of X, the CONGR of X #) is Moufangian )
assume A1: X is satisfying_TDES ; :: thesis: AffinStruct(# the carrier of X, the CONGR of X #) is Moufangian
let K9 be Subset of AffinStruct(# the carrier of X, the CONGR of X #); :: according to AFF_2:def 7 :: thesis: for b₁, b₂, b₃, b₄, b₅, b₆, b₇ being Element of the carrier of AffinStruct(# the carrier of X, the CONGR of X #) holds
( not K9 is being_line or not b₁ in K9 or not b₄ in K9 or not b₇ in K9 or b₂ in K9 or b₁ = b₄ or b₂ = b₃ or not LIN b₁,b₂,b₅ or not LIN b₁,b₃,b₆ or not b₂,b₃ // b₅,b₆ or not b₂,b₄ // b₅,b₇ or not b₂,b₃ // K9 or b₃,b₄ // b₆,b₇ )
let o9, a9, b9, c9, a19, b19, c19 be Element of AffinStruct(# the carrier of X, the CONGR of X #); :: thesis: ( not K9 is being_line or not o9 in K9 or not c9 in K9 or not c19 in K9 or a9 in K9 or o9 = c9 or a9 = b9 or not LIN o9,a9,a19 or not LIN o9,b9,b19 or not a9,b9 // a19,b19 or not a9,c9 // a19,c19 or not a9,b9 // K9 or b9,c9 // b19,c19 )
assume that
A2: K9 is being_line and
A3: o9 in K9 and
A4: c9 in K9 and
A5: c19 in K9 and
A6: not a9 in K9 and
A7: o9 <> c9 and
A8: a9 <> b9 and
A9: LIN o9,a9,a19 and
A10: LIN o9,b9,b19 and
A11: a9,b9 // a19,b19 and
A12: a9,c9 // a19,c19 and
A13: a9,b9 // K9 ; :: thesis: b9,c9 // b19,c19
reconsider K = K9 as Subset of X ;
reconsider o = o9, a = a9, a1 = a19, b = b9, b1 = b19, c = c9, c1 = c19 as Element of X ;
A14: a,c // a1,c1 by A12, ANALMETR:36;
A15: a,b // a1,b1 by A11, ANALMETR:36;

now :: thesis: ( not b in K implies b9,c9 // b19,c19 )

A16: now :: thesis: ( o <> a1 implies b9,c9 // b19,c19 )

assume A17: o <> a1 ; :: thesis: b9,c9 // b19,c19
A18: ( o <> a & o <> b & o <> c & o <> c1 & o <> b1 )

proof

A19: now :: thesis: not o = b1

o9,c9 // K9 by A2, A3, A4, AFF_1:23;
then A20: a9,b9 // o9,c9 by A2, A13, AFF_1:31;
assume o = b1 ; :: thesis: contradiction
then a19,o9 // o9,c9 by A8, A11, A20, DIRAF:40;
then o9,c9 // o9,a19 by AFF_1:4;
then LIN o9,c9,a19 by AFF_1:def 1;
then A21: a19 in K9 by A2, A3, A4, A7, AFF_1:25;
LIN o9,a19,a9 by A9, AFF_1:6;
hence contradiction by A2, A3, A6, A17, A21, AFF_1:25; :: thesis: verum

end;

A22: now :: thesis: not o = c1

o9,a9 // o9,a19 by A9, AFF_1:def 1;
then A23: o9,a19 // a9,o9 by AFF_1:4;
assume o = c1 ; :: thesis: contradiction
then o9,a19 // a9,c9 by A12, AFF_1:4;
then a9,c9 // a9,o9 by A17, A23, DIRAF:40;
then LIN a9,c9,o9 by AFF_1:def 1;
then LIN o9,c9,a9 by AFF_1:6;
hence contradiction by A2, A3, A4, A6, A7, AFF_1:25; :: thesis: verum

end;

assume ( o = a or o = b or o = c or o = c1 or o = b1 ) ; :: thesis: contradiction
hence contradiction by A3, A6, A7, A13, A22, A19, AFF_1:35; :: thesis: verum

end;

A24: now :: thesis: ( a <> a19 implies b9,c9 // b19,c19 )

assume A25: a <> a19 ; :: thesis: b9,c9 // b19,c19
A26: ( not LIN a,a1,b & not LIN a,a1,c )

proof

A27: now :: thesis: not LIN a,a1,b

LIN a9,a19,o9 by A9, AFF_1:6;
then a9,a19 // a9,o9 by AFF_1:def 1;
then A28: a,a1 // a,o by ANALMETR:36;
assume LIN a,a1,b ; :: thesis: contradiction
then a,a1 // a,b by ANALMETR:def 10;
then a,b // a,o by A25, A28, ANALMETR:60;
then A29: a,b // o,a by ANALMETR:59;
a9,b9 // o9,c9 by A2, A3, A4, A7, A13, AFF_1:27;
then a,b // o,c by ANALMETR:36;
then o,c // o,a by A8, A29, ANALMETR:60;
then LIN o,c,a by ANALMETR:def 10;
then LIN o9,c9,a9 by ANALMETR:40;
hence contradiction by A2, A3, A4, A6, A7, AFF_1:25; :: thesis: verum

end;

A30: now :: thesis: not LIN a,a1,c

LIN a9,a19,o9 by A9, AFF_1:6;
then a9,a19 // a9,o9 by AFF_1:def 1;
then A31: a,a1 // a,o by ANALMETR:36;
assume LIN a,a1,c ; :: thesis: contradiction
then a,a1 // a,c by ANALMETR:def 10;
then a,c // a,o by A25, A31, ANALMETR:60;
then LIN a,c,o by ANALMETR:def 10;
then LIN a9,c9,o9 by ANALMETR:40;
then LIN c9,o9,a9 by AFF_1:6;
hence contradiction by A2, A3, A4, A6, A7, AFF_1:25; :: thesis: verum

end;

assume ( LIN a,a1,b or LIN a,a1,c ) ; :: thesis: contradiction
hence contradiction by A27, A30; :: thesis: verum

end;

A32: LIN o,b,b1 by A10, ANALMETR:40;
o9,c9 // o9,c19 by A2, A3, A4, A5, AFF_1:39, AFF_1:41;
then o,c // o,c1 by ANALMETR:36;
then A33: LIN o,c,c1 by ANALMETR:def 10;
o9,c9 // K9 by A2, A3, A4, AFF_1:40, AFF_1:41;
then a9,b9 // o9,c9 by A2, A13, AFF_1:31;
then b9,a9 // o9,c9 by AFF_1:4;
then A34: b,a // o,c by ANALMETR:36;
A35: b,a // b1,a1 by A15, ANALMETR:59;
LIN o,a,a1 by A9, ANALMETR:40;
then b,c // b1,c1 by A1, A14, A17, A18, A26, A32, A33, A35, A34;
hence b9,c9 // b19,c19 by ANALMETR:36; :: thesis: verum

end;

now :: thesis: ( a = a1 implies b9,c9 // b19,c19 )

A36: not LIN o9,a9,c9

proof

assume LIN o9,a9,c9 ; :: thesis: contradiction
then LIN o9,c9,a9 by AFF_1:6;
hence contradiction by A2, A3, A4, A6, A7, AFF_1:25; :: thesis: verum

end;

assume A37: a = a1 ; :: thesis: b9,c9 // b19,c19
o9,c9 // o9,c19 by A2, A3, A4, A5, AFF_1:39, AFF_1:41;
then LIN o9,c9,c19 by AFF_1:def 1;
then A38: c9 = c19 by A12, A37, A36, AFF_1:14;
not LIN o9,a9,b9

proof

assume LIN o9,a9,b9 ; :: thesis: contradiction
then LIN a9,b9,o9 by AFF_1:6;
then A39: a9,b9 // a9,o9 by AFF_1:def 1;
o9,c9 // K9 by A2, A3, A4, AFF_1:23;
then a9,b9 // o9,c9 by A2, A13, AFF_1:31;
then a9,o9 // o9,c9 by A8, A39, DIRAF:40;
then o9,c9 // o9,a9 by AFF_1:4;
then LIN o9,c9,a9 by AFF_1:def 1;
hence contradiction by A2, A3, A4, A6, A7, AFF_1:25; :: thesis: verum

end;

then b9 = b19 by A10, A11, A37, AFF_1:14;
hence b9,c9 // b19,c19 by A38, AFF_1:2; :: thesis: verum

end;

hence b9,c9 // b19,c19 by A24; :: thesis: verum

end;

assume A40: not b in K ; :: thesis: b9,c9 // b19,c19
A41: ( o = a1 implies ( o = b1 & o = c1 ) )

proof

assume that
A42: o = a1 and
A43: ( o <> b1 or o <> c1 ) ; :: thesis: contradiction

A44: now :: thesis: not o <> c1

A45: o9,c19 // a9,c9 by A12, A42, AFF_1:4;
assume A46: o <> c1 ; :: thesis: contradiction
o9,c19 // o9,c9 by A2, A3, A4, A5, AFF_1:39, AFF_1:41;
then a9,c9 // o9,c9 by A46, A45, DIRAF:40;
then c9,a9 // c9,o9 by AFF_1:4;
then LIN c9,a9,o9 by AFF_1:def 1;
then LIN o9,c9,a9 by AFF_1:6;
hence contradiction by A2, A3, A4, A6, A7, AFF_1:25; :: thesis: verum

end;

now :: thesis: not o <> b1

o9,c9 // K9 by A2, A3, A4, AFF_1:23;
then a9,b9 // o9,c9 by A2, A13, AFF_1:31;
then o9,c9 // o9,b19 by A8, A11, A42, DIRAF:40;
then LIN o9,c9,b19 by AFF_1:def 1;
then A47: b19 in K9 by A2, A3, A4, A7, AFF_1:25;
assume A48: o <> b1 ; :: thesis: contradiction
LIN o9,b19,b9 by A10, AFF_1:6;
hence contradiction by A2, A3, A40, A48, A47, AFF_1:25; :: thesis: verum

end;

hence contradiction by A43, A44; :: thesis: verum

end;

now :: thesis: ( o = a1 implies b9,c9 // b19,c19 )

assume o = a1 ; :: thesis: b9,c9 // b19,c19
then b,c // b1,c1 by A41, ANALMETR:39;
hence b9,c9 // b19,c19 by ANALMETR:36; :: thesis: verum

end;

hence b9,c9 // b19,c19 by A16; :: thesis: verum

end;

hence b9,c9 // b19,c19 by A6, A13, AFF_1:35; :: thesis: verum