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

proof

assume o',e1' // a2',e2' ; :: thesis: contradiction
then o,e1 // a2,e2 by ANALMETR:48;
then a2,e2 _|_ o,b by A16, A17, ANALMETR:84;
then a,b // o,b by A18, A19, ANALMETR:85;
then A20: a',b' // o',b' by ANALMETR:48;
then b',a' // b',o' by AFF_1:13;
then A21: LIN b',a',o' by AFF_1:def 1;
o',b' // b',a' by A20, AFF_1:13;
then A22: o,b // b,a by ANALMETR:48;
A23: b' <> a'

proof

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

end;

o,b // o,b1 by A10, ANALMETR:def 11;
then b,a // o,b1 by A4, A22, ANALMETR:82;
then b',a' // o',b1' by ANALMETR:48;
then LIN b',a',b1' by A21, A23, AFF_1:18;
then LIN b',b1',a' by AFF_1:15;
hence contradiction by A7, ANALMETR:55; :: thesis: verum

end;

then consider b2' being Element of such that
A24: LIN o',e1',b2' and
A25: LIN a2',e2',b2' by AFF_1:74;
reconsider b2 = b2' as Element of by ANALMETR:47;
LIN o,e1,b2 by A24, ANALMETR:55;
then o,e1 // o,b2 by ANALMETR:def 11;
then A26: o,b _|_ o,b2 by A16, A17, ANALMETR:84;
LIN a2,e2,b2 by A25, ANALMETR:55;
then a2,e2 // a2,b2 by ANALMETR:def 11;
then A27: a,b _|_ a2,b2 by A18, A19, ANALMETR:84;
consider e1 being Element of such that
A28: o,c _|_ o,e1 and
A29: o <> e1 by ANALMETR:def 10;
consider e2 being Element of such that
A30: a,c _|_ a2,e2 and
A31: a2 <> e2 by ANALMETR:def 10;
reconsider e1' = e1, e2' = e2 as Element of by ANALMETR:47;
not o',e1' // a2',e2'

proof

assume o',e1' // a2',e2' ; :: thesis: contradiction
then o,e1 // a2,e2 by ANALMETR:48;
then o,c _|_ a2,e2 by A28, A29, ANALMETR:84;
then o,c // a,c by A30, A31, ANALMETR:85;
then c,o // c,a by ANALMETR:81;
then LIN c,o,a by ANALMETR:def 11;
then LIN c',o',a' by ANALMETR:55;
then LIN a',c',o' by AFF_1:15;
then LIN a,c,o by ANALMETR:55;
then a,c // a,o by ANALMETR:def 11;
then A32: o,a // a,c by ANALMETR:81;
LIN o',a',a1' by A9, ANALMETR:55;
then LIN a',o',a1' by AFF_1:15;
then LIN a,o,a1 by ANALMETR:55;
then a,o // a,a1 by ANALMETR:def 11;
then o,a // a,a1 by ANALMETR:81;
then a,a1 // a,c by A2, A32, ANALMETR:82;
hence contradiction by A8, ANALMETR:def 11; :: thesis: verum

end;

then consider c2' being Element of such that
A33: LIN o',e1',c2' and
A34: LIN a2',e2',c2' by AFF_1:74;
reconsider c2 = c2' as Element of by ANALMETR:47;
LIN o,e1,c2 by A33, ANALMETR:55;
then o,e1 // o,c2 by ANALMETR:def 11;
then A35: o,c _|_ o,c2 by A28, A29, ANALMETR:84;
LIN a2,e2,c2 by A34, ANALMETR:55;
then a2,e2 // a2,c2 by ANALMETR:def 11;
then A36: a,c _|_ a2,c2 by A30, A31, ANALMETR:84;
A37: not o,c // o,a

proof

