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

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

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

c9 in K

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

assume that

A2: K is being_line and

A3: o in K and

A4: c in K and

A5: not a in K and

A6: o <> c and

A7: a <> b and

A8: LIN o,a,a9 and

A9: LIN o,b,b9 and

A10: a,b // a9,b9 and

A11: a,c // a9,c9 and

A12: b,c // b9,c9 and

A13: a,b // K ; :: thesis: c9 in K

set A = Line (o,a);

set P = Line (o,b);

set N = Line (b,c);

A14: o in Line (o,a) by A3, A5, AFF_1:24;

A15: not LIN a,b,c

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

A18: a9,b9 // b,a by A10, AFF_1:4;

A19: b <> c by A4, A5, A13, AFF_1:35;

then A20: ( b in Line (b,c) & c in Line (b,c) ) by AFF_1:24;

A21: a in Line (o,a) by A3, A5, AFF_1:24;

A22: Line (o,a) is being_line by A3, A5, AFF_1:24;

A23: Line (o,a) <> Line (o,b)

A25: Line (o,b) is being_line by A16, AFF_1:24;

A26: o in Line (o,b) by A16, AFF_1:24;

then A27: b9 in Line (o,b) by A9, A16, A25, A17, AFF_1:25;

A28: a9 in Line (o,a) by A3, A5, A8, A22, A14, A21, AFF_1:25;

A29: a9 <> b9

A33: x in K and

A34: LIN a9,c9,x by A2, AFF_1:59;

a9,c9 // a9,x by A34, AFF_1:def 1;

then A35: a,c // a9,x by A11, A31, AFF_1:5;

Line (b,c) is being_line by A19, AFF_1:24;

then consider T being Subset of AP such that

A36: x in T and

A37: Line (b,c) // T by AFF_1:49;

A38: not b in K by A5, A13, AFF_1:35;

A39: not T // Line (o,b)

then consider y being Element of AP such that

A40: y in T and

A41: y in Line (o,b) by A25, A39, AFF_1:58;

A42: b,c // y,x by A20, A36, A37, A40, AFF_1:39;

then a,b // a9,y by A1, A2, A3, A4, A5, A6, A7, A8, A13, A33, A42, A35;

then a9,b9 // a9,y by A7, A10, AFF_1:5;

then LIN a9,b9,y by AFF_1:def 1;

then LIN b9,y,a9 by AFF_1:6;

then a9 in Line (o,b) by A25, A27, A41, A43, AFF_1:25;

then a in Line (o,b) by A25, A17, A27, A29, A18, AFF_1:48;

hence contradiction by A3, A5, A25, A26, A23, AFF_1:24; :: thesis: verum

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

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

c9 in K

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

assume that

A2: K is being_line and

A3: o in K and

A4: c in K and

A5: not a in K and

A6: o <> c and

A7: a <> b and

A8: LIN o,a,a9 and

A9: LIN o,b,b9 and

A10: a,b // a9,b9 and

A11: a,c // a9,c9 and

A12: b,c // b9,c9 and

A13: a,b // K ; :: thesis: c9 in K

set A = Line (o,a);

set P = Line (o,b);

set N = Line (b,c);

A14: o in Line (o,a) by A3, A5, AFF_1:24;

A15: not LIN a,b,c

proof

A16:
o <> b
by A3, A5, A13, AFF_1:35;
assume
LIN a,b,c
; :: thesis: contradiction

then a,b // a,c by AFF_1:def 1;

then a,c // K by A7, A13, AFF_1:32;

then c,a // K by AFF_1:34;

hence contradiction by A2, A4, A5, AFF_1:23; :: thesis: verum

end;then a,b // a,c by AFF_1:def 1;

then a,c // K by A7, A13, AFF_1:32;

then c,a // K by AFF_1:34;

hence contradiction by A2, A4, A5, AFF_1:23; :: thesis: verum

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

A18: a9,b9 // b,a by A10, AFF_1:4;

A19: b <> c by A4, A5, A13, AFF_1:35;

then A20: ( b in Line (b,c) & c in Line (b,c) ) by AFF_1:24;

A21: a in Line (o,a) by A3, A5, AFF_1:24;

A22: Line (o,a) is being_line by A3, A5, AFF_1:24;

A23: Line (o,a) <> Line (o,b)

proof

assume A24:
not c9 in K
; :: thesis: contradiction
assume
Line (o,a) = Line (o,b)
; :: thesis: contradiction

then a,b // Line (o,a) by A22, A21, A17, AFF_1:40, AFF_1:41;

hence contradiction by A3, A5, A7, A13, A14, A21, AFF_1:45, AFF_1:53; :: thesis: verum

end;then a,b // Line (o,a) by A22, A21, A17, AFF_1:40, AFF_1:41;

hence contradiction by A3, A5, A7, A13, A14, A21, AFF_1:45, AFF_1:53; :: thesis: verum

A25: Line (o,b) is being_line by A16, AFF_1:24;

A26: o in Line (o,b) by A16, AFF_1:24;

then A27: b9 in Line (o,b) by A9, A16, A25, A17, AFF_1:25;

