let X be OrtAfPl; :: thesis: ( X is satisfying_AH implies X is satisfying_TDES )
assume A1: X is satisfying_AH ; :: thesis: X is satisfying_TDES
let o be Element of ; :: according to CONMETR:def 5 :: thesis: for a, a1, b, b1, c, c1 being Element of st 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 holds
a,c // a1,c1
let a, a1, b, b1, c, c1 be Element of ; :: 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
A2: o <> a and
A3: o <> a1 and
A4: o <> b and
A5: o <> b1 and
A6: o <> c and
A7: o <> c1 and
A8: not LIN b,b1,a and
A9: not LIN b,b1,c and
A10: LIN o,a,a1 and
A11: LIN o,b,b1 and
A12: LIN o,c,c1 and
A13: a,b // a1,b1 and
A14: a,b // o,c and
A15: b,c // b1,c1 ; :: thesis: a,c // a1,c1
consider e1 being Element of such that
A16: o,b _|_ o,e1 and
A17: o <> e1 by ANALMETR:def 10;
consider c2 being Element of such that
A18: o,c _|_ o,c2 and
A19: o <> c2 by ANALMETR:def 10;
consider e2 being Element of such that
A20: b,c _|_ c2,e2 and
A21: c2 <> e2 by ANALMETR:def 10;
reconsider o' = o, a' = a, a1' = a1, b' = b, b1' = b1, c' = c, c1' = c1, c2' = c2, e1' = e1, e2' = e2 as Element of by ANALMETR:47;
A22: b1 <> a1

proof

assume b1 = a1 ; :: thesis: contradiction
then LIN o',b',a1' by A11, ANALMETR:55;
then o',b' // o',a1' by AFF_1:def 1;
then o',a1' // o',b' by AFF_1:13;
then A23: o,a1 // o,b by ANALMETR:48;
o,a // o,a1 by A10, ANALMETR:def 11;
then o',a' // o',a1' by ANALMETR:48;
then o',a1' // o',a' by AFF_1:13;
then o,a1 // o,a by ANALMETR:48;
then o,a // o,b by A3, A23, ANALMETR:82;
then LIN o,a,b by ANALMETR:def 11;
then A24: LIN o',a',b' by ANALMETR:55;
then LIN b',o',a' by AFF_1:15;
then b',o' // b',a' by AFF_1:def 1;
then o',b' // a',b' by AFF_1:13;
then A25: o,b // a,b by ANALMETR:48;
A26: a' <> b'

proof

assume a' = b' ; :: thesis: contradiction
then LIN b',b1',a' by AFF_1:16;
hence contradiction by A8, ANALMETR:55; :: thesis: verum

end;

o,b // o,b1 by A11, ANALMETR:def 11;
then a,b // o,b1 by A4, A25, ANALMETR:82;
then A27: a',b' // o',b1' by ANALMETR:48;
LIN a',b',o' by A24, AFF_1:15;
then LIN a',b',b1' by A27, A26, AFF_1:18;
then LIN b',b1',a' by AFF_1:15;
hence contradiction by A8, ANALMETR:55; :: thesis: verum

end;

A28: now

not o',e1' // c2',e2'

proof

assume o',e1' // c2',e2' ; :: thesis: contradiction
then o,e1 // c2,e2 by ANALMETR:48;
then c2,e2 _|_ o,b by A16, A17, ANALMETR:84;
then c2,e2 _|_ b,o by ANALMETR:83;
then b,c // b,o by A20, A21, ANALMETR:85;
then LIN b,c,o by ANALMETR:def 11;
then LIN b',c',o' by ANALMETR:55;
then LIN b',o',c' by AFF_1:15;
then LIN b,o,c by ANALMETR:55;
then A29: b,o // b,c by ANALMETR:def 11;
LIN o',b',b1' by A11, ANALMETR:55;
then LIN b',o',b1' by AFF_1:15;
then LIN b,o,b1 by ANALMETR:55;
then b,o // b,b1 by ANALMETR:def 11;
then b,b1 // b,c by A4, A29, ANALMETR:82;
hence contradiction by A9, ANALMETR:def 11; :: thesis: verum

end;

