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

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

let K be Subset of AP; :: according to AFF_2:def 9 :: thesis: for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds

a,b // a9,b9

let o, a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K implies a,b // a9,b9 )

assume that

A2: K is being_line and

A3: o in K and

A4: c in K and

A5: c9 in K and

A6: not a in K and

A7: o <> c and

A8: a <> b and

A9: LIN o,a,a9 and

A10: LIN o,b,b9 and

A11: b,c // b9,c9 and

A12: a,c // a9,c9 and

A13: a,b // K ; :: thesis: a,b // a9,b9

set A = Line (o,a);

set P = Line (o,b);

A14: ( Line (o,a) is being_line & a in Line (o,a) ) by A3, A6, AFF_1:24;

A15: o in Line (o,a) by A3, A6, AFF_1:24;

then A16: a9 in Line (o,a) by A3, A6, A9, A14, AFF_1:25;

A17: o <> b by A3, A6, A13, AFF_1:35;

then A18: Line (o,b) is being_line by AFF_1:24;

consider N being Subset of AP such that

A19: a9 in N and

A20: K // N by A2, AFF_1:49;

A21: N is being_line by A20, AFF_1:36;

set T = Line (b9,c9);

A22: not b in K by A6, A13, AFF_1:35;

A23: b in Line (o,b) by A17, AFF_1:24;

A24: o in Line (o,b) by A17, AFF_1:24;

then A25: b9 in Line (o,b) by A10, A17, A18, A23, AFF_1:25;

assume A26: not a,b // a9,b9 ; :: thesis: contradiction

then A27: a9 <> b9 by AFF_1:3;

A28: not b9 in K

A33: b9 in Line (b9,c9) by A5, A28, AFF_1:24;

A34: c9 in Line (b9,c9) by A5, A28, AFF_1:24;

not N // Line (b9,c9)

A35: x in N and

A36: x in Line (b9,c9) by A32, A21, AFF_1:58;

a9,x // K by A19, A20, A35, AFF_1:40;

then A37: a,b // a9,x by A2, A13, AFF_1:31;

LIN c9,b9,x by A32, A33, A34, A36, AFF_1:21;

then c9,b9 // c9,x by AFF_1:def 1;

then b9,c9 // x,c9 by AFF_1:4;

then b,c // x,c9 by A5, A11, A28, AFF_1:5;

then LIN o,b,x by A1, A2, A3, A4, A5, A6, A7, A8, A9, A12, A13, A37;

then x in Line (o,b) by A17, A18, A24, A23, AFF_1:25;

then Line (o,b) = Line (b9,c9) by A26, A18, A25, A32, A33, A36, A37, AFF_1:18;

then LIN c9,b9,b by A18, A23, A33, A34, AFF_1:21;

then c9,b9 // c9,b by AFF_1:def 1;

then b9,c9 // b,c9 by AFF_1:4;

then b,c // b,c9 by A5, A11, A28, AFF_1:5;

then LIN b,c,c9 by AFF_1:def 1;

then A38: LIN c,c9,b by AFF_1:6;

then a,c // a9,c by A2, A4, A5, A12, A22, AFF_1:25;

then c,a // c,a9 by AFF_1:4;

then LIN c,a,a9 by AFF_1:def 1;

then LIN a,a9,c by AFF_1:6;

then A39: ( a = a9 or c in Line (o,a) ) by A14, A16, AFF_1:25;

b,c // b9,c by A2, A4, A5, A11, A22, A38, AFF_1:25;

then c,b // c,b9 by AFF_1:4;

then LIN c,b,b9 by AFF_1:def 1;

then LIN b,b9,c by AFF_1:6;

then ( b = b9 or c in Line (o,b) ) by A18, A23, A25, AFF_1:25;

hence contradiction by A2, A3, A4, A6, A7, A26, A22, A18, A15, A14, A24, A23, A39, AFF_1:2, AFF_1:18; :: thesis: verum

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

let K be Subset of AP; :: according to AFF_2:def 9 :: thesis: for o, a, b, c, a9, b9, c9 being Element of AP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K holds

a,b // a9,b9

