let AP be AffinPlane; :: thesis: ( AP is satisfying_TDES_1 implies AP is satisfying_des_1 )

assume A1: AP is satisfying_TDES_1 ; :: thesis: AP is satisfying_des_1

let A be Subset of AP; :: according to AFF_2:def 12 :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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

assume A25: not A // C ; :: thesis: 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

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)

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

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

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

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)

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;

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; :: thesis: verum

assume A1: AP is satisfying_TDES_1 ; :: thesis: AP is satisfying_des_1

let A be Subset of AP; :: according to AFF_2:def 12 :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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

A22:
not c9 in A
assume
a9 = c9
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

proof

A24:
Line (a9,b9) is being_line
by A19, AFF_1:24;
assume A23:
c9 in A
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

assume A25: not A // C ; :: thesis: 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

A33:
o <> a9
assume A30:
a = a9
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

proof

A35:
a <> b
by A17, AFF_1:7;
assume A34:
o = a9
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

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)

proof

N is being_line
by A38, AFF_1:36;
assume
N // Line (a9,b9)
; :: thesis: contradiction

then A // Line (a9,b9) by A38, AFF_1:44;

then b9 in A by A4, A39, A20, AFF_1:45;

hence contradiction by A2, A6, A12, AFF_1:45; :: thesis: verum

end;then A // Line (a9,b9) by A38, AFF_1:44;

then b9 in A by A4, A39, A20, AFF_1:45;

hence contradiction by A2, A6, A12, AFF_1:45; :: thesis: verum

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

A45:
c9,a9 // c,a
by A15, AFF_1:4;
assume
c9 = q
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

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

not P // C
by A2, A25, AFF_1:44;
assume A50:
c in P
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

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

A55:
s <> b
assume
b = b9
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

proof

consider M being Subset of AP such that
assume A56:
s = b
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

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)

proof

then consider p being Element of AP such that
assume
M // Line (a,b)
; :: thesis: contradiction

then A // Line (a,b) by A58, AFF_1:44;

then b in A by A3, A60, A47, AFF_1:45;

hence contradiction by A2, A5, A12, AFF_1:45; :: thesis: verum

end;then A // Line (a,b) by A58, AFF_1:44;

then b in A by A3, A60, A47, AFF_1:45;

hence contradiction by A2, A5, A12, AFF_1:45; :: thesis: verum

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 :: thesis: not p = q

A67:
Line (a,b) // Line (a9,b9)
by A14, A35, A19, AFF_1:37;assume
p = q
; :: thesis: contradiction

then M = N by A64, A61, A41, AFF_1:45;

hence contradiction by A7, A8, A11, A18, A25, A57, A58, A37, A59, AFF_1:18; :: thesis: verum

end;then M = N by A64, A61, A41, AFF_1:45;

hence contradiction by A7, A8, A11, A18, A25, A57, A58, A37, A59, AFF_1:18; :: thesis: verum

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; :: thesis: verum