then consider b2' being Element of such that
A30: LIN o',e1',b2' and
A31: LIN c2',e2',b2' by AFF_1:74;
reconsider b2 = b2' as Element of by ANALMETR:47;
LIN o,e1,b2 by A30, ANALMETR:55;
then o,e1 // o,b2 by ANALMETR:def 11;
then A32: o,b _|_ o,b2 by A16, A17, ANALMETR:84;
o,b // o,b1 by A11, ANALMETR:def 11;
then A33: o,b1 _|_ o,b2 by A4, A32, ANALMETR:84;
assume A34: not LIN a,b,c ; :: thesis: a,c // a1,c1
A35: b <> a

proof

assume b = a ; :: thesis: contradiction
then LIN a',b',c' by AFF_1:16;
hence contradiction by A34, ANALMETR:55; :: thesis: verum

end;

A36: not o,c // o,b

proof

assume o,c // o,b ; :: thesis: contradiction
then LIN o,c,b by ANALMETR:def 11;
then LIN o',c',b' by ANALMETR:55;
then LIN c',o',b' by AFF_1:15;
then c',o' // c',b' by AFF_1:def 1;
then o',c' // b',c' by AFF_1:13;
then A37: o,c // b,c by ANALMETR:48;
a',b' // o',c' by A14, ANALMETR:48;
then o',c' // b',a' by AFF_1:13;
then o,c // b,a by ANALMETR:48;
then b,a // b,c by A6, A37, ANALMETR:82;
then LIN b,a,c by ANALMETR:def 11;
then LIN b',a',c' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A34, ANALMETR:55; :: thesis: verum

end;

A38: not o,a // o,c

proof

assume o,a // o,c ; :: thesis: contradiction
then LIN o,a,c by ANALMETR:def 11;
then LIN o',a',c' by ANALMETR:55;
then LIN c',o',a' by AFF_1:15;
then LIN c,o,a by ANALMETR:55;
then A39: c,o // c,a by ANALMETR:def 11;
a',b' // o',c' by A14, ANALMETR:48;
then c',o' // a',b' by AFF_1:13;
then c,o // a,b by ANALMETR:48;
then a,b // c,a by A6, A39, ANALMETR:82;
then a',b' // c',a' by ANALMETR:48;
then a',b' // a',c' by AFF_1:13;
then a,b // a,c by ANALMETR:48;
hence contradiction by A34, ANALMETR:def 11; :: thesis: verum

end;

LIN c2,e2,b2 by A31, ANALMETR:55;
then c2,e2 // c2,b2 by ANALMETR:def 11;
then A40: b,c _|_ c2,b2 by A20, A21, ANALMETR:84;
consider e1 being Element of such that
A41: o,a _|_ o,e1 and
A42: o <> e1 by ANALMETR:def 10;
consider e2 being Element of such that
A43: a,c _|_ c2,e2 and
A44: c2 <> e2 by ANALMETR:def 10;
reconsider e1' = e1, e2' = e2 as Element of by ANALMETR:47;
not o',e1' // c2',e2'

proof

assume o',e1' // c2',e2' ; :: thesis: contradiction
then o,e1 // c2,e2 by ANALMETR:48;
then c2,e2 _|_ o,a by A41, A42, ANALMETR:84;
then a,c // o,a by A43, A44, ANALMETR:85;
then a',c' // o',a' by ANALMETR:48;
then a',c' // a',o' by AFF_1:13;
then LIN a',c',o' by AFF_1:def 1;
then LIN c',o',a' by AFF_1:15;
then LIN c,o,a by ANALMETR:55;
then A45: c,o // c,a by ANALMETR:def 11;
a',b' // o',c' by A14, ANALMETR:48;
then c',o' // a',b' by AFF_1:13;
then c,o // a,b by ANALMETR:48;
then a,b // c,a by A6, A45, ANALMETR:82;
then a',b' // c',a' by ANALMETR:48;
then a',b' // a',c' by AFF_1:13;
then a,b // a,c by ANALMETR:48;
hence contradiction by A34, ANALMETR:def 11; :: thesis: verum

end;

then consider a2' being Element of such that
A46: LIN o',e1',a2' and
A47: LIN c2',e2',a2' by AFF_1:74;
reconsider a2 = a2' as Element of by ANALMETR:47;
LIN o,e1,a2 by A46, ANALMETR:55;
then o,e1 // o,a2 by ANALMETR:def 11;
then A48: o,a _|_ o,a2 by A41, A42, ANALMETR:84;
A49: c2 <> a2

proof