let o, a, b, c, a9, b9, c9 be Element of AP; :: thesis: ( K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN o,a,a9 & LIN o,b,b9 & b,c // b9,c9 & a,c // a9,c9 & a,b // K implies a,b // a9,b9 )

assume that

A2: K is being_line and

A3: o in K and

A4: c in K and

A5: c9 in K and

A6: not a in K and

A7: o <> c and

A8: a <> b and

A9: LIN o,a,a9 and

A10: LIN o,b,b9 and

A11: b,c // b9,c9 and

A12: a,c // a9,c9 and

A13: a,b // K ; :: thesis: a,b // a9,b9

set A = Line (o,a);

set P = Line (o,b);

A14: ( Line (o,a) is being_line & a in Line (o,a) ) by A3, A6, AFF_1:24;

A15: o in Line (o,a) by A3, A6, AFF_1:24;

then A16: a9 in Line (o,a) by A3, A6, A9, A14, AFF_1:25;

A17: o <> b by A3, A6, A13, AFF_1:35;

then A18: Line (o,b) is being_line by AFF_1:24;

consider N being Subset of AP such that

A19: a9 in N and

A20: K // N by A2, AFF_1:49;

A21: N is being_line by A20, AFF_1:36;

set T = Line (b9,c9);

A22: not b in K by A6, A13, AFF_1:35;

A23: b in Line (o,b) by A17, AFF_1:24;

A24: o in Line (o,b) by A17, AFF_1:24;

then A25: b9 in Line (o,b) by A10, A17, A18, A23, AFF_1:25;

assume A26: not a,b // a9,b9 ; :: thesis: contradiction

then A27: a9 <> b9 by AFF_1:3;

A28: not b9 in K

proof

then A32:
Line (b9,c9) is being_line
by A5, AFF_1:24;
A29:
a9,c9 // a,c
by A12, AFF_1:4;

A30: b9,c9 // c,b by A11, AFF_1:4;

assume A31: b9 in K ; :: thesis: contradiction

then b9 = o by A2, A3, A22, A18, A24, A23, A25, AFF_1:18;

then c9 in Line (o,a) by A2, A3, A4, A5, A22, A15, A30, AFF_1:48;

then ( a9 = c9 or c in Line (o,a) ) by A14, A16, A29, AFF_1:48;

hence contradiction by A2, A3, A4, A5, A6, A7, A27, A22, A15, A14, A31, A30, AFF_1:18, AFF_1:48; :: thesis: verum

end;A30: b9,c9 // c,b by A11, AFF_1:4;

assume A31: b9 in K ; :: thesis: contradiction

then b9 = o by A2, A3, A22, A18, A24, A23, A25, AFF_1:18;

then c9 in Line (o,a) by A2, A3, A4, A5, A22, A15, A30, AFF_1:48;

then ( a9 = c9 or c in Line (o,a) ) by A14, A16, A29, AFF_1:48;

hence contradiction by A2, A3, A4, A5, A6, A7, A27, A22, A15, A14, A31, A30, AFF_1:18, AFF_1:48; :: thesis: verum

A33: b9 in Line (b9,c9) by A5, A28, AFF_1:24;

A34: c9 in Line (b9,c9) by A5, A28, AFF_1:24;

not N // Line (b9,c9)

proof

then consider x being Element of AP such that
assume
N // Line (b9,c9)
; :: thesis: contradiction

then K // Line (b9,c9) by A20, AFF_1:44;

hence contradiction by A5, A28, A33, A34, AFF_1:45; :: thesis: verum

end;then K // Line (b9,c9) by A20, AFF_1:44;

hence contradiction by A5, A28, A33, A34, AFF_1:45; :: thesis: verum

A35: x in N and

A36: x in Line (b9,c9) by A32, A21, AFF_1:58;

a9,x // K by A19, A20, A35, AFF_1:40;

then A37: a,b // a9,x by A2, A13, AFF_1:31;

LIN c9,b9,x by A32, A33, A34, A36, AFF_1:21;

then c9,b9 // c9,x by AFF_1:def 1;

then b9,c9 // x,c9 by AFF_1:4;

then b,c // x,c9 by A5, A11, A28, AFF_1:5;

then LIN o,b,x by A1, A2, A3, A4, A5, A6, A7, A8, A9, A12, A13, A37;

then x in Line (o,b) by A17, A18, A24, A23, AFF_1:25;

then Line (o,b) = Line (b9,c9) by A26, A18, A25, A32, A33, A36, A37, AFF_1:18;

then LIN c9,b9,b by A18, A23, A33, A34, AFF_1:21;

then c9,b9 // c9,b by AFF_1:def 1;

then b9,c9 // b,c9 by AFF_1:4;

then b,c // b,c9 by A5, A11, A28, AFF_1:5;

then LIN b,c,c9 by AFF_1:def 1;

then A38: LIN c,c9,b by AFF_1:6;

then a,c // a9,c by A2, A4, A5, A12, A22, AFF_1:25;

then c,a // c,a9 by AFF_1:4;

then LIN c,a,a9 by AFF_1:def 1;

then LIN a,a9,c by AFF_1:6;

then A39: ( a = a9 or c in Line (o,a) ) by A14, A16, AFF_1:25;

b,c // b9,c by A2, A4, A5, A11, A22, A38, AFF_1:25;

then c,b // c,b9 by AFF_1:4;

then LIN c,b,b9 by AFF_1:def 1;

then LIN b,b9,c by AFF_1:6;

then ( b = b9 or c in Line (o,b) ) by A18, A23, A25, AFF_1:25;

hence contradiction by A2, A3, A4, A6, A7, A26, A22, A18, A15, A14, A24, A23, A39, AFF_1:2, AFF_1:18; :: thesis: verum