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 X; :: according to CONMETR:def 5 :: thesis: for a, a1, b, b1, c, c1 being Element of X 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 X; :: 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 A2: ( 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 ) ; :: thesis: a,c // a1,c1
consider c2 being Element of X such that
A3: ( o,c _|_ o,c2 & o <> c2 ) by ANALMETR:def 10;
consider e1 being Element of X such that
A4: ( o,b _|_ o,e1 & o <> e1 ) by ANALMETR:def 10;
consider e2 being Element of X such that
A5: ( b,c _|_ c2,e2 & 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 (Af X) by ANALMETR:47;
A6: b1 <> a1

proof

assume b1 = a1 ; :: thesis: contradiction
then LIN o',b',a1' by A2, ANALMETR:55;
then o',b' // o',a1' by AFF_1:def 1;
then o',a1' // o',b' by AFF_1:13;
then A7: o,a1 // o,b by ANALMETR:48;
o,a // o,a1 by A2, 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 A2, A7, ANALMETR:82;
then LIN o,a,b by ANALMETR:def 11;
then A8: LIN o',a',b' by ANALMETR:55;
then A9: LIN a',b',o' by AFF_1:15;
LIN b',o',a' by A8, AFF_1:15;
then b',o' // b',a' by AFF_1:def 1;
then o',b' // a',b' by AFF_1:13;
then A10: o,b // a,b by ANALMETR:48;
o,b // o,b1 by A2, ANALMETR:def 11;
then a,b // o,b1 by A2, A10, ANALMETR:82;
then A11: a',b' // o',b1' by ANALMETR:48;
a' <> b'

proof

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

end;

then LIN a',b',b1' by A9, A11, AFF_1:18;
then LIN b',b1',a' by AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

A12: now

assume A13: not LIN a,b,c ; :: thesis: a,c // a1,c1
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 A4, ANALMETR:84;
then c2,e2 _|_ b,o by ANALMETR:83;
then b,c // b,o by A5, 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 A14: b,o // b,c by ANALMETR:def 11;
LIN o',b',b1' by A2, 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 A2, A14, ANALMETR:82;
hence contradiction by A2, ANALMETR:def 11; :: thesis: verum

end;

then consider b2' being Element of (Af X) such that
A15: ( LIN o',e1',b2' & LIN c2',e2',b2' ) by AFF_1:74;
reconsider b2 = b2' as Element of X by ANALMETR:47;
LIN o,e1,b2 by A15, ANALMETR:55;
then o,e1 // o,b2 by ANALMETR:def 11;
then A16: o,b _|_ o,b2 by A4, ANALMETR:84;
LIN c2,e2,b2 by A15, ANALMETR:55;
then c2,e2 // c2,b2 by ANALMETR:def 11;
then A17: b,c _|_ c2,b2 by A5, ANALMETR:84;
consider e1 being Element of X such that
A18: ( o,a _|_ o,e1 & o <> e1 ) by ANALMETR:def 10;
consider e2 being Element of X such that
A19: ( a,c _|_ c2,e2 & c2 <> e2 ) by ANALMETR:def 10;
reconsider e1' = e1, e2' = e2 as Element of (Af X) 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 A18, ANALMETR:84;
then a,c // o,a by A19, 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 A20: c,o // c,a by ANALMETR:def 11;
a',b' // o',c' by A2, 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 A2, A20, 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 A13, ANALMETR:def 11; :: thesis: verum

end;

then consider a2' being Element of (Af X) such that
A21: ( LIN o',e1',a2' & LIN c2',e2',a2' ) by AFF_1:74;
reconsider a2 = a2' as Element of X by ANALMETR:47;
LIN o,e1,a2 by A21, ANALMETR:55;
then o,e1 // o,a2 by ANALMETR:def 11;
then A22: o,a _|_ o,a2 by A18, ANALMETR:84;
LIN c2,e2,a2 by A21, ANALMETR:55;
then c2,e2 // c2,a2 by ANALMETR:def 11;
then A23: a,c _|_ c2,a2 by A19, ANALMETR:84;
A24: c,b _|_ c2,b2 by A17, ANALMETR:83;
a',b' // o',c' by A2, ANALMETR:48;
then o',c' // b',a' by AFF_1:13;
then A25: o,c // b,a by ANALMETR:48;
A26: c,a _|_ c2,a2 by A23, ANALMETR:83;
A27: 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 A28: c,o // c,a by ANALMETR:def 11;
a',b' // o',c' by A2, 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 A2, A28, 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 A13, ANALMETR:def 11; :: thesis: verum

end;

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 A29: o,c // b,c by ANALMETR:48;
a',b' // o',c' by A2, 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 A2, A29, 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 A13, ANALMETR:55; :: thesis: verum

end;

then A30: b,a _|_ b2,a2 by A1, A3, A16, A22, A24, A25, A26, A27, CONAFFM:def 2;
consider e1 being Element of X such that
A31: ( o,a1 _|_ o,e1 & o <> e1 ) by ANALMETR:def 10;
consider e2 being Element of X such that
A32: ( a1,c1 _|_ c2,e2 & c2 <> e2 ) by ANALMETR:def 10;
reconsider e1' = e1, e2' = e2 as Element of (Af X) 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 A31, ANALMETR:84;
then a1,c1 // o,a1 by A32, 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 A33: o,c1 // o,a1 by ANALMETR:48;
LIN o',c',c1' by A2, 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 A34: o,a1 // o,c by A2, A33, ANALMETR:82;
LIN o',a',a1' by A2, ANALMETR:55;
then o',a' // o',a1' by AFF_1:def 1;
then o',a1' // o',a' by AFF_1:13;
then o,a1 // o,a by ANALMETR:48;
then o,a // o,c by A2, A34, 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 A2, ANALMETR:82;
hence contradiction by A13, ANALMETR:def 11; :: thesis: verum

end;

then consider a3' being Element of (Af X) such that
A35: ( LIN o',e1',a3' & LIN c2',e2',a3' ) by AFF_1:74;
reconsider a3 = a3' as Element of X by ANALMETR:47;
A36: o,a1 _|_ o,a3

proof

LIN o,e1,a3 by A35, ANALMETR:55;
then o,e1 // o,a3 by ANALMETR:def 11;
hence o,a1 _|_ o,a3 by A31, ANALMETR:84; :: thesis: verum

end;

A37: a1,c1 _|_ c2,a3

proof

LIN c2,e2,a3 by A35, ANALMETR:55;
then c2,e2 // c2,a3 by ANALMETR:def 11;
hence a1,c1 _|_ c2,a3 by A32, ANALMETR:84; :: thesis: verum

end;

A38: o,c1 _|_ o,c2

proof

o,c // o,c1 by A2, ANALMETR:def 11;
hence o,c1 _|_ o,c2 by A2, A3, ANALMETR:84; :: thesis: verum

end;

A39: o,b1 _|_ o,b2

proof

o,b // o,b1 by A2, ANALMETR:def 11;
hence o,b1 _|_ o,b2 by A2, A16, ANALMETR:84; :: thesis: verum

end;

A40: c1,b1 _|_ c2,b2

proof

b <> c

proof

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

end;

then c2,b2 _|_ b1,c1 by A2, A17, ANALMETR:84;
hence c1,b1 _|_ c2,b2 by ANALMETR:83; :: thesis: verum

end;

A41: o,c1 // b1,a1

proof

a <> b

proof

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

end;

then o,c // a1,b1 by A2, ANALMETR:82;
then o',c' // a1',b1' by ANALMETR:48;
then o',c' // b1',a1' by AFF_1:13;
then A42: o,c // b1,a1 by ANALMETR:48;
o,c // o,c1 by A2, ANALMETR:def 11;
hence o,c1 // b1,a1 by A2, A42, ANALMETR:82; :: thesis: verum

end;

A43: c1,a1 _|_ c2,a3 by A37, ANALMETR:83;
A44: not o,a1 // o,c1

proof

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 A45: o,c1 // o,a1 by ANALMETR:48;
o,c // o,c1 by A2, 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 A46: o,a1 // o,c by A2, A45, ANALMETR:82;
o,a // o,a1 by A2, 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,c by A2, A46, 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 A2, ANALMETR:82;
hence contradiction by A13, ANALMETR:def 11; :: thesis: verum

end;

not o,c1 // o,b1

proof

assume A47: o,c1 // o,b1 ; :: thesis: contradiction
( o,c // o,c1 & o,b // o,b1 ) by A2, ANALMETR:def 11;
then ( o',c' // o',c1' & o',b' // o',b1' ) by ANALMETR:48;
then ( o',c1' // o',c' & o',b1' // o',b' ) by AFF_1:13;
then A48: ( o,c1 // o,c & o,b1 // o,b ) by ANALMETR:48;
then o,b1 // o,c by A2, A47, ANALMETR:82;
then o,b // o,c by A2, A48, 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 A49: o,c // b,c by ANALMETR:48;
a',b' // o',c' by A2, 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 A2, A49, 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 A13, ANALMETR:55; :: thesis: verum

end;

then A50: b1,a1 _|_ b2,a3 by A1, A36, A38, A39, A40, A41, A43, A44, CONAFFM:def 2;
A51: b2,a3 // b2,a2

proof

A52: b <> a

proof

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

end;

b2,a2 _|_ a,b by A30, ANALMETR:83;
then b2,a2 _|_ a1,b1 by A2, A52, ANALMETR:84;
then b1,a1 _|_ b2,a2 by ANALMETR:83;
hence b2,a3 // b2,a2 by A6, A50, ANALMETR:85; :: thesis: verum

end;

A53: not LIN o',b2',a2'

proof

assume LIN o',b2',a2' ; :: thesis: contradiction
then LIN o,b2,a2 by ANALMETR:55;
then A54: o,b2 // o,a2 by ANALMETR:def 11;
o <> b2

proof

assume o = b2 ; :: thesis: contradiction
then o,c2 _|_ b,c by A17, ANALMETR:83;
then A55: o,c // b,c by A3, ANALMETR:85;
a',b' // o',c' by A2, 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 A2, A55, 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 A13, ANALMETR:55; :: thesis: verum

end;

then A56: o,a2 _|_ o,b by A16, A54, ANALMETR:84;
o <> a2

proof

assume A57: o = a2 ; :: thesis: contradiction
c2,o _|_ o,c by A3, ANALMETR:83;
then o,c // c,a by A3, A26, A57, ANALMETR:85;
then a,b // c,a by A2, 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 A13, ANALMETR:def 11; :: thesis: verum

end;

then o,a // o,b by A22, A56, ANALMETR:85;
then LIN o,a,b by ANALMETR:def 11;
then LIN o',a',b' by ANALMETR:55;
then A58: LIN a',b',o' by AFF_1:15;
A59: a' <> b'

proof

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

end;

a',b' // o',c' by A2, ANALMETR:48;
then LIN a',b',c' by A58, A59, AFF_1:18;
hence contradiction by A13, ANALMETR:55; :: thesis: verum

end;

A60: LIN o',a2',a3'

proof

o,a // o,a1 by A2, ANALMETR:def 11;
then o,a1 _|_ o,a2 by A2, A22, ANALMETR:84;
then o,a2 // o,a3 by A2, A36, ANALMETR:85;
then LIN o,a2,a3 by ANALMETR:def 11;
hence LIN o',a2',a3' by ANALMETR:55; :: thesis: verum

end;

b2',a2' // b2',a3'

proof

b2',a3' // b2',a2' by A51, ANALMETR:48;
hence b2',a2' // b2',a3' by AFF_1:13; :: thesis: verum

end;

then A61: a2' = a3' by A53, A60, AFF_1:23;
a,c // a1,c1

proof

c2 <> a2

proof

assume c2 = a2 ; :: thesis: contradiction
then o,c // o,a by A3, A22, 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 A2, ANALMETR:82;
hence contradiction by A13, ANALMETR:def 11; :: thesis: verum

end;

then c,a // a1,c1 by A26, A37, A61, 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;

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

end;

now

assume A62: LIN a,b,c ; :: thesis: a,c // a1,c1
then A63: LIN a',b',c' by ANALMETR:55;
then LIN b',a',c' by AFF_1:15;
then b',a' // b',c' by AFF_1:def 1;
then a',b' // b',c' by AFF_1:13;
then A64: a,b // b,c by ANALMETR:48;
A65: a <> b

proof

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

end;

A66: b <> c

proof

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

end;

b,c // a1,b1 by A2, A64, A65, ANALMETR:82;
then b1,c1 // a1,b1 by A2, A66, 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 A67: a1,b1 // a1,c1 by ANALMETR:def 11;
a',b' // a1',b1' by A2, ANALMETR:48;
then a1',b1' // a',b' by AFF_1:13;
then A68: a1,b1 // a,b by ANALMETR:48;

A69: 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 A70: a,b // a1,c1 by ANALMETR:48;
a,b // a,c by A62, ANALMETR:def 11;
hence a,c // a1,c1 by A65, A70, ANALMETR:82; :: thesis: verum

end;

now

assume A71: a1 = b1 ; :: thesis: a,c // a1,c1
LIN c',b',a' by A63, AFF_1:15;
then c',b' // c',a' by AFF_1:def 1;
then b',c' // a',c' by AFF_1:13;
then b,c // a,c by ANALMETR:48;
hence a,c // a1,c1 by A2, A66, A71, ANALMETR:82; :: thesis: verum

end;

hence a,c // a1,c1 by A67, A68, A69, ANALMETR:82; :: thesis: verum

end;

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