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 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 X such that
A14: o,a _|_ o,a2 and
A15: o <> a2 by ANALMETR:def 9;
consider e1 being Element of X such that
A16: o,b _|_ o,e1 and
A17: o <> e1 by ANALMETR:def 9;
consider e2 being Element of X such that
A18: a,b _|_ a2,e2 and
A19: a2 <> e2 by ANALMETR:def 9;
reconsider o9 = o, a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1, a29 = a2, e19 = e1, e29 = e2 as Element of AffinStruct(# the U1 of X, the CONGR of X #) ;
not o9,e19 // a29,e29
proof
assume o9,e19 // a29,e29 ; :: thesis: contradiction
then o,e1 // a2,e2 by ANALMETR:36;
then a2,e2 _|_ o,b by A16, A17, ANALMETR:62;
then a,b // o,b by A18, A19, ANALMETR:63;
then A20: a9,b9 // o9,b9 by ANALMETR:36;
then b9,a9 // b9,o9 by AFF_1:4;
then A21: LIN b9,a9,o9 by AFF_1:def 1;
o9,b9 // b9,a9 by A20, AFF_1:4;
then A22: o,b // b,a by ANALMETR:36;
A23: b9 <> a9
proof
assume b9 = a9 ; :: thesis: contradiction
then LIN b9,b19,a9 by AFF_1:7;
hence contradiction by A7, ANALMETR:40; :: thesis: verum
end;
o,b // o,b1 by A10, ANALMETR:def 10;
then b,a // o,b1 by A4, A22, ANALMETR:60;
then b9,a9 // o9,b19 by ANALMETR:36;
then LIN b9,a9,b19 by A21, A23, AFF_1:9;
then LIN b9,b19,a9 by AFF_1:6;
hence contradiction by A7, ANALMETR:40; :: thesis: verum
end;
then consider b29 being Element of AffinStruct(# the U1 of X, the CONGR of X #) such that
A24: LIN o9,e19,b29 and
A25: LIN a29,e29,b29 by AFF_1:60;
reconsider b2 = b29 as Element of X ;
LIN o,e1,b2 by A24, ANALMETR:40;
then o,e1 // o,b2 by ANALMETR:def 10;
then A26: o,b _|_ o,b2 by A16, A17, ANALMETR:62;
LIN a2,e2,b2 by A25, ANALMETR:40;
then a2,e2 // a2,b2 by ANALMETR:def 10;
then A27: a,b _|_ a2,b2 by A18, A19, ANALMETR:62;
consider e1 being Element of X such that
A28: o,c _|_ o,e1 and
A29: o <> e1 by ANALMETR:def 9;
consider e2 being Element of X such that
A30: a,c _|_ a2,e2 and
A31: a2 <> e2 by ANALMETR:def 9;
reconsider e19 = e1, e29 = e2 as Element of AffinStruct(# the U1 of X, the CONGR of X #) ;
not o9,e19 // a29,e29
proof
assume o9,e19 // a29,e29 ; :: thesis: contradiction
then o,e1 // a2,e2 by ANALMETR:36;
then o,c _|_ a2,e2 by A28, A29, ANALMETR:62;
then o,c // a,c by A30, A31, ANALMETR:63;
then c,o // c,a by ANALMETR:59;
then LIN c,o,a by ANALMETR:def 10;
then LIN c9,o9,a9 by ANALMETR:40;
then LIN a9,c9,o9 by AFF_1:6;
then LIN a,c,o by ANALMETR:40;
then a,c // a,o by ANALMETR:def 10;
then A32: o,a // a,c by ANALMETR:59;
LIN o9,a9,a19 by A9, ANALMETR:40;
then LIN a9,o9,a19 by AFF_1:6;
then LIN a,o,a1 by ANALMETR:40;
then a,o // a,a1 by ANALMETR:def 10;
then o,a // a,a1 by ANALMETR:59;
then a,a1 // a,c by A2, A32, ANALMETR:60;
hence contradiction by A8, ANALMETR:def 10; :: thesis: verum
end;
then consider c29 being Element of AffinStruct(# the U1 of X, the CONGR of X #) such that
A33: LIN o9,e19,c29 and
A34: LIN a29,e29,c29 by AFF_1:60;
reconsider c2 = c29 as Element of X ;
LIN o,e1,c2 by A33, ANALMETR:40;
then o,e1 // o,c2 by ANALMETR:def 10;
then A35: o,c _|_ o,c2 by A28, A29, ANALMETR:62;
LIN a2,e2,c2 by A34, ANALMETR:40;
then a2,e2 // a2,c2 by ANALMETR:def 10;
then A36: a,c _|_ a2,c2 by A30, A31, ANALMETR:62;
A37: not o,c // o,a
proof
assume o,c // o,a ; :: thesis: contradiction
then LIN o,c,a by ANALMETR:def 10;
then LIN o9,c9,a9 by ANALMETR:40;
then LIN a9,o9,c9 by AFF_1:6;
then LIN a,o,c by ANALMETR:40;
then A38: a,o // a,c by ANALMETR:def 10;
LIN o9,a9,a19 by A9, ANALMETR:40;
then LIN a9,o9,a19 by AFF_1:6;
then LIN a,o,a1 by ANALMETR:40;
then a,o // a,a1 by ANALMETR:def 10;
then a,a1 // a,c by A2, A38, ANALMETR:60;
hence contradiction by A8, ANALMETR:def 10; :: thesis: verum
end;
not o,a // o,b
proof
assume o,a // o,b ; :: thesis: contradiction
then LIN o,a,b by ANALMETR:def 10;
then LIN o9,a9,b9 by ANALMETR:40;
then LIN b9,o9,a9 by AFF_1:6;
then LIN b,o,a by ANALMETR:40;
then A39: b,o // b,a by ANALMETR:def 10;
LIN o9,b9,b19 by A10, ANALMETR:40;
then LIN b9,o9,b19 by AFF_1:6;
then LIN b,o,b1 by ANALMETR:40;
then b,o // b,b1 by ANALMETR:def 10;
then b,b1 // b,a by A4, A39, ANALMETR:60;
hence contradiction by A7, ANALMETR:def 10; :: thesis: verum
end;
then A40: b,c _|_ b2,c2 by A1, A14, A26, A27, A35, A36, A37;
o,a // o,a1 by A9, ANALMETR:def 10;
then A41: o,a1 _|_ o,a2 by A2, A14, ANALMETR:62;
o,b // o,b1 by A10, ANALMETR:def 10;
then A42: o,b1 _|_ o,b2 by A4, A26, ANALMETR:62;
o,c // o,c1 by A11, ANALMETR:def 10;
then A43: o,c1 _|_ o,c2 by A6, A35, ANALMETR:62;
a <> b
proof
assume a = b ; :: thesis: contradiction
then LIN b9,b19,a9 by AFF_1:7;
hence contradiction by A7, ANALMETR:40; :: thesis: verum
end;
then A44: a1,b1 _|_ a2,b2 by A12, A27, ANALMETR:62;
a <> c
proof
assume a = c ; :: thesis: contradiction
then LIN a9,a19,c9 by AFF_1:7;
hence contradiction by A8, ANALMETR:40; :: thesis: verum
end;
then A45: a1,c1 _|_ a2,c2 by A13, A36, ANALMETR:62;
A46: not o,c1 // o,a1
proof
assume o,c1 // o,a1 ; :: thesis: contradiction
then LIN o,c1,a1 by ANALMETR:def 10;
then LIN o9,c19,a19 by ANALMETR:40;
then LIN a19,o9,c19 by AFF_1:6;
then LIN a1,o,c1 by ANALMETR:40;
then A47: a1,o // a1,c1 by ANALMETR:def 10;
A48: a1 <> c1
proof
assume a1 = c1 ; :: thesis: contradiction
then LIN o9,c9,a19 by A11, ANALMETR:40;
then LIN a19,c9,o9 by AFF_1:6;
then LIN a1,c,o by ANALMETR:40;
then A49: a1,c // a1,o by ANALMETR:def 10;
LIN o9,a9,a19 by A9, ANALMETR:40;
then LIN a19,o9,a9 by AFF_1:6;
then LIN a1,o,a by ANALMETR:40;
then a1,o // a1,a by ANALMETR:def 10;
then a1,c // a1,a by A3, A49, ANALMETR:60;
then LIN a1,c,a by ANALMETR:def 10;
then LIN a19,c9,a9 by ANALMETR:40;
then LIN a9,a19,c9 by AFF_1:6;
hence contradiction by A8, ANALMETR:40; :: thesis: verum
end;
LIN o9,a9,a19 by A9, ANALMETR:40;
then LIN a19,o9,a9 by AFF_1:6;
then LIN a1,o,a by ANALMETR:40;
then a1,o // a1,a by ANALMETR:def 10;
then a1,c1 // a1,a by A3, A47, ANALMETR:60;
then a1,a // a,c by A13, A48, ANALMETR:60;
then a,a1 // a,c by ANALMETR:59;
hence contradiction by A8, ANALMETR:def 10; :: thesis: verum
end;
not o,a1 // o,b1
proof
assume o,a1 // o,b1 ; :: thesis: contradiction
then LIN o,a1,b1 by ANALMETR:def 10;
then LIN o9,a19,b19 by ANALMETR:40;
then LIN b19,a19,o9 by AFF_1:6;
then LIN b1,a1,o by ANALMETR:40;
then A50: b1,a1 // b1,o by ANALMETR:def 10;
A51: a1 <> b1
proof
assume a1 = b1 ; :: thesis: contradiction
then LIN o9,a9,b19 by A9, ANALMETR:40;
then LIN b19,o9,a9 by AFF_1:6;
then LIN b1,o,a by ANALMETR:40;
then A52: b1,o // b1,a by ANALMETR:def 10;
LIN o9,b9,b19 by A10, ANALMETR:40;
then LIN b19,b9,o9 by AFF_1:6;
then LIN b1,b,o by ANALMETR:40;
then b1,b // b1,o by ANALMETR:def 10;
then b1,a // b1,b by A5, A52, ANALMETR:60;
then LIN b1,a,b by ANALMETR:def 10;
then LIN b19,a9,b9 by ANALMETR:40;
then LIN b9,b19,a9 by AFF_1:6;
hence contradiction by A7, ANALMETR:40; :: thesis: verum
end;
A53: b1,a1 // a,b by A12, ANALMETR:59;
LIN o9,b9,b19 by A10, ANALMETR:40;
then LIN b19,b9,o9 by AFF_1:6;
then LIN b1,b,o by ANALMETR:40;
then b1,b // b1,o by ANALMETR:def 10;
then b1,a1 // b1,b by A5, A50, ANALMETR:60;
then b1,b // a,b by A51, A53, ANALMETR:60;
then b,b1 // b,a by ANALMETR:59;
hence contradiction by A7, ANALMETR:def 10; :: thesis: verum
end;
then A54: b1,c1 _|_ b2,c2 by A1, A41, A42, A43, A44, A45, A46;
A55: now :: thesis: ( not LIN o,b,c implies b,c // b1,c1 )
assume A56: not LIN o,b,c ; :: thesis: b,c // b1,c1
b2 <> c2
proof
assume A57: b2 = c2 ; :: thesis: contradiction
o <> b2 then o,b // o,c by A26, A35, A57, ANALMETR:63;
hence contradiction by A56, ANALMETR:def 10; :: thesis: verum
end;
hence b,c // b1,c1 by A40, A54, ANALMETR:63; :: thesis: verum
end;
now :: thesis: ( LIN o,b,c implies b,c // b1,c1 )
assume A60: LIN o,b,c ; :: thesis: b,c // b1,c1
then LIN o9,b9,c9 by ANALMETR:40;
then LIN b9,o9,c9 by AFF_1:6;
then A61: b9,o9 // b9,c9 by AFF_1:def 1;
LIN o9,b9,b19 by A10, ANALMETR:40;
then LIN b9,o9,b19 by AFF_1:6;
then b9,o9 // b9,b19 by AFF_1:def 1;
then b9,c9 // b9,b19 by A4, A61, AFF_1:5;
then A62: LIN b9,c9,b19 by AFF_1:def 1;
LIN o9,b9,c9 by A60, ANALMETR:40;
then LIN c9,o9,b9 by AFF_1:6;
then A63: c9,o9 // c9,b9 by AFF_1:def 1;
LIN o9,c9,c19 by A11, ANALMETR:40;
then LIN c9,o9,c19 by AFF_1:6;
then c9,o9 // c9,c19 by AFF_1:def 1;
then c9,b9 // c9,c19 by A6, A63, AFF_1:5;
then LIN c9,b9,c19 by AFF_1:def 1;
then LIN b9,c9,c19 by AFF_1:6;
then b9,c9 // b19,c19 by A62, AFF_1:10;
hence b,c // b1,c1 by ANALMETR:36; :: thesis: verum
end;
hence b,c // b1,c1 by A55; :: thesis: verum