assume c2 = a2 ; :: thesis: contradiction
then o,c // o,a by A18, A19, A48, ANALMETR:85;
then LIN o,c,a by ANALMETR:def 11;
then LIN o',c',a' by ANALMETR:55;
then LIN c',a',o' by AFF_1:15;
then c',a' // c',o' by AFF_1:def 1;
then o',c' // a',c' by AFF_1:13;
then o,c // a,c by ANALMETR:48;
then a,b // a,c by A6, A14, ANALMETR:82;
hence contradiction by A34, ANALMETR:def 11; :: thesis: verum

end;

LIN c2,e2,a2 by A47, ANALMETR:55;
then c2,e2 // c2,a2 by ANALMETR:def 11;
then a,c _|_ c2,a2 by A43, A44, ANALMETR:84;
then A50: c,a _|_ c2,a2 by ANALMETR:83;
A51: not LIN o',b2',a2'

proof

A52: o <> b2

proof

a',b' // o',c' by A14, ANALMETR:48;
then o',c' // b',a' by AFF_1:13;
then A53: o,c // b,a by ANALMETR:48;
assume o = b2 ; :: thesis: contradiction
then o,c2 _|_ b,c by A40, ANALMETR:83;
then o,c // b,c by A18, A19, ANALMETR:85;
then b,a // b,c by A6, A53, ANALMETR:82;
then LIN b,a,c by ANALMETR:def 11;
then LIN b',a',c' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A34, ANALMETR:55; :: thesis: verum

end;

A54: o <> a2

proof

assume A55: o = a2 ; :: thesis: contradiction
c2,o _|_ o,c by A18, ANALMETR:83;
then o,c // c,a by A19, A50, A55, ANALMETR:85;
then a,b // c,a by A6, A14, ANALMETR:82;
then a',b' // c',a' by ANALMETR:48;
then a',b' // a',c' by AFF_1:13;
then a,b // a,c by ANALMETR:48;
hence contradiction by A34, ANALMETR:def 11; :: thesis: verum

end;

assume LIN o',b2',a2' ; :: thesis: contradiction
then LIN o,b2,a2 by ANALMETR:55;
then o,b2 // o,a2 by ANALMETR:def 11;
then o,a2 _|_ o,b by A32, A52, ANALMETR:84;
then o,a // o,b by A48, A54, ANALMETR:85;
then LIN o,a,b by ANALMETR:def 11;
then LIN o',a',b' by ANALMETR:55;
then A56: LIN a',b',o' by AFF_1:15;
A57: a' <> b'

proof

assume a' = b' ; :: thesis: contradiction
then LIN a',b',c' by AFF_1:16;
hence contradiction by A34, ANALMETR:55; :: thesis: verum

end;

a',b' // o',c' by A14, ANALMETR:48;
then LIN a',b',c' by A56, A57, AFF_1:18;
hence contradiction by A34, ANALMETR:55; :: thesis: verum

end;

consider e1 being Element of such that
A58: o,a1 _|_ o,e1 and
A59: o <> e1 by ANALMETR:def 10;
consider e2 being Element of such that
A60: a1,c1 _|_ c2,e2 and
A61: c2 <> e2 by ANALMETR:def 10;
reconsider e1' = e1, e2' = e2 as Element of by ANALMETR:47;
not o',e1' // c2',e2'

proof

assume o',e1' // c2',e2' ; :: thesis: contradiction
then o,e1 // c2,e2 by ANALMETR:48;
then c2,e2 _|_ o,a1 by A58, A59, ANALMETR:84;
then a1,c1 // o,a1 by A60, A61, ANALMETR:85;
then a1',c1' // o',a1' by ANALMETR:48;
then a1',c1' // a1',o' by AFF_1:13;
then LIN a1',c1',o' by AFF_1:def 1;
then LIN o',c1',a1' by AFF_1:15;
then o',c1' // o',a1' by AFF_1:def 1;
then A62: o,c1 // o,a1 by ANALMETR:48;
LIN o',a',a1' by A10, ANALMETR:55;
then o',a' // o',a1' by AFF_1:def 1;
then o',a1' // o',a' by AFF_1:13;
then A63: o,a1 // o,a by ANALMETR:48;
LIN o',c',c1' by A12, ANALMETR:55;
then o',c' // o',c1' by AFF_1:def 1;
then o',c1' // o',c' by AFF_1:13;
then o,c1 // o,c by ANALMETR:48;
then o,a1 // o,c by A7, A62, ANALMETR:82;
then o,a // o,c by A3, A63, ANALMETR:82;
then LIN o,a,c by ANALMETR:def 11;
then LIN o',a',c' by ANALMETR:55;
then LIN c',o',a' by AFF_1:15;
then c',o' // c',a' by AFF_1:def 1;
then o',c' // a',c' by AFF_1:13;
then o,c // a,c by ANALMETR:48;
then a,b // a,c by A6, A14, ANALMETR:82;
hence contradiction by A34, ANALMETR:def 11; :: thesis: verum