assume o,c // o,a ; :: thesis: contradiction
then LIN o,c,a by ANALMETR:def 11;
then LIN o',c',a' by ANALMETR:55;
then LIN a',o',c' by AFF_1:15;
then LIN a,o,c by ANALMETR:55;
then A38: a,o // a,c by ANALMETR:def 11;
LIN o',a',a1' by A9, ANALMETR:55;
then LIN a',o',a1' by AFF_1:15;
then LIN a,o,a1 by ANALMETR:55;
then a,o // a,a1 by ANALMETR:def 11;
then a,a1 // a,c by A2, A38, ANALMETR:82;
hence contradiction by A8, ANALMETR:def 11; :: thesis: verum

end;

not o,a // o,b

proof

assume o,a // o,b ; :: thesis: contradiction
then LIN o,a,b by ANALMETR:def 11;
then LIN o',a',b' by ANALMETR:55;
then LIN b',o',a' by AFF_1:15;
then LIN b,o,a by ANALMETR:55;
then A39: b,o // b,a by ANALMETR:def 11;
LIN o',b',b1' by A10, 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,a by A4, A39, ANALMETR:82;
hence contradiction by A7, ANALMETR:def 11; :: thesis: verum

end;

then A40: b,c _|_ b2,c2 by A1, A14, A26, A27, A35, A36, A37, Def4;
o,a // o,a1 by A9, ANALMETR:def 11;
then A41: o,a1 _|_ o,a2 by A2, A14, ANALMETR:84;
o,b // o,b1 by A10, ANALMETR:def 11;
then A42: o,b1 _|_ o,b2 by A4, A26, ANALMETR:84;
o,c // o,c1 by A11, ANALMETR:def 11;
then A43: o,c1 _|_ o,c2 by A6, A35, ANALMETR:84;
a <> b

proof

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

end;

then A44: a1,b1 _|_ a2,b2 by A12, A27, ANALMETR:84;
a <> c

proof

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

end;

then A45: a1,c1 _|_ a2,c2 by A13, A36, ANALMETR:84;
A46: not o,c1 // o,a1

proof

assume o,c1 // o,a1 ; :: thesis: contradiction
then LIN o,c1,a1 by ANALMETR:def 11;
then LIN o',c1',a1' by ANALMETR:55;
then LIN a1',o',c1' by AFF_1:15;
then LIN a1,o,c1 by ANALMETR:55;
then A47: a1,o // a1,c1 by ANALMETR:def 11;
A48: a1 <> c1

proof

assume a1 = c1 ; :: thesis: contradiction
then LIN o',c',a1' by A11, ANALMETR:55;
then LIN a1',c',o' by AFF_1:15;
then LIN a1,c,o by ANALMETR:55;
then A49: a1,c // a1,o by ANALMETR:def 11;
LIN o',a',a1' by A9, ANALMETR:55;
then LIN a1',o',a' by AFF_1:15;
then LIN a1,o,a by ANALMETR:55;
then a1,o // a1,a by ANALMETR:def 11;
then a1,c // a1,a by A3, A49, ANALMETR:82;
then LIN a1,c,a by ANALMETR:def 11;
then LIN a1',c',a' by ANALMETR:55;
then LIN a',a1',c' by AFF_1:15;
hence contradiction by A8, ANALMETR:55; :: thesis: verum

end;

LIN o',a',a1' by A9, ANALMETR:55;
then LIN a1',o',a' by AFF_1:15;
then LIN a1,o,a by ANALMETR:55;
then a1,o // a1,a by ANALMETR:def 11;
then a1,c1 // a1,a by A3, A47, ANALMETR:82;
then a1,a // a,c by A13, A48, ANALMETR:82;
then a,a1 // a,c by ANALMETR:81;
hence contradiction by A8, ANALMETR:def 11; :: thesis: verum

end;

not o,a1 // o,b1

proof

assume o,a1 // o,b1 ; :: thesis: contradiction
then LIN o,a1,b1 by ANALMETR:def 11;
then LIN o',a1',b1' by ANALMETR:55;
then LIN b1',a1',o' by AFF_1:15;
then LIN b1,a1,o by ANALMETR:55;
then A50: b1,a1 // b1,o by ANALMETR:def 11;
A51: a1 <> b1

