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
thus AP is satisfying_TDES_3 :: thesis: verum

proof

let K be Subset of ; :: according to AFF_2:def 10 :: thesis: for o, a, b, c, a', b', c' being Element of st K is being_line & o in K & c in K & not a in K & o <> c & a <> b & LIN o,a,a' & LIN o,b,b' & a,b // a',b' & a,c // a',c' & b,c // b',c' & a,b // K holds
c' in K
let o, a, b, c, a', b', c' be Element of ; :: thesis: ( K is being_line & o in K & c in K & not a in K & o <> c & a <> b & LIN o,a,a' & LIN o,b,b' & a,b // a',b' & a,c // a',c' & b,c // b',c' & a,b // K implies c' 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,a' and
A9: LIN o,b,b' and
A10: a,b // a',b' and
A11: a,c // a',c' and
A12: b,c // b',c' and
A13: a,b // K ; :: thesis: c' 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:38;
A15: not LIN a,b,c

proof

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:46;
then c,a // K by AFF_1:48;
hence contradiction by A2, A4, A5, AFF_1:37; :: thesis: verum

end;

A16: o <> b by A3, A5, A13, AFF_1:49;
then A17: b in Line o,b by AFF_1:38;
A18: a',b' // b,a by A10, AFF_1:13;
A19: b <> c by A4, A5, A13, AFF_1:49;
then A20: ( b in Line b,c & c in Line b,c ) by AFF_1:38;
A21: a in Line o,a by A3, A5, AFF_1:38;
A22: Line o,a is being_line by A3, A5, AFF_1:38;
A23: Line o,a <> Line o,b

proof

assume Line o,a = Line o,b ; :: thesis: contradiction
then a,b // Line o,a by A22, A21, A17, AFF_1:54, AFF_1:55;
hence contradiction by A3, A5, A7, A13, A14, A21, AFF_1:59, AFF_1:67; :: thesis: verum

end;

assume A24: not c' in K ; :: thesis: contradiction
A25: Line o,b is being_line by A16, AFF_1:38;
A26: o in Line o,b by A16, AFF_1:38;
then A27: b' in Line o,b by A9, A16, A25, A17, AFF_1:39;
A28: a' in Line o,a by A3, A5, A8, A22, A14, A21, AFF_1:39;
A29: a' <> b'

proof

assume A30: a' = b' ; :: thesis: contradiction
then ( a,c // b,c or a' = c' ) by A11, A12, AFF_1:14;
then ( c,a // c,b or a' = c' ) by AFF_1:13;
then ( LIN c,a,b or a' = c' ) by AFF_1:def 1;
hence contradiction by A3, A24, A15, A22, A25, A14, A26, A28, A27, A23, A30, AFF_1:15, AFF_1:30; :: thesis: verum

end;

A31: a' <> c'

proof

assume a' = c' ; :: thesis: contradiction
then b,c // a',b' by A12, AFF_1:13;
then a,b // b,c by A10, A29, AFF_1:14;
then b,a // b,c by AFF_1:13;
then LIN b,a,c by AFF_1:def 1;
hence contradiction by A15, AFF_1:15; :: thesis: verum

end;

not a',c' // K

proof

assume A32: a',c' // K ; :: thesis: contradiction
a',c' // a,c by A11, AFF_1:13;
then a,c // K by A31, A32, AFF_1:46;
then c,a // K by AFF_1:48;
hence contradiction by A2, A4, A5, AFF_1:37; :: thesis: verum

end;

then consider x being Element of such that
A33: x in K and
A34: LIN a',c',x by A2, AFF_1:73;
a',c' // a',x by A34, AFF_1:def 1;
then A35: a,c // a',x by A11, A31, AFF_1:14;
Line b,c is being_line by A19, AFF_1:38;
then consider T being Subset of such that
A36: x in T and
A37: Line b,c // T by AFF_1:63;
A38: not b in K by A5, A13, AFF_1:49;
A39: not T // Line o,b

proof

assume T // Line o,b ; :: thesis: contradiction
then Line b,c // Line o,b by A37, AFF_1:58;
then c in Line o,b by A17, A20, AFF_1:59;
hence contradiction by A2, A3, A4, A6, A38, A25, A26, A17, AFF_1:30; :: thesis: verum

end;

T is being_line by A37, AFF_1:50;
then consider y being Element of such that
A40: y in T and
A41: y in Line o,b by A25, A39, AFF_1:72;
A42: b,c // y,x by A20, A36, A37, A40, AFF_1:53;

A43: now

assume y = b' ; :: thesis: contradiction
then b',c' // b',x by A12, A19, A42, AFF_1:14;
then LIN b',c',x by AFF_1:def 1;
then A44: LIN c',x,b' by AFF_1:15;
( LIN c',x,a' & LIN c',x,c' ) by A34, AFF_1:15, AFF_1:16;
then LIN a',b',c' by A24, A33, A44, AFF_1:17;
then a',b' // a',c' by AFF_1:def 1;
then a',b' // a,c by A11, A31, AFF_1:14;
then a,b // a,c by A10, A29, AFF_1:14;
hence contradiction by A15, AFF_1:def 1; :: thesis: verum

end;

LIN o,b,y by A25, A26, A17, A41, AFF_1:33;
then a,b // a',y by A1, A2, A3, A4, A5, A6, A7, A8, A13, A33, A42, A35, Def9;
then a',b' // a',y by A7, A10, AFF_1:14;
then LIN a',b',y by AFF_1:def 1;
then LIN b',y,a' by AFF_1:15;
then a' in Line o,b by A25, A27, A41, A43, AFF_1:39;
then a in Line o,b by A25, A17, A27, A29, A18, AFF_1:62;
hence contradiction by A3, A5, A25, A26, A23, AFF_1:38; :: thesis: verum

end;