let X be OrtAfPl; :: thesis: ( X is satisfying_AH implies X is satisfying_TDES )
assume A1: X is satisfying_AH ; :: thesis: X is satisfying_TDES
let o be Element of X; :: according to CONMETR:def 5 :: 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 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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
proof
assume a9 = b9 ; :: thesis: contradiction
then LIN b9,b19,a9 by AFF_1:7;
hence contradiction by A8, ANALMETR:40; :: thesis: verum
end;
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; :: thesis: verum
end;
A28: now :: thesis: ( not LIN a,b,c implies a,c // a1,c1 )
not o9,e19 // c29,e29
proof
assume o9,e19 // c29,e29 ; :: thesis: 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; :: thesis: 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 ; :: thesis: a,c // a1,c1
A35: b <> a
proof
assume b = a ; :: thesis: contradiction
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A34, ANALMETR:40; :: thesis: verum
end;
A36: not o,c // o,b
proof
assume o,c // o,b ; :: thesis: 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; :: thesis: verum
end;
A38: not o,a // o,c
proof
assume o,a // o,c ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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 A54: o <> a2 assume LIN o9,b29,a29 ; :: thesis: 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
proof
assume a9 = b9 ; :: thesis: contradiction
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A34, ANALMETR:40; :: thesis: verum
end;
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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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
proof
assume b = c ; :: thesis: contradiction
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A34, ANALMETR:40; :: thesis: verum
end;
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 ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
a <> b
proof
assume a = b ; :: thesis: contradiction
then LIN b9,b19,a9 by AFF_1:7;
hence contradiction by A8, ANALMETR:40; :: thesis: verum
end;
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; :: thesis: verum
end;
now :: thesis: ( LIN a,b,c implies a,c // a1,c1 )
assume A82: LIN a,b,c ; :: thesis: a,c // a1,c1
then A83: LIN a9,b9,c9 by ANALMETR:40;
A84: a <> b
proof
assume a = b ; :: thesis: contradiction
then LIN b9,b19,a9 by AFF_1:7;
hence contradiction by A8, ANALMETR:40; :: thesis: verum
end;
A85: now :: thesis: ( a1,c1 // a,b implies a,c // a1,c1 )
assume a1,c1 // a,b ; :: thesis: a,c // a1,c1
then 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; :: thesis: verum
end;
A87: b <> c
proof
assume b = c ; :: thesis: contradiction
then LIN b9,b19,c9 by AFF_1:7;
hence contradiction by A9, ANALMETR:40; :: thesis: verum
end;
A88: now :: thesis: ( 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 ; :: thesis: a,c // a1,c1
hence a,c // a1,c1 by A15, A87, A89, ANALMETR:60; :: thesis: 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; :: thesis: verum
end;
hence a,c // a1,c1 by A28; :: thesis: verum