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 b1, b2, b3, b4, b5, b6, b7 being Element of the carrier of AffinStruct(# the carrier of X, the CONGR of X #) holds
( not K9 is being_line or not b1 in K9 or not b4 in K9 or not b7 in K9 or b2 in K9 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 // K9 or b3,b4 // b6,b7 )
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
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