let AP be AffinPlane; ( AP is satisfying_TDES_1 implies AP is satisfying_des_1 )
assume A1:
AP is satisfying_TDES_1
; AP is satisfying_des_1
let A be Subset of AP; AFF_2:def 12 for P, C being Subset of AP
for a, b, c, a9, b9, c9 being Element of AP st A // P & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
A // C
let P, C be Subset of AP; for a, b, c, a9, b9, c9 being Element of AP st A // P & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 holds
A // C
let a, b, c, a9, b9, c9 be Element of AP; ( A // P & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 & b,c // b9,c9 & not LIN a,b,c & c <> c9 implies A // C )
assume that
A2:
A // P
and
A3:
a in A
and
A4:
a9 in A
and
A5:
b in P
and
A6:
b9 in P
and
A7:
c in C
and
A8:
c9 in C
and
A9:
A is being_line
and
A10:
P is being_line
and
A11:
C is being_line
and
A12:
A <> P
and
A13:
A <> C
and
A14:
a,b // a9,b9
and
A15:
a,c // a9,c9
and
A16:
b,c // b9,c9
and
A17:
not LIN a,b,c
and
A18:
c <> c9
; A // C
set P9 = Line (a,b);
set C9 = Line (a9,b9);
A19:
a9 <> b9
by A2, A4, A6, A12, AFF_1:45;
then A20:
a9 in Line (a9,b9)
by AFF_1:24;
A21:
a9 <> c9
proof
assume
a9 = c9
;
contradiction
then
b,
c // a9,
b9
by A16, AFF_1:4;
then
a,
b // b,
c
by A14, A19, AFF_1:5;
then
b,
a // b,
c
by AFF_1:4;
then
LIN b,
a,
c
by AFF_1:def 1;
hence
contradiction
by A17, AFF_1:6;
verum
end;
A22:
not c9 in A
proof
assume A23:
c9 in A
;
contradiction
a9,
c9 // a,
c
by A15, AFF_1:4;
then
c in A
by A3, A4, A9, A21, A23, AFF_1:48;
hence
contradiction
by A7, A8, A9, A11, A13, A18, A23, AFF_1:18;
verum
end;
A24:
Line (a9,b9) is being_line
by A19, AFF_1:24;
assume A25:
not A // C
; contradiction
then consider o being Element of AP such that
A26:
o in A
and
A27:
o in C
by A9, A11, AFF_1:58;
A28:
LIN o,c9,c
by A7, A8, A11, A27, AFF_1:21;
A29:
a <> a9
proof
assume A30:
a = a9
;
contradiction
then
LIN a,
c,
c9
by A15, AFF_1:def 1;
then A31:
LIN c,
c9,
a
by AFF_1:6;
LIN a,
b,
b9
by A14, A30, AFF_1:def 1;
then
LIN b,
b9,
a
by AFF_1:6;
then
(
b = b9 or
a in P )
by A5, A6, A10, AFF_1:25;
then
LIN b,
c,
c9
by A2, A3, A12, A16, AFF_1:45, AFF_1:def 1;
then A32:
LIN c,
c9,
b
by AFF_1:6;
LIN c,
c9,
c
by AFF_1:7;
hence
contradiction
by A17, A18, A31, A32, AFF_1:8;
verum
end;
A33:
o <> a9
proof
assume A34:
o = a9
;
contradiction
a9,
c9 // c,
a
by A15, AFF_1:4;
then
a in C
by A7, A8, A11, A27, A21, A34, AFF_1:48;
hence
contradiction
by A3, A4, A9, A11, A13, A27, A29, A34, AFF_1:18;
verum
end;
A35:
a <> b
by A17, AFF_1:7;
then A36:
Line (a,b) is being_line
by AFF_1:24;
consider N being Subset of AP such that
A37:
c9 in N
and
A38:
A // N
by A9, AFF_1:49;
A39:
b9 in Line (a9,b9)
by A19, AFF_1:24;
A40:
not N // Line (a9,b9)
N is being_line
by A38, AFF_1:36;
then consider q being Element of AP such that
A41:
q in N
and
A42:
q in Line (a9,b9)
by A24, A40, AFF_1:58;
A43:
c9,q // A
by A37, A38, A41, AFF_1:40;
A44:
c9 <> q
proof
assume
c9 = q
;
contradiction
then
LIN a9,
b9,
c9
by A24, A39, A20, A42, AFF_1:21;
then
a9,
b9 // a9,
c9
by AFF_1:def 1;
then
a9,
b9 // a,
c
by A15, A21, AFF_1:5;
then
a,
b // a,
c
by A14, A19, AFF_1:5;
hence
contradiction
by A17, AFF_1:def 1;
verum
end;
A45:
c9,a9 // c,a
by A15, AFF_1:4;
A46:
c,b // c9,b9
by A16, AFF_1:4;
A47:
a in Line (a,b)
by A35, AFF_1:24;
A48:
b <> c
by A17, AFF_1:7;
A49:
not c in P
proof
assume A50:
c in P
;
contradiction
then
c9 in P
by A5, A6, A10, A16, A48, AFF_1:48;
hence
contradiction
by A2, A7, A8, A10, A11, A18, A25, A50, AFF_1:18;
verum
end;
not P // C
by A2, A25, AFF_1:44;
then consider s being Element of AP such that
A51:
s in P
and
A52:
s in C
by A10, A11, AFF_1:58;
A53:
LIN s,c,c9
by A7, A8, A11, A52, AFF_1:21;
A54:
b <> b9
proof
assume
b = b9
;
contradiction
then
b,
a // b,
a9
by A14, AFF_1:4;
then
LIN b,
a,
a9
by AFF_1:def 1;
then
LIN a,
a9,
b
by AFF_1:6;
then
b in A
by A3, A4, A9, A29, AFF_1:25;
hence
contradiction
by A2, A5, A12, AFF_1:45;
verum
end;
A55:
s <> b
proof
assume A56:
s = b
;
contradiction
b,
c // c9,
b9
by A16, AFF_1:4;
then
b9 in C
by A7, A8, A11, A48, A52, A56, AFF_1:48;
hence
contradiction
by A2, A5, A6, A10, A11, A25, A54, A52, A56, AFF_1:18;
verum
end;
consider M being Subset of AP such that
A57:
c in M
and
A58:
A // M
by A9, AFF_1:49;
A59:
M is being_line
by A58, AFF_1:36;
A60:
b in Line (a,b)
by A35, AFF_1:24;
not M // Line (a,b)
then consider p being Element of AP such that
A61:
p in M
and
A62:
p in Line (a,b)
by A59, A36, AFF_1:58;
M // P
by A2, A58, AFF_1:44;
then A63:
c,p // P
by A57, A61, AFF_1:40;
A64:
M // N
by A58, A38, AFF_1:44;
then A65:
c,p // c9,q
by A57, A37, A61, A41, AFF_1:39;
A66:
now not p = qassume
p = q
;
contradictionthen
M = N
by A64, A61, A41, AFF_1:45;
hence
contradiction
by A7, A8, A11, A18, A25, A57, A58, A37, A59, AFF_1:18;
verum end;
A67:
Line (a,b) // Line (a9,b9)
by A14, A35, A19, AFF_1:37;
then A68:
p,b // q,b9
by A60, A39, A62, A42, AFF_1:39;
A69:
q,a9 // p,a
by A47, A20, A67, A62, A42, AFF_1:39;
c9,q // c,p
by A57, A37, A64, A61, A41, AFF_1:39;
then
LIN o,q,p
by A1, A3, A4, A9, A26, A28, A22, A45, A69, A43, A44, A33;
then A70:
LIN p,q,o
by AFF_1:6;
c <> p
by A17, A36, A60, A47, A62, AFF_1:21;
then
LIN s,p,q
by A1, A5, A6, A10, A51, A53, A63, A68, A49, A55, A65, A46;
then A71:
LIN p,q,s
by AFF_1:6;
LIN p,q,p
by AFF_1:7;
then
( o = s or p in C )
by A11, A27, A52, A70, A71, A66, AFF_1:8, AFF_1:25;
then
c in Line (a,b)
by A2, A7, A11, A12, A25, A26, A57, A58, A59, A61, A62, A51, AFF_1:18, AFF_1:45;
hence
contradiction
by A17, A36, A60, A47, AFF_1:21; verum