A28: a9 in Line (o,a) by A3, A5, A8, A22, A14, A21, AFF_1:25;

A29: a9 <> b9

proof

A31:
a9 <> c9
assume A30:
a9 = b9
; :: thesis: contradiction

then ( a,c // b,c or a9 = c9 ) by A11, A12, AFF_1:5;

then ( c,a // c,b or a9 = c9 ) by AFF_1:4;

then ( LIN c,a,b or a9 = c9 ) by AFF_1:def 1;

hence contradiction by A3, A24, A15, A22, A25, A14, A26, A28, A27, A23, A30, AFF_1:6, AFF_1:18; :: thesis: verum

end;then ( a,c // b,c or a9 = c9 ) by A11, A12, AFF_1:5;

then ( c,a // c,b or a9 = c9 ) by AFF_1:4;

then ( LIN c,a,b or a9 = c9 ) by AFF_1:def 1;

hence contradiction by A3, A24, A15, A22, A25, A14, A26, A28, A27, A23, A30, AFF_1:6, AFF_1:18; :: thesis: verum

proof

not a9,c9 // K
assume
a9 = c9
; :: thesis: contradiction

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

then a,b // b,c by A10, A29, 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 A15, AFF_1:6; :: thesis: verum

end;then b,c // a9,b9 by A12, AFF_1:4;

then a,b // b,c by A10, A29, 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 A15, AFF_1:6; :: thesis: verum

proof

then consider x being Element of AP such that
assume A32:
a9,c9 // K
; :: thesis: contradiction

a9,c9 // a,c by A11, AFF_1:4;

then a,c // K by A31, A32, AFF_1:32;

then c,a // K by AFF_1:34;

hence contradiction by A2, A4, A5, AFF_1:23; :: thesis: verum

end;a9,c9 // a,c by A11, AFF_1:4;

then a,c // K by A31, A32, AFF_1:32;

then c,a // K by AFF_1:34;

hence contradiction by A2, A4, A5, AFF_1:23; :: thesis: verum

A33: x in K and

A34: LIN a9,c9,x by A2, AFF_1:59;

a9,c9 // a9,x by A34, AFF_1:def 1;

then A35: a,c // a9,x by A11, A31, AFF_1:5;

Line (b,c) is being_line by A19, AFF_1:24;

then consider T being Subset of AP such that

A36: x in T and

A37: Line (b,c) // T by AFF_1:49;

A38: not b in K by A5, A13, AFF_1:35;

A39: not T // Line (o,b)

proof

T is being_line
by A37, AFF_1:36;
assume
T // Line (o,b)
; :: thesis: contradiction

then Line (b,c) // Line (o,b) by A37, AFF_1:44;

then c in Line (o,b) by A17, A20, AFF_1:45;

hence contradiction by A2, A3, A4, A6, A38, A25, A26, A17, AFF_1:18; :: thesis: verum

end;then Line (b,c) // Line (o,b) by A37, AFF_1:44;

then c in Line (o,b) by A17, A20, AFF_1:45;

hence contradiction by A2, A3, A4, A6, A38, A25, A26, A17, AFF_1:18; :: thesis: verum

then consider y being Element of AP such that

A40: y in T and

A41: y in Line (o,b) by A25, A39, AFF_1:58;

A42: b,c // y,x by A20, A36, A37, A40, AFF_1:39;

A43: now :: thesis: not y = b9

LIN o,b,y
by A25, A26, A17, A41, AFF_1:21;assume
y = b9
; :: thesis: contradiction

then b9,c9 // b9,x by A12, A19, A42, AFF_1:5;

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

then A44: LIN c9,x,b9 by AFF_1:6;

( LIN c9,x,a9 & LIN c9,x,c9 ) by A34, AFF_1:6, AFF_1:7;

then LIN a9,b9,c9 by A24, A33, A44, AFF_1:8;

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

then a9,b9 // a,c by A11, A31, AFF_1:5;

then a,b // a,c by A10, A29, AFF_1:5;

hence contradiction by A15, AFF_1:def 1; :: thesis: verum

end;then b9,c9 // b9,x by A12, A19, A42, AFF_1:5;

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

then A44: LIN c9,x,b9 by AFF_1:6;

( LIN c9,x,a9 & LIN c9,x,c9 ) by A34, AFF_1:6, AFF_1:7;

then LIN a9,b9,c9 by A24, A33, A44, AFF_1:8;

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

then a9,b9 // a,c by A11, A31, AFF_1:5;

then a,b // a,c by A10, A29, AFF_1:5;

hence contradiction by A15, AFF_1:def 1; :: thesis: verum

then a,b // a9,y by A1, A2, A3, A4, A5, A6, A7, A8, A13, A33, A42, A35;

then a9,b9 // a9,y by A7, A10, AFF_1:5;

then LIN a9,b9,y by AFF_1:def 1;

then LIN b9,y,a9 by AFF_1:6;

then a9 in Line (o,b) by A25, A27, A41, A43, AFF_1:25;

then a in Line (o,b) by A25, A17, A27, A29, A18, AFF_1:48;

hence contradiction by A3, A5, A25, A26, A23, AFF_1:24; :: thesis: verum