let X be OrtAfPl; ( X is satisfying_ODES implies X is satisfying_DES )
assume A1:
X is satisfying_ODES
; X is satisfying_DES
let o be Element of X; CONAFFM:def 1 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; ( 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
; 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
;
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
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;
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
;
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;
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
;
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;
verum
end;
not o,a // o,b
proof
assume
o,
a // o,
b
;
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;
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
then A44:
a1,b1 _|_ a2,b2
by A12, A27, ANALMETR:62;
a <> c
then A45:
a1,c1 _|_ a2,c2
by A13, A36, ANALMETR:62;
A46:
not o,c1 // o,a1
proof
assume
o,
c1 // o,
a1
;
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
;
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;
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;
verum
end;
not o,a1 // o,b1
proof
assume
o,
a1 // o,
b1
;
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
;
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;
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;
verum
end;
then A54:
b1,c1 _|_ b2,c2
by A1, A41, A42, A43, A44, A45, A46;
A55:
now ( not LIN o,b,c implies b,c // b1,c1 )assume A56:
not
LIN o,
b,
c
;
b,c // b1,c1
b2 <> c2
proof
assume A57:
b2 = c2
;
contradiction
o <> b2
proof
assume A58:
o = b2
;
contradiction
a2,
o _|_ a,
o
by A14, ANALMETR:61;
then
a,
o // a,
b
by A15, A27, A58, ANALMETR:63;
then
LIN a,
o,
b
by ANALMETR:def 10;
then
LIN a9,
o9,
b9
by ANALMETR:40;
then
LIN b9,
o9,
a9
by AFF_1:6;
then
LIN b,
o,
a
by ANALMETR:40;
then A59:
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, A59, ANALMETR:60;
hence
contradiction
by A7, ANALMETR:def 10;
verum
end;
then
o,
b // o,
c
by A26, A35, A57, ANALMETR:63;
hence
contradiction
by A56, ANALMETR:def 10;
verum
end; hence
b,
c // b1,
c1
by A40, A54, ANALMETR:63;
verum end;
now ( LIN o,b,c implies b,c // b1,c1 )assume A60:
LIN o,
b,
c
;
b,c // b1,c1then
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;
verum end;
hence
b,c // b1,c1
by A55; verum