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 X; :: according to CONAFFM:def 1 :: 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 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 X; :: 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 A2: ( 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 ) ; :: thesis: b,c // b1,c1
consider a2 being Element of X such that
A3: ( o,a _|_ o,a2 & o <> a2 ) 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: ( a,b _|_ a2,e2 & 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 (Af X) 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 A4, ANALMETR:84;
then a,b // o,b by A5, ANALMETR:85;
then A6: a',b' // o',b' by ANALMETR:48;
then b',a' // b',o' by AFF_1:13;
then A7: LIN b',a',o' by AFF_1:def 1;
o',b' // b',a' by A6, AFF_1:13;
then A8: o,b // b,a by ANALMETR:48;
A9: b' <> a'
proof
assume b' = a' ; :: thesis: contradiction
then LIN b',b1',a' by AFF_1:16;
hence contradiction by A2, ANALMETR:55; :: thesis: verum
end;
o,b // o,b1 by A2, ANALMETR:def 11;
then b,a // o,b1 by A2, A8, ANALMETR:82;
then b',a' // o',b1' by ANALMETR:48;
then LIN b',a',b1' by A7, A9, AFF_1:18;
then LIN b',b1',a' by AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum
end;
then consider b2' being Element of (Af X) such that
A10: ( LIN o',e1',b2' & LIN a2',e2',b2' ) by AFF_1:74;
reconsider b2 = b2' as Element of X by ANALMETR:47;
A11: o,b _|_ o,b2
proof
LIN o,e1,b2 by A10, ANALMETR:55;
then o,e1 // o,b2 by ANALMETR:def 11;
hence o,b _|_ o,b2 by A4, ANALMETR:84; :: thesis: verum
end;
A12: a,b _|_ a2,b2
proof
LIN a2,e2,b2 by A10, ANALMETR:55;
then a2,e2 // a2,b2 by ANALMETR:def 11;
hence a,b _|_ a2,b2 by A5, ANALMETR:84; :: thesis: verum
end;
consider e1 being Element of X such that
A13: ( o,c _|_ o,e1 & o <> e1 ) by ANALMETR:def 10;
consider e2 being Element of X such that
A14: ( a,c _|_ a2,e2 & a2 <> e2 ) by ANALMETR:def 10;
reconsider e1' = e1, e2' = e2 as Element of (Af X) 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 A13, ANALMETR:84;
then o,c // a,c by A14, 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 A15: o,a // a,c by ANALMETR:81;
LIN o',a',a1' by A2, 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, A15, ANALMETR:82;
hence contradiction by A2, ANALMETR:def 11; :: thesis: verum
end;
then consider c2' being Element of (Af X) such that
A16: ( LIN o',e1',c2' & LIN a2',e2',c2' ) by AFF_1:74;
reconsider c2 = c2' as Element of X by ANALMETR:47;
A17: o,c _|_ o,c2
proof
LIN o,e1,c2 by A16, ANALMETR:55;
then o,e1 // o,c2 by ANALMETR:def 11;
hence o,c _|_ o,c2 by A13, ANALMETR:84; :: thesis: verum
end;
A18: a,c _|_ a2,c2
proof
LIN a2,e2,c2 by A16, ANALMETR:55;
then a2,e2 // a2,c2 by ANALMETR:def 11;
hence a,c _|_ a2,c2 by A14, ANALMETR:84; :: thesis: verum
end;
A19: 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 A20: a,o // a,c by ANALMETR:def 11;
LIN o',a',a1' by A2, 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, A20, ANALMETR:82;
hence contradiction by A2, 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 A21: b,o // b,a 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,a by A2, A21, ANALMETR:82;
hence contradiction by A2, ANALMETR:def 11; :: thesis: verum
end;
then A22: b,c _|_ b2,c2 by A1, A3, A11, A12, A17, A18, A19, Def4;
A23: o,a1 _|_ o,a2
proof
o,a // o,a1 by A2, ANALMETR:def 11;
hence o,a1 _|_ o,a2 by A2, A3, ANALMETR:84; :: thesis: verum
end;
A24: o,b1 _|_ o,b2
proof
o,b // o,b1 by A2, ANALMETR:def 11;
hence o,b1 _|_ o,b2 by A2, A11, ANALMETR:84; :: thesis: verum
end;
A25: o,c1 _|_ o,c2
proof
o,c // o,c1 by A2, ANALMETR:def 11;
hence o,c1 _|_ o,c2 by A2, A17, ANALMETR:84; :: thesis: verum
end;
A26: a1,b1 _|_ a2,b2
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;
hence a1,b1 _|_ a2,b2 by A2, A12, ANALMETR:84; :: thesis: verum
end;
A27: a1,c1 _|_ a2,c2
proof
a <> c
proof
assume a = c ; :: thesis: contradiction
then LIN a',a1',c' by AFF_1:16;
hence contradiction by A2, ANALMETR:55; :: thesis: verum
end;
hence a1,c1 _|_ a2,c2 by A2, A18, ANALMETR:84; :: thesis: verum
end;
A28: 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 A29: a1,o // a1,c1 by ANALMETR:def 11;
A30: a1 <> c1
proof
assume a1 = c1 ; :: thesis: contradiction
then LIN o',c',a1' by A2, ANALMETR:55;
then LIN a1',c',o' by AFF_1:15;
then LIN a1,c,o by ANALMETR:55;
then A31: a1,c // a1,o by ANALMETR:def 11;
LIN o',a',a1' by A2, 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 A2, A31, 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 A2, ANALMETR:55; :: thesis: verum
end;
LIN o',a',a1' by A2, 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 A2, A29, ANALMETR:82;
then a1,a // a,c by A2, A30, ANALMETR:82;
then a,a1 // a,c by ANALMETR:81;
hence contradiction by A2, 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 A32: b1,a1 // b1,o by ANALMETR:def 11;
A33: a1 <> b1
proof
assume a1 = b1 ; :: thesis: contradiction
then LIN o',a',b1' by A2, ANALMETR:55;
then LIN b1',o',a' by AFF_1:15;
then LIN b1,o,a by ANALMETR:55;
then A34: b1,o // b1,a by ANALMETR:def 11;
LIN o',b',b1' by A2, 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 A2, A34, 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 A2, ANALMETR:55; :: thesis: verum
end;
A35: b1,a1 // a,b by A2, ANALMETR:81;
LIN o',b',b1' by A2, 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 A2, A32, ANALMETR:82;
then b1,b // a,b by A33, A35, ANALMETR:82;
then b,b1 // b,a by ANALMETR:81;
hence contradiction by A2, ANALMETR:def 11; :: thesis: verum
end;
then A36: b1,c1 _|_ b2,c2 by A1, A23, A24, A25, A26, A27, A28, Def4;
A37: now
assume A38: not LIN o,b,c ; :: thesis: b,c // b1,c1
b2 <> c2
proof
assume A39: b2 = c2 ; :: thesis: contradiction
o <> b2 then o,b // o,c by A11, A17, A39, ANALMETR:85;
hence contradiction by A38, ANALMETR:def 11; :: thesis: verum
end;
hence b,c // b1,c1 by A22, A36, ANALMETR:85; :: thesis: verum
end;
now
assume A42: LIN o,b,c ; :: thesis: b,c // b1,c1
now
A43: LIN b',c',b1'
proof
LIN o',b',c' by A42, ANALMETR:55;
then LIN b',o',c' by AFF_1:15;
then A44: b',o' // b',c' by AFF_1:def 1;
LIN o',b',b1' by A2, 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 A2, A44, AFF_1:14;
hence LIN b',c',b1' by AFF_1:def 1; :: thesis: verum
end;
LIN b',c',c1'
proof
LIN o',b',c' by A42, ANALMETR:55;
then LIN c',o',b' by AFF_1:15;
then A45: c',o' // c',b' by AFF_1:def 1;
LIN o',c',c1' by A2, 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 A2, A45, AFF_1:14;
then LIN c',b',c1' by AFF_1:def 1;
hence LIN b',c',c1' by AFF_1:15; :: thesis: verum
end;
then b',c' // b1',c1' by A43, AFF_1:19;
hence b,c // b1,c1 by ANALMETR:48; :: thesis: verum
end;
hence b,c // b1,c1 ; :: thesis: verum
end;
hence b,c // b1,c1 by A37; :: thesis: verum