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 the carrier 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 the carrier 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 & c in K & c' in K ) and
A5: not a in K and
A6: ( o <> c & a <> b ) and
A7: ( LIN o,a,a' & LIN o,b,b' ) and
A8: ( a,b // a',b' & a,c // a',c' ) and
A9: 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;
A10: LIN o,c,c' by A3, A4, AFF_1:33;
then A11: ( LIN o1,a1,a1' & LIN o1,b1,b1' & LIN o1,c1,c1' ) by A7, ANALMETR:55;
A12: ( o1 <> c1 & o1 <> a1 & o1 <> b1 ) by A4, A5, A6, A9, AFF_1:49;
A13: b1,a1 // b1',a1'
proof
a1,b1 // a1',b1' by A8, ANALMETR:48;
hence b1,a1 // b1',a1' by ANALMETR:81; :: thesis: verum
end;
A14: b1,a1 // o1,c1
proof
a,b // o,c by A3, A4, A6, A9, AFF_1:41;
then b,a // o,c by AFF_1:13;
hence b1,a1 // o1,c1 by ANALMETR:48; :: thesis: verum
end;
A15: a1,c1 // a1',c1' by A8, ANALMETR:48;
A16: not LIN o,a,c
proof
assume LIN o,a,c ; :: thesis: contradiction
then LIN o,c,a by AFF_1:15;
hence contradiction by A3, A4, A5, A6, AFF_1:39; :: thesis: verum
end;
A17: not LIN o,a,b
proof
assume LIN o,a,b ; :: thesis: contradiction
then A18: LIN a,b,o by AFF_1:15;
set M = Line a,b;
A19: ( a in Line a,b & o in Line a,b ) by A18, AFF_1:26, AFF_1:def 2;
Line a,b // K by A6, A9, AFF_1:def 5;
then a in K by A4, A19, AFF_1:59;
hence contradiction by A3, A4, A16, AFF_1:33; :: thesis: verum
end;
A20: now
assume A21: a' = o ; :: thesis: b,c // b',c'
then A22: b' = o by A7, A8, A17, AFF_1:69;
c' = o by A7, A8, A10, A16, A21, AFF_1:69;
hence b,c // b',c' by A22, AFF_1:12; :: thesis: verum
end;
now
assume A23: a' <> o ; :: thesis: b,c // b',c'
A24: now
assume a = a' ; :: thesis: b,c // b',c'
then A25: ( a,b // a',b & a,c // a',c & LIN o,b,b & LIN o,c,c ) by AFF_1:11, AFF_1:16;
then A26: b = b' by A7, A8, A17, AFF_1:70;
c = c' by A7, A8, A10, A16, A25, AFF_1:70;
hence b,c // b',c' by A26, AFF_1:11; :: thesis: verum
end;
now
assume A27: a <> a' ; :: thesis: b,c // b',c'
A28: ( o1 <> a1' & o1 <> b1' & o1 <> c1' )
proof
thus o1 <> a1' by A23; :: thesis: ( o1 <> b1' & o1 <> c1' )
A29: ( b,a // b',a' & c,a // c',a' ) by A8, AFF_1:13;
( not LIN o,b,a & not LIN o,c,a ) by A16, A17, AFF_1:15;
hence ( o1 <> b1' & o1 <> c1' ) by A7, A10, A23, A29, AFF_1:69; :: thesis: verum
end;
A30: not LIN a1,a1',c1
proof
assume LIN a1,a1',c1 ; :: thesis: contradiction
then A31: LIN a,a',c by ANALMETR:55;
( LIN a,a',o & LIN a,a',a ) by A7, AFF_1:15, AFF_1:16;
hence contradiction by A16, A27, A31, AFF_1:17; :: thesis: verum
end;
not LIN a1,a1',b1
proof
assume LIN a1,a1',b1 ; :: thesis: contradiction
then A32: LIN a,a',b by ANALMETR:55;
( LIN a,a',o & LIN a,a',a ) by A7, AFF_1:15, AFF_1:16;
hence contradiction by A17, A27, A32, AFF_1:17; :: thesis: verum
end;
then b1,c1 // b1',c1' by A2, A11, A12, A13, A14, A15, A28, A30, CONMETR:def 5;
hence b,c // b',c' by ANALMETR:48; :: thesis: verum
end;
hence b,c // b',c' by A24; :: thesis: verum
end;
hence b,c // b',c' by A20; :: 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 A33: 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
A34: ( o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 ) and
A35: ( not LIN b,b1,a & not LIN b,b1,c ) and
A36: ( LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 ) and
A37: ( a,b // a1,b1 & a,b // o,c & 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 MS) by ANALMETR:47;
set K = Line o',c';
A38: ( Line o',c' is being_line & o' in Line o',c' & c' in Line o',c' ) by A34, AFF_1:26, AFF_1:def 3;
LIN o',c',c1' by A36, ANALMETR:55;
then A39: ( c1' in Line o',c' & o' <> c' ) by A34, A38, AFF_1:39;
A40: ( LIN o',a',a1' & LIN o',b',b1' ) by A36, ANALMETR:55;
A41: not b' in Line o',c'
proof
assume A42: b' in Line o',c' ; :: thesis: contradiction
then b1' in Line o',c' by A34, A38, A40, AFF_1:39;
then LIN b',b1',c' by A38, A42, AFF_1:33;
hence contradiction by A35, ANALMETR:55; :: thesis: verum
end;
A43: b',a' // Line o',c' A44: b',a' // b1',a1'
proof
a',b' // a1',b1' by A37, ANALMETR:48;
hence b',a' // b1',a1' by AFF_1:13; :: thesis: verum
end;
A45: b',c' // b1',c1' by A37, ANALMETR:48;
b' <> a' by A35, Th1;
then a',c' // a1',c1' by A33, A38, A39, A40, A41, A43, A44, A45, 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