proof

assume a1 = b1 ; :: thesis: contradiction
then LIN o',a',b1' by A9, ANALMETR:55;
then LIN b1',o',a' by AFF_1:15;
then LIN b1,o,a by ANALMETR:55;
then A52: b1,o // b1,a by ANALMETR:def 11;
LIN o',b',b1' by A10, ANALMETR:55;
then LIN b1',b',o' by AFF_1:15;
then LIN b1,b,o by ANALMETR:55;
then b1,b // b1,o by ANALMETR:def 11;
then b1,a // b1,b by A5, A52, ANALMETR:82;
then LIN b1,a,b by ANALMETR:def 11;
then LIN b1',a',b' by ANALMETR:55;
then LIN b',b1',a' by AFF_1:15;
hence contradiction by A7, ANALMETR:55; :: thesis: verum

end;

A53: b1,a1 // a,b by A12, ANALMETR:81;
LIN o',b',b1' by A10, ANALMETR:55;
then LIN b1',b',o' by AFF_1:15;
then LIN b1,b,o by ANALMETR:55;
then b1,b // b1,o by ANALMETR:def 11;
then b1,a1 // b1,b by A5, A50, ANALMETR:82;
then b1,b // a,b by A51, A53, ANALMETR:82;
then b,b1 // b,a by ANALMETR:81;
hence contradiction by A7, ANALMETR:def 11; :: thesis: verum

end;

then A54: b1,c1 _|_ b2,c2 by A1, A41, A42, A43, A44, A45, A46, Def4;

A55: now

assume A56: not LIN o,b,c ; :: thesis: b,c // b1,c1
b2 <> c2

proof

assume A57: b2 = c2 ; :: thesis: contradiction
o <> b2

proof

assume A58: o = b2 ; :: thesis: contradiction
a2,o _|_ a,o by A14, ANALMETR:83;
then a,o // a,b by A15, A27, A58, ANALMETR:85;
then LIN a,o,b by ANALMETR:def 11;
then LIN a',o',b' by ANALMETR:55;
then LIN b',o',a' by AFF_1:15;
then LIN b,o,a by ANALMETR:55;
then A59: b,o // b,a by ANALMETR:def 11;
LIN o',b',b1' by A10, 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,a by A4, A59, ANALMETR:82;
hence contradiction by A7, ANALMETR:def 11; :: thesis: verum

end;

then o,b // o,c by A26, A35, A57, ANALMETR:85;
hence contradiction by A56, ANALMETR:def 11; :: thesis: verum

end;

hence b,c // b1,c1 by A40, A54, ANALMETR:85; :: thesis: verum

end;

now

assume A60: LIN o,b,c ; :: thesis: b,c // b1,c1
then LIN o',b',c' by ANALMETR:55;
then LIN b',o',c' by AFF_1:15;
then A61: b',o' // b',c' by AFF_1:def 1;
LIN o',b',b1' by A10, ANALMETR:55;
then LIN b',o',b1' by AFF_1:15;
then b',o' // b',b1' by AFF_1:def 1;
then b',c' // b',b1' by A4, A61, AFF_1:14;
then A62: LIN b',c',b1' by AFF_1:def 1;
LIN o',b',c' by A60, ANALMETR:55;
then LIN c',o',b' by AFF_1:15;
then A63: c',o' // c',b' by AFF_1:def 1;
LIN o',c',c1' by A11, ANALMETR:55;
then LIN c',o',c1' by AFF_1:15;
then c',o' // c',c1' by AFF_1:def 1;
then c',b' // c',c1' by A6, A63, AFF_1:14;
then LIN c',b',c1' by AFF_1:def 1;
then LIN b',c',c1' by AFF_1:15;
then b',c' // b1',c1' by A62, AFF_1:19;
hence b,c // b1,c1 by ANALMETR:48; :: thesis: verum

end;

hence b,c // b1,c1 by A55; :: thesis: verum