let X be OrtAfPl; ( X is satisfying_AH implies X is satisfying_TDES )
assume A1:
X is satisfying_AH
; X is satisfying_TDES
let o be Element of X; CONMETR:def 5 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; ( 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 that
A2:
o <> a
and
A3:
o <> a1
and
A4:
o <> b
and
A5:
o <> b1
and
A6:
o <> c
and
A7:
o <> c1
and
A8:
not LIN b,b1,a
and
A9:
not LIN b,b1,c
and
A10:
LIN o,a,a1
and
A11:
LIN o,b,b1
and
A12:
LIN o,c,c1
and
A13:
a,b // a1,b1
and
A14:
a,b // o,c
and
A15:
b,c // b1,c1
; a,c // a1,c1
consider e1 being Element of X such that
A16:
o,b _|_ o,e1
and
A17:
o <> e1
by ANALMETR:def 9;
consider c2 being Element of X such that
A18:
o,c _|_ o,c2
and
A19:
o <> c2
by ANALMETR:def 9;
consider e2 being Element of X such that
A20:
b,c _|_ c2,e2
and
A21:
c2 <> e2
by ANALMETR:def 9;
reconsider o9 = o, a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1, c29 = c2, e19 = e1, e29 = e2 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
A22:
b1 <> a1
proof
assume
b1 = a1
;
contradiction
then
LIN o9,
b9,
a19
by A11, ANALMETR:40;
then
o9,
b9 // o9,
a19
by AFF_1:def 1;
then
o9,
a19 // o9,
b9
by AFF_1:4;
then A23:
o,
a1 // o,
b
by ANALMETR:36;
o,
a // o,
a1
by A10, ANALMETR:def 10;
then
o9,
a9 // o9,
a19
by ANALMETR:36;
then
o9,
a19 // o9,
a9
by AFF_1:4;
then
o,
a1 // o,
a
by ANALMETR:36;
then
o,
a // o,
b
by A3, A23, ANALMETR:60;
then
LIN o,
a,
b
by ANALMETR:def 10;
then A24:
LIN o9,
a9,
b9
by ANALMETR:40;
then
LIN b9,
o9,
a9
by AFF_1:6;
then
b9,
o9 // b9,
a9
by AFF_1:def 1;
then
o9,
b9 // a9,
b9
by AFF_1:4;
then A25:
o,
b // a,
b
by ANALMETR:36;
A26:
a9 <> b9
o,
b // o,
b1
by A11, ANALMETR:def 10;
then
a,
b // o,
b1
by A4, A25, ANALMETR:60;
then A27:
a9,
b9 // o9,
b19
by ANALMETR:36;
LIN a9,
b9,
o9
by A24, AFF_1:6;
then
LIN a9,
b9,
b19
by A27, A26, AFF_1:9;
then
LIN b9,
b19,
a9
by AFF_1:6;
hence
contradiction
by A8, ANALMETR:40;
verum
end;
A28:
now ( not LIN a,b,c implies a,c // a1,c1 )
not
o9,
e19 // c29,
e29
proof
assume
o9,
e19 // c29,
e29
;
contradiction
then
o,
e1 // c2,
e2
by ANALMETR:36;
then
c2,
e2 _|_ o,
b
by A16, A17, ANALMETR:62;
then
c2,
e2 _|_ b,
o
by ANALMETR:61;
then
b,
c // b,
o
by A20, A21, ANALMETR:63;
then
LIN b,
c,
o
by ANALMETR:def 10;
then
LIN b9,
c9,
o9
by ANALMETR:40;
then
LIN b9,
o9,
c9
by AFF_1:6;
then
LIN b,
o,
c
by ANALMETR:40;
then A29:
b,
o // b,
c
by ANALMETR:def 10;
LIN o9,
b9,
b19
by A11, 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,
c
by A4, A29, ANALMETR:60;
hence
contradiction
by A9, ANALMETR:def 10;
verum
end; then consider b29 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A30:
LIN o9,
e19,
b29
and A31:
LIN c29,
e29,
b29
by AFF_1:60;
reconsider b2 =
b29 as
Element of
X ;
LIN o,
e1,
b2
by A30, ANALMETR:40;
then
o,
e1 // o,
b2
by ANALMETR:def 10;
then A32:
o,
b _|_ o,
b2
by A16, A17, ANALMETR:62;
o,
b // o,
b1
by A11, ANALMETR:def 10;
then A33:
o,
b1 _|_ o,
b2
by A4, A32, ANALMETR:62;
assume A34:
not
LIN a,
b,
c
;
a,c // a1,c1A35:
b <> a
A36:
not
o,
c // o,
b
proof
assume
o,
c // o,
b
;
contradiction
then
LIN o,
c,
b
by ANALMETR:def 10;
then
LIN o9,
c9,
b9
by ANALMETR:40;
then
LIN c9,
o9,
b9
by AFF_1:6;
then
c9,
o9 // c9,
b9
by AFF_1:def 1;
then
o9,
c9 // b9,
c9
by AFF_1:4;
then A37:
o,
c // b,
c
by ANALMETR:36;
a9,
b9 // o9,
c9
by A14, ANALMETR:36;
then
o9,
c9 // b9,
a9
by AFF_1:4;
then
o,
c // b,
a
by ANALMETR:36;
then
b,
a // b,
c
by A6, A37, ANALMETR:60;
then
LIN b,
a,
c
by ANALMETR:def 10;
then
LIN b9,
a9,
c9
by ANALMETR:40;
then
LIN a9,
b9,
c9
by AFF_1:6;
hence
contradiction
by A34, ANALMETR:40;
verum
end; A38:
not
o,
a // o,
c
proof
assume
o,
a // o,
c
;
contradiction
then
LIN o,
a,
c
by ANALMETR:def 10;
then
LIN o9,
a9,
c9
by ANALMETR:40;
then
LIN c9,
o9,
a9
by AFF_1:6;
then
LIN c,
o,
a
by ANALMETR:40;
then A39:
c,
o // c,
a
by ANALMETR:def 10;
a9,
b9 // o9,
c9
by A14, ANALMETR:36;
then
c9,
o9 // a9,
b9
by AFF_1:4;
then
c,
o // a,
b
by ANALMETR:36;
then
a,
b // c,
a
by A6, A39, ANALMETR:60;
then
a9,
b9 // c9,
a9
by ANALMETR:36;
then
a9,
b9 // a9,
c9
by AFF_1:4;
then
a,
b // a,
c
by ANALMETR:36;
hence
contradiction
by A34, ANALMETR:def 10;
verum
end;
LIN c2,
e2,
b2
by A31, ANALMETR:40;
then
c2,
e2 // c2,
b2
by ANALMETR:def 10;
then A40:
b,
c _|_ c2,
b2
by A20, A21, ANALMETR:62;
consider e1 being
Element of
X such that A41:
o,
a _|_ o,
e1
and A42:
o <> e1
by ANALMETR:def 9;
consider e2 being
Element of
X such that A43:
a,
c _|_ c2,
e2
and A44:
c2 <> e2
by ANALMETR:def 9;
reconsider e19 =
e1,
e29 =
e2 as
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #) ;
not
o9,
e19 // c29,
e29
proof
assume
o9,
e19 // c29,
e29
;
contradiction
then
o,
e1 // c2,
e2
by ANALMETR:36;
then
c2,
e2 _|_ o,
a
by A41, A42, ANALMETR:62;
then
a,
c // o,
a
by A43, A44, ANALMETR:63;
then
a9,
c9 // o9,
a9
by ANALMETR:36;
then
a9,
c9 // a9,
o9
by AFF_1:4;
then
LIN a9,
c9,
o9
by AFF_1:def 1;
then
LIN c9,
o9,
a9
by AFF_1:6;
then
LIN c,
o,
a
by ANALMETR:40;
then A45:
c,
o // c,
a
by ANALMETR:def 10;
a9,
b9 // o9,
c9
by A14, ANALMETR:36;
then
c9,
o9 // a9,
b9
by AFF_1:4;
then
c,
o // a,
b
by ANALMETR:36;
then
a,
b // c,
a
by A6, A45, ANALMETR:60;
then
a9,
b9 // c9,
a9
by ANALMETR:36;
then
a9,
b9 // a9,
c9
by AFF_1:4;
then
a,
b // a,
c
by ANALMETR:36;
hence
contradiction
by A34, ANALMETR:def 10;
verum
end; then consider a29 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A46:
LIN o9,
e19,
a29
and A47:
LIN c29,
e29,
a29
by AFF_1:60;
reconsider a2 =
a29 as
Element of
X ;
LIN o,
e1,
a2
by A46, ANALMETR:40;
then
o,
e1 // o,
a2
by ANALMETR:def 10;
then A48:
o,
a _|_ o,
a2
by A41, A42, ANALMETR:62;
A49:
c2 <> a2
proof
assume
c2 = a2
;
contradiction
then
o,
c // o,
a
by A18, A19, A48, ANALMETR:63;
then
LIN o,
c,
a
by ANALMETR:def 10;
then
LIN o9,
c9,
a9
by ANALMETR:40;
then
LIN c9,
a9,
o9
by AFF_1:6;
then
c9,
a9 // c9,
o9
by AFF_1:def 1;
then
o9,
c9 // a9,
c9
by AFF_1:4;
then
o,
c // a,
c
by ANALMETR:36;
then
a,
b // a,
c
by A6, A14, ANALMETR:60;
hence
contradiction
by A34, ANALMETR:def 10;
verum
end;
LIN c2,
e2,
a2
by A47, ANALMETR:40;
then
c2,
e2 // c2,
a2
by ANALMETR:def 10;
then
a,
c _|_ c2,
a2
by A43, A44, ANALMETR:62;
then A50:
c,
a _|_ c2,
a2
by ANALMETR:61;
A51:
not
LIN o9,
b29,
a29
proof
A52:
o <> b2
proof
a9,
b9 // o9,
c9
by A14, ANALMETR:36;
then
o9,
c9 // b9,
a9
by AFF_1:4;
then A53:
o,
c // b,
a
by ANALMETR:36;
assume
o = b2
;
contradiction
then
o,
c2 _|_ b,
c
by A40, ANALMETR:61;
then
o,
c // b,
c
by A18, A19, ANALMETR:63;
then
b,
a // b,
c
by A6, A53, ANALMETR:60;
then
LIN b,
a,
c
by ANALMETR:def 10;
then
LIN b9,
a9,
c9
by ANALMETR:40;
then
LIN a9,
b9,
c9
by AFF_1:6;
hence
contradiction
by A34, ANALMETR:40;
verum
end;
A54:
o <> a2
proof
assume A55:
o = a2
;
contradiction
c2,
o _|_ o,
c
by A18, ANALMETR:61;
then
o,
c // c,
a
by A19, A50, A55, ANALMETR:63;
then
a,
b // c,
a
by A6, A14, ANALMETR:60;
then
a9,
b9 // c9,
a9
by ANALMETR:36;
then
a9,
b9 // a9,
c9
by AFF_1:4;
then
a,
b // a,
c
by ANALMETR:36;
hence
contradiction
by A34, ANALMETR:def 10;
verum
end;
assume
LIN o9,
b29,
a29
;
contradiction
then
LIN o,
b2,
a2
by ANALMETR:40;
then
o,
b2 // o,
a2
by ANALMETR:def 10;
then
o,
a2 _|_ o,
b
by A32, A52, ANALMETR:62;
then
o,
a // o,
b
by A48, A54, ANALMETR:63;
then
LIN o,
a,
b
by ANALMETR:def 10;
then
LIN o9,
a9,
b9
by ANALMETR:40;
then A56:
LIN a9,
b9,
o9
by AFF_1:6;
A57:
a9 <> b9
a9,
b9 // o9,
c9
by A14, ANALMETR:36;
then
LIN a9,
b9,
c9
by A56, A57, AFF_1:9;
hence
contradiction
by A34, ANALMETR:40;
verum
end; consider e1 being
Element of
X such that A58:
o,
a1 _|_ o,
e1
and A59:
o <> e1
by ANALMETR:def 9;
consider e2 being
Element of
X such that A60:
a1,
c1 _|_ c2,
e2
and A61:
c2 <> e2
by ANALMETR:def 9;
reconsider e19 =
e1,
e29 =
e2 as
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #) ;
not
o9,
e19 // c29,
e29
proof
assume
o9,
e19 // c29,
e29
;
contradiction
then
o,
e1 // c2,
e2
by ANALMETR:36;
then
c2,
e2 _|_ o,
a1
by A58, A59, ANALMETR:62;
then
a1,
c1 // o,
a1
by A60, A61, ANALMETR:63;
then
a19,
c19 // o9,
a19
by ANALMETR:36;
then
a19,
c19 // a19,
o9
by AFF_1:4;
then
LIN a19,
c19,
o9
by AFF_1:def 1;
then
LIN o9,
c19,
a19
by AFF_1:6;
then
o9,
c19 // o9,
a19
by AFF_1:def 1;
then A62:
o,
c1 // o,
a1
by ANALMETR:36;
LIN o9,
a9,
a19
by A10, ANALMETR:40;
then
o9,
a9 // o9,
a19
by AFF_1:def 1;
then
o9,
a19 // o9,
a9
by AFF_1:4;
then A63:
o,
a1 // o,
a
by ANALMETR:36;
LIN o9,
c9,
c19
by A12, ANALMETR:40;
then
o9,
c9 // o9,
c19
by AFF_1:def 1;
then
o9,
c19 // o9,
c9
by AFF_1:4;
then
o,
c1 // o,
c
by ANALMETR:36;
then
o,
a1 // o,
c
by A7, A62, ANALMETR:60;
then
o,
a // o,
c
by A3, A63, ANALMETR:60;
then
LIN o,
a,
c
by ANALMETR:def 10;
then
LIN o9,
a9,
c9
by ANALMETR:40;
then
LIN c9,
o9,
a9
by AFF_1:6;
then
c9,
o9 // c9,
a9
by AFF_1:def 1;
then
o9,
c9 // a9,
c9
by AFF_1:4;
then
o,
c // a,
c
by ANALMETR:36;
then
a,
b // a,
c
by A6, A14, ANALMETR:60;
hence
contradiction
by A34, ANALMETR:def 10;
verum
end; then consider a39 being
Element of
AffinStruct(# the
carrier of
X, the
CONGR of
X #)
such that A64:
LIN o9,
e19,
a39
and A65:
LIN c29,
e29,
a39
by AFF_1:60;
reconsider a3 =
a39 as
Element of
X ;
LIN o,
e1,
a3
by A64, ANALMETR:40;
then
o,
e1 // o,
a3
by ANALMETR:def 10;
then A66:
o,
a1 _|_ o,
a3
by A58, A59, ANALMETR:62;
b <> c
then
c2,
b2 _|_ b1,
c1
by A15, A40, ANALMETR:62;
then A67:
c1,
b1 _|_ c2,
b2
by ANALMETR:61;
A68:
not
o,
a1 // o,
c1
proof
o,
a // o,
a1
by A10, ANALMETR:def 10;
then
o9,
a9 // o9,
a19
by ANALMETR:36;
then
o9,
a19 // o9,
a9
by AFF_1:4;
then A69:
o,
a1 // o,
a
by ANALMETR:36;
assume
o,
a1 // o,
c1
;
contradiction
then
o9,
a19 // o9,
c19
by ANALMETR:36;
then
o9,
c19 // o9,
a19
by AFF_1:4;
then A70:
o,
c1 // o,
a1
by ANALMETR:36;
o,
c // o,
c1
by A12, ANALMETR:def 10;
then
o9,
c9 // o9,
c19
by ANALMETR:36;
then
o9,
c19 // o9,
c9
by AFF_1:4;
then
o,
c1 // o,
c
by ANALMETR:36;
then
o,
a1 // o,
c
by A7, A70, ANALMETR:60;
then
o,
a // o,
c
by A3, A69, ANALMETR:60;
then
LIN o,
a,
c
by ANALMETR:def 10;
then
LIN o9,
a9,
c9
by ANALMETR:40;
then
LIN c9,
a9,
o9
by AFF_1:6;
then
c9,
a9 // c9,
o9
by AFF_1:def 1;
then
o9,
c9 // a9,
c9
by AFF_1:4;
then
o,
c // a,
c
by ANALMETR:36;
then
a,
b // a,
c
by A6, A14, ANALMETR:60;
hence
contradiction
by A34, ANALMETR:def 10;
verum
end;
a9,
b9 // o9,
c9
by A14, ANALMETR:36;
then
o9,
c9 // b9,
a9
by AFF_1:4;
then A71:
o,
c // b,
a
by ANALMETR:36;
A72:
not
o,
c1 // o,
b1
proof
o,
b // o,
b1
by A11, ANALMETR:def 10;
then
o9,
b9 // o9,
b19
by ANALMETR:36;
then
o9,
b19 // o9,
b9
by AFF_1:4;
then A73:
o,
b1 // o,
b
by ANALMETR:36;
o,
c // o,
c1
by A12, ANALMETR:def 10;
then
o9,
c9 // o9,
c19
by ANALMETR:36;
then
o9,
c19 // o9,
c9
by AFF_1:4;
then A74:
o,
c1 // o,
c
by ANALMETR:36;
assume
o,
c1 // o,
b1
;
contradiction
then
o,
b1 // o,
c
by A7, A74, ANALMETR:60;
then
o,
b // o,
c
by A5, A73, ANALMETR:60;
then
LIN o,
b,
c
by ANALMETR:def 10;
then
LIN o9,
b9,
c9
by ANALMETR:40;
then
LIN c9,
o9,
b9
by AFF_1:6;
then
c9,
o9 // c9,
b9
by AFF_1:def 1;
then
o9,
c9 // b9,
c9
by AFF_1:4;
then A75:
o,
c // b,
c
by ANALMETR:36;
a9,
b9 // o9,
c9
by A14, ANALMETR:36;
then
o9,
c9 // b9,
a9
by AFF_1:4;
then
o,
c // b,
a
by ANALMETR:36;
then
b,
a // b,
c
by A6, A75, ANALMETR:60;
then
LIN b,
a,
c
by ANALMETR:def 10;
then
LIN b9,
a9,
c9
by ANALMETR:40;
then
LIN a9,
b9,
c9
by AFF_1:6;
hence
contradiction
by A34, ANALMETR:40;
verum
end;
a <> b
then
o,
c // a1,
b1
by A13, A14, ANALMETR:60;
then
o9,
c9 // a19,
b19
by ANALMETR:36;
then
o9,
c9 // b19,
a19
by AFF_1:4;
then A76:
o,
c // b1,
a1
by ANALMETR:36;
o,
c // o,
c1
by A12, ANALMETR:def 10;
then A77:
o,
c1 // b1,
a1
by A6, A76, ANALMETR:60;
o,
c // o,
c1
by A12, ANALMETR:def 10;
then A78:
o,
c1 _|_ o,
c2
by A6, A18, ANALMETR:62;
c,
b _|_ c2,
b2
by A40, ANALMETR:61;
then
b,
a _|_ b2,
a2
by A1, A18, A32, A48, A71, A50, A38, A36, CONAFFM:def 2;
then
b2,
a2 _|_ a,
b
by ANALMETR:61;
then
b2,
a2 _|_ a1,
b1
by A13, A35, ANALMETR:62;
then A79:
b1,
a1 _|_ b2,
a2
by ANALMETR:61;
o,
a // o,
a1
by A10, ANALMETR:def 10;
then
o,
a1 _|_ o,
a2
by A2, A48, ANALMETR:62;
then
o,
a2 // o,
a3
by A3, A66, ANALMETR:63;
then
LIN o,
a2,
a3
by ANALMETR:def 10;
then A80:
LIN o9,
a29,
a39
by ANALMETR:40;
LIN c2,
e2,
a3
by A65, ANALMETR:40;
then
c2,
e2 // c2,
a3
by ANALMETR:def 10;
then A81:
a1,
c1 _|_ c2,
a3
by A60, A61, ANALMETR:62;
then
c1,
a1 _|_ c2,
a3
by ANALMETR:61;
then
b1,
a1 _|_ b2,
a3
by A1, A66, A78, A33, A67, A77, A68, A72, CONAFFM:def 2;
then
b2,
a3 // b2,
a2
by A22, A79, ANALMETR:63;
then
b29,
a39 // b29,
a29
by ANALMETR:36;
then
b29,
a29 // b29,
a39
by AFF_1:4;
then
a29 = a39
by A51, A80, AFF_1:14;
then
c,
a // a1,
c1
by A50, A81, A49, ANALMETR:63;
then
c9,
a9 // a19,
c19
by ANALMETR:36;
then
a9,
c9 // a19,
c19
by AFF_1:4;
hence
a,
c // a1,
c1
by ANALMETR:36;
verum end;
now ( LIN a,b,c implies a,c // a1,c1 )assume A82:
LIN a,
b,
c
;
a,c // a1,c1then A83:
LIN a9,
b9,
c9
by ANALMETR:40;
A84:
a <> b
A85:
now ( a1,c1 // a,b implies a,c // a1,c1 )assume
a1,
c1 // a,
b
;
a,c // a1,c1then
a19,
c19 // a9,
b9
by ANALMETR:36;
then
a9,
b9 // a19,
c19
by AFF_1:4;
then A86:
a,
b // a1,
c1
by ANALMETR:36;
a,
b // a,
c
by A82, ANALMETR:def 10;
hence
a,
c // a1,
c1
by A84, A86, ANALMETR:60;
verum end; A87:
b <> c
A88:
now ( a1 = b1 implies a,c // a1,c1 )
LIN c9,
b9,
a9
by A83, AFF_1:6;
then
c9,
b9 // c9,
a9
by AFF_1:def 1;
then
b9,
c9 // a9,
c9
by AFF_1:4;
then A89:
b,
c // a,
c
by ANALMETR:36;
assume
a1 = b1
;
a,c // a1,c1hence
a,
c // a1,
c1
by A15, A87, A89, ANALMETR:60;
verum end;
LIN b9,
a9,
c9
by A83, AFF_1:6;
then
b9,
a9 // b9,
c9
by AFF_1:def 1;
then
a9,
b9 // b9,
c9
by AFF_1:4;
then
a,
b // b,
c
by ANALMETR:36;
then
b,
c // a1,
b1
by A13, A84, ANALMETR:60;
then
b1,
c1 // a1,
b1
by A15, A87, ANALMETR:60;
then
b19,
c19 // a19,
b19
by ANALMETR:36;
then
b19,
a19 // b19,
c19
by AFF_1:4;
then
LIN b19,
a19,
c19
by AFF_1:def 1;
then
LIN a19,
b19,
c19
by AFF_1:6;
then
LIN a1,
b1,
c1
by ANALMETR:40;
then A90:
a1,
b1 // a1,
c1
by ANALMETR:def 10;
a9,
b9 // a19,
b19
by A13, ANALMETR:36;
then
a19,
b19 // a9,
b9
by AFF_1:4;
then
a1,
b1 // a,
b
by ANALMETR:36;
hence
a,
c // a1,
c1
by A90, A85, A88, ANALMETR:60;
verum end;
hence
a,c // a1,c1
by A28; verum