end;

then consider a3' being Element of such that
A64: LIN o',e1',a3' and
A65: LIN c2',e2',a3' by AFF_1:74;
reconsider a3 = a3' as Element of by ANALMETR:47;
LIN o,e1,a3 by A64, ANALMETR:55;
then o,e1 // o,a3 by ANALMETR:def 11;
then A66: o,a1 _|_ o,a3 by A58, A59, ANALMETR:84;
b <> c

proof

assume b = c ; :: thesis: contradiction
then LIN a',b',c' by AFF_1:16;
hence contradiction by A34, ANALMETR:55; :: thesis: verum

end;

then c2,b2 _|_ b1,c1 by A15, A40, ANALMETR:84;
then A67: c1,b1 _|_ c2,b2 by ANALMETR:83;
A68: not o,a1 // o,c1

proof

o,a // o,a1 by A10, ANALMETR:def 11;
then o',a' // o',a1' by ANALMETR:48;
then o',a1' // o',a' by AFF_1:13;
then A69: o,a1 // o,a by ANALMETR:48;
assume o,a1 // o,c1 ; :: thesis: contradiction
then o',a1' // o',c1' by ANALMETR:48;
then o',c1' // o',a1' by AFF_1:13;
then A70: o,c1 // o,a1 by ANALMETR:48;
o,c // o,c1 by A12, ANALMETR:def 11;
then o',c' // o',c1' by ANALMETR:48;
then o',c1' // o',c' by AFF_1:13;
then o,c1 // o,c by ANALMETR:48;
then o,a1 // o,c by A7, A70, ANALMETR:82;
then o,a // o,c by A3, A69, ANALMETR:82;
then LIN o,a,c by ANALMETR:def 11;
then LIN o',a',c' by ANALMETR:55;
then LIN c',a',o' by AFF_1:15;
then c',a' // c',o' by AFF_1:def 1;
then o',c' // a',c' by AFF_1:13;
then o,c // a,c by ANALMETR:48;
then a,b // a,c by A6, A14, ANALMETR:82;
hence contradiction by A34, ANALMETR:def 11; :: thesis: verum

end;

a',b' // o',c' by A14, ANALMETR:48;
then o',c' // b',a' by AFF_1:13;
then A71: o,c // b,a by ANALMETR:48;
A72: not o,c1 // o,b1

proof

o,b // o,b1 by A11, ANALMETR:def 11;
then o',b' // o',b1' by ANALMETR:48;
then o',b1' // o',b' by AFF_1:13;
then A73: o,b1 // o,b by ANALMETR:48;
o,c // o,c1 by A12, ANALMETR:def 11;
then o',c' // o',c1' by ANALMETR:48;
then o',c1' // o',c' by AFF_1:13;
then A74: o,c1 // o,c by ANALMETR:48;
assume o,c1 // o,b1 ; :: thesis: contradiction
then o,b1 // o,c by A7, A74, ANALMETR:82;
then o,b // o,c by A5, A73, ANALMETR:82;
then LIN o,b,c by ANALMETR:def 11;
then LIN o',b',c' by ANALMETR:55;
then LIN c',o',b' by AFF_1:15;
then c',o' // c',b' by AFF_1:def 1;
then o',c' // b',c' by AFF_1:13;
then A75: o,c // b,c by ANALMETR:48;
a',b' // o',c' by A14, ANALMETR:48;
then o',c' // b',a' by AFF_1:13;
then o,c // b,a by ANALMETR:48;
then b,a // b,c by A6, A75, ANALMETR:82;
then LIN b,a,c by ANALMETR:def 11;
then LIN b',a',c' by ANALMETR:55;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A34, ANALMETR:55; :: thesis: verum

end;

a <> b

proof

assume a = b ; :: thesis: contradiction
then LIN b',b1',a' by AFF_1:16;
hence contradiction by A8, ANALMETR:55; :: thesis: verum

end;

then o,c // a1,b1 by A13, A14, ANALMETR:82;
then o',c' // a1',b1' by ANALMETR:48;
then o',c' // b1',a1' by AFF_1:13;
then A76: o,c // b1,a1 by ANALMETR:48;
o,c // o,c1 by A12, ANALMETR:def 11;
then A77: o,c1 // b1,a1 by A6, A76, ANALMETR:82;
o,c // o,c1 by A12, ANALMETR:def 11;
then A78: o,c1 _|_ o,c2 by A6, A18, ANALMETR:84;
c,b _|_ c2,b2 by A40, ANALMETR:83;
then b,a _|_ b2,a2 by A1, A18, A32, A48, A71, A50, A38, A36, CONAFFM:def 2;
then b2,a2 _|_ a,b by ANALMETR:83;
then b2,a2 _|_ a1,b1 by A13, A35, ANALMETR:84;
then A79: b1,a1 _|_ b2,a2 by ANALMETR:83;
o,a // o,a1 by A10, ANALMETR:def 11;
then o,a1 _|_ o,a2 by A2, A48, ANALMETR:84;
then o,a2 // o,a3 by A3, A66, ANALMETR:85;
then LIN o,a2,a3 by ANALMETR:def 11;
then A80: LIN o',a2',a3' by ANALMETR:55;
LIN c2,e2,a3 by A65, ANALMETR:55;
then c2,e2 // c2,a3 by ANALMETR:def 11;
then A81: a1,c1 _|_ c2,a3 by A60, A61, ANALMETR:84;
then c1,a1 _|_ c2,a3 by ANALMETR:83;
then b1,a1 _|_ b2,a3 by A1, A66, A78, A33, A67, A77, A68, A72, CONAFFM:def 2;
then b2,a3 // b2,a2 by A22, A79, ANALMETR:85;
then b2',a3' // b2',a2' by ANALMETR:48;
then b2',a2' // b2',a3' by AFF_1:13;
then a2' = a3' by A51, A80, AFF_1:23;
then c,a // a1,c1 by A50, A81, A49, ANALMETR:85;
then c',a' // a1',c1' by ANALMETR:48;
then a',c' // a1',c1' by AFF_1:13;
hence a,c // a1,c1 by ANALMETR:48; :: thesis: verum

end;

now

assume A82: LIN a,b,c ; :: thesis: a,c // a1,c1
then A83: LIN a',b',c' by ANALMETR:55;
A84: a <> b

proof

assume a = b ; :: thesis: contradiction
then LIN b',b1',a' by AFF_1:16;
hence contradiction by A8, ANALMETR:55; :: thesis: verum

end;

A85: now

assume a1,c1 // a,b ; :: thesis: a,c // a1,c1
then a1',c1' // a',b' by ANALMETR:48;
then a',b' // a1',c1' by AFF_1:13;
then A86: a,b // a1,c1 by ANALMETR:48;
a,b // a,c by A82, ANALMETR:def 11;
hence a,c // a1,c1 by A84, A86, ANALMETR:82; :: thesis: verum

end;

A87: b <> c

proof

assume b = c ; :: thesis: contradiction
then LIN b',b1',c' by AFF_1:16;
hence contradiction by A9, ANALMETR:55; :: thesis: verum

end;

A88: now

LIN c',b',a' by A83, AFF_1:15;
then c',b' // c',a' by AFF_1:def 1;
then b',c' // a',c' by AFF_1:13;
then A89: b,c // a,c by ANALMETR:48;
assume a1 = b1 ; :: thesis: a,c // a1,c1
hence a,c // a1,c1 by A15, A87, A89, ANALMETR:82; :: thesis: verum

end;

LIN b',a',c' by A83, AFF_1:15;
then b',a' // b',c' by AFF_1:def 1;
then a',b' // b',c' by AFF_1:13;
then a,b // b,c by ANALMETR:48;
then b,c // a1,b1 by A13, A84, ANALMETR:82;
then b1,c1 // a1,b1 by A15, A87, ANALMETR:82;
then b1',c1' // a1',b1' by ANALMETR:48;
then b1',a1' // b1',c1' by AFF_1:13;
then LIN b1',a1',c1' by AFF_1:def 1;
then LIN a1',b1',c1' by AFF_1:15;
then LIN a1,b1,c1 by ANALMETR:55;
then A90: a1,b1 // a1,c1 by ANALMETR:def 11;
a',b' // a1',b1' by A13, ANALMETR:48;
then a1',b1' // a',b' by AFF_1:13;
then a1,b1 // a,b by ANALMETR:48;
hence a,c // a1,c1 by A90, A85, A88, ANALMETR:82; :: thesis: verum

end;

hence a,c // a1,c1 by A28; :: thesis: verum