let AP be AffinPlane; :: thesis: ( AP is satisfying_DES2_1 implies AP is satisfying_DES2 )
assume A1: AP is satisfying_DES2_1 ; :: thesis: AP is satisfying_DES2
let A be Subset of AP; :: according to AFF_3:def 5 :: thesis: for P, C being Subset of AP
for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds
a,c // p,q
let P, C be Subset of AP; :: thesis: for a, a9, b, b9, c, c9, p, q being Element of AP st A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds
a,c // p,q
let a, a9, b, b9, c, c9, p, q be Element of AP; :: thesis: ( A is being_line & P is being_line & C is being_line & A <> P & A <> C & P <> C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A // P & A // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 implies a,c // p,q )
assume that
A2: A is being_line and
A3: P is being_line and
A4: C is being_line and
A5: A <> P and
A6: A <> C and
A7: P <> C and
A8: a in A and
A9: a9 in A and
A10: b in P and
A11: b9 in P and
A12: c in C and
A13: c9 in C and
A14: A // P and
A15: A // C and
A16: not LIN b,a,c and
A17: not LIN b9,a9,c9 and
A18: p <> q and
A19: a <> a9 and
A20: LIN b,a,p and
A21: LIN b9,a9,p and
A22: ( LIN b,c,q & LIN b9,c9,q ) and
A23: a,c // a9,c9 ; :: thesis: a,c // p,q
A24: P // C by A14, A15, AFF_1:44;
set P9 = Line (b9,a9);
A25: p in Line (b9,a9) by A21, AFF_1:def 2;
a9 <> b9 by A17, AFF_1:7;
then A26: Line (b9,a9) is being_line by AFF_1:def 3;
set K = Line (a,c);
set N = Line (a9,c9);
set D = Line (b,c);
set T = Line (b9,c9);
A27: ( q in Line (b,c) & q in Line (b9,c9) ) by A22, AFF_1:def 2;
A28: c9 in Line (a9,c9) by AFF_1:15;
b <> c by A16, AFF_1:7;
then A29: Line (b,c) is being_line by AFF_1:def 3;
b9 <> c9 by A17, AFF_1:7;
then A30: Line (b9,c9) is being_line by AFF_1:def 3;
A31: a <> c by A16, AFF_1:7;
then A32: Line (a,c) is being_line by AFF_1:def 3;
A33: a9 <> c9 by A17, AFF_1:7;
then A34: Line (a9,c9) is being_line by AFF_1:def 3;
then consider M being Subset of AP such that
A35: p in M and
A36: Line (a9,c9) // M by AFF_1:49;
A37: Line (a,c) // Line (a9,c9) by A23, A31, A33, AFF_1:37;
then A38: Line (a,c) // M by A36, AFF_1:44;
A39: c in Line (b,c) by AFF_1:15;
A40: b in Line (b,c) by AFF_1:15;
set A9 = Line (b,a);
A41: p in Line (b,a) by A20, AFF_1:def 2;
a <> b by A16, AFF_1:7;
then A42: Line (b,a) is being_line by AFF_1:def 3;
A43: c9 in Line (b9,c9) by AFF_1:15;
A44: b9 in Line (b9,c9) by AFF_1:15;
A45: a9 in Line (a9,c9) by AFF_1:15;
A46: a in Line (a,c) by AFF_1:15;
A47: a9 in Line (b9,a9) by AFF_1:15;
A48: b9 in Line (b9,a9) by AFF_1:15;
A49: a in Line (b,a) by AFF_1:15;
A50: b in Line (b,a) by AFF_1:15;
A51: c in Line (a,c) by AFF_1:15;
then A52: Line (a,c) <> A by A6, A12, A15, AFF_1:45;
A53: c <> c9

proof

assume c = c9 ; :: thesis: contradiction
then Line (a,c) = Line (a9,c9) by A51, A28, A37, AFF_1:45;
hence contradiction by A2, A8, A9, A19, A32, A46, A45, A52, AFF_1:18; :: thesis: verum

end;

A54: Line (b,c) <> Line (b9,c9)

proof

assume Line (b,c) = Line (b9,c9) ; :: thesis: contradiction
then Line (b,c) = C by A4, A12, A13, A29, A39, A43, A53, AFF_1:18;
hence contradiction by A7, A10, A24, A40, AFF_1:45; :: thesis: verum

end;

A55: b <> b9

proof

A56: Line (b,a) <> Line (b9,a9)

proof

assume Line (b,a) = Line (b9,a9) ; :: thesis: contradiction
then Line (b,a) = A by A2, A8, A9, A19, A42, A49, A47, AFF_1:18;
hence contradiction by A5, A10, A14, A50, AFF_1:45; :: thesis: verum

end;

assume A57: b = b9 ; :: thesis: contradiction
then b9 = q by A29, A30, A40, A44, A27, A54, AFF_1:18;
hence contradiction by A18, A42, A26, A50, A41, A48, A25, A57, A56, AFF_1:18; :: thesis: verum

end;

A58: M is being_line by A36, AFF_1:36;

A59: now :: thesis: ( not Line (b9,c9) // M implies a,c // p,q )

assume not Line (b9,c9) // M ; :: thesis: a,c // p,q
then consider x being Element of AP such that
A60: x in Line (b9,c9) and
A61: x in M by A30, A58, AFF_1:58;
A62: p <> x

proof

assume p = x ; :: thesis: contradiction
then ( p = b9 or Line (b9,c9) = Line (b9,a9) ) by A30, A44, A26, A48, A25, A60, AFF_1:18;
then ( LIN b,b9,a or c9 in Line (b9,a9) ) by A42, A50, A49, A41, AFF_1:15, AFF_1:21;
then a in P by A3, A10, A11, A17, A55, AFF_1:25, AFF_1:def 2;
hence contradiction by A5, A8, A14, AFF_1:45; :: thesis: verum

end;

not b,x // C

proof

assume A63: b,x // C ; :: thesis: contradiction
C // P by A14, A15, AFF_1:44;
then b,x // P by A63, AFF_1:43;
then x in P by A3, A10, AFF_1:23;
then ( b9 in M or c9 in P ) by A3, A11, A30, A44, A43, A60, A61, AFF_1:18;
then ( b9 = p or M = Line (b9,a9) ) by A7, A13, A24, A26, A48, A25, A35, A58, AFF_1:18, AFF_1:45;
then ( LIN b,b9,a or Line (a9,c9) // Line (b9,a9) ) by A20, A36, AFF_1:6;
then ( a in P or Line (a9,c9) = Line (b9,a9) ) by A3, A10, A11, A45, A47, A55, AFF_1:25, AFF_1:45;
hence contradiction by A5, A8, A14, A17, A28, AFF_1:45, AFF_1:def 2; :: thesis: verum

end;

then consider y being Element of AP such that
A64: y in C and
A65: LIN b,x,y by A4, AFF_1:59;
A66: LIN b,y,x by A65, AFF_1:6;
A67: not LIN b,a,y

proof

A68: now :: thesis: not x = p

assume x = p ; :: thesis: contradiction
then ( p = b9 or Line (b9,c9) = Line (b9,a9) ) by A30, A44, A26, A48, A25, A60, AFF_1:18;
then ( LIN b,b9,a or c9 in Line (b9,a9) ) by A42, A50, A49, A41, AFF_1:15, AFF_1:21;
then a in P by A3, A10, A11, A17, A55, AFF_1:25, AFF_1:def 2;
hence contradiction by A5, A8, A14, AFF_1:45; :: thesis: verum

end;

assume LIN b,a,y ; :: thesis: contradiction
then A69: LIN b,y,a by AFF_1:6;
LIN b,y,b by AFF_1:7;
then ( b = y or LIN a,b,x ) by A66, A69, AFF_1:8;
then x in Line (b,a) by A7, A10, A24, A64, AFF_1:45, AFF_1:def 2;
then ( x = p or Line (b,a) = M ) by A42, A41, A35, A58, A61, AFF_1:18;
then Line (a,c) = Line (b,a) by A46, A49, A38, A68, AFF_1:45;
hence contradiction by A16, A51, AFF_1:def 2; :: thesis: verum

end;

( LIN b9,c9,x & a9,c9 // p,x ) by A30, A45, A28, A44, A43, A35, A36, A60, A61, AFF_1:21, AFF_1:39;
then a9,c9 // a,y by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A13, A14, A15, A17, A20, A21, A64, A66, A67, A62;
then a,c // a,y by A23, A33, AFF_1:5;
then LIN a,c,y by AFF_1:def 1;
then y in Line (a,c) by AFF_1:def 2;
then ( Line (a,c) = C or y = c ) by A4, A12, A32, A51, A64, AFF_1:18;
then ( a in C or LIN b,c,x ) by A65, AFF_1:6, AFF_1:15;
then x in Line (b,c) by A6, A8, A15, AFF_1:45, AFF_1:def 2;
then ( q in M or c9 in Line (b,c) ) by A29, A30, A43, A27, A60, A61, AFF_1:18;
then ( a,c // p,q or LIN c,c9,b ) by A29, A46, A51, A40, A39, A35, A38, AFF_1:21, AFF_1:39;
then ( a,c // p,q or b in C ) by A4, A12, A13, A53, AFF_1:25;
hence a,c // p,q by A7, A10, A24, AFF_1:45; :: thesis: verum

end;

A70: now :: thesis: ( not M // Line (b,c) implies a,c // p,q )

assume not M // Line (b,c) ; :: thesis: a,c // p,q
then consider x being Element of AP such that
A71: x in M and
A72: x in Line (b,c) by A29, A58, AFF_1:58;
A73: p <> x

proof

assume p = x ; :: thesis: contradiction
then ( p = b or Line (b,c) = Line (b,a) ) by A29, A40, A42, A50, A41, A72, AFF_1:18;
then ( LIN b,b9,a9 or c in Line (b,a) ) by A26, A48, A47, A25, AFF_1:15, AFF_1:21;
then a9 in P by A3, A10, A11, A16, A55, AFF_1:25, AFF_1:def 2;
hence contradiction by A5, A9, A14, AFF_1:45; :: thesis: verum

end;

not b9,x // C

proof

A74: now :: thesis: not b = p

assume b = p ; :: thesis: contradiction
then LIN b,b9,a9 by A26, A48, A47, A25, AFF_1:21;
then a9 in P by A3, A10, A11, A55, AFF_1:25;
hence contradiction by A5, A9, A14, AFF_1:45; :: thesis: verum

end;

assume A75: b9,x // C ; :: thesis: contradiction
C // P by A14, A15, AFF_1:44;
then b9,x // P by A75, AFF_1:43;
then x in P by A3, A11, AFF_1:23;
then ( x = b or Line (b,c) = P ) by A3, A10, A29, A40, A72, AFF_1:18;
then ( b = p or M = Line (b,a) ) by A7, A12, A24, A39, A42, A50, A41, A35, A58, A71, AFF_1:18, AFF_1:45;
then b in Line (a,c) by A46, A50, A49, A38, A74, AFF_1:45;
hence contradiction by A16, A32, A46, A51, AFF_1:21; :: thesis: verum

end;

then consider y being Element of AP such that
A76: y in C and
A77: LIN b9,x,y by A4, AFF_1:59;
A78: LIN b9,y,x by A77, AFF_1:6;
A79: not LIN b9,a9,y

proof

A80: now :: thesis: not x = p

assume x = p ; :: thesis: contradiction
then ( p = b or Line (b,c) = Line (b,a) ) by A29, A40, A42, A50, A41, A72, AFF_1:18;
then ( LIN b,b9,a9 or c in Line (b,a) ) by A26, A48, A47, A25, AFF_1:15, AFF_1:21;
then a9 in P by A3, A10, A11, A16, A55, AFF_1:25, AFF_1:def 2;
hence contradiction by A5, A9, A14, AFF_1:45; :: thesis: verum

end;

assume LIN b9,a9,y ; :: thesis: contradiction
then A81: LIN b9,y,a9 by AFF_1:6;
LIN b9,y,b9 by AFF_1:7;
then ( b9 = y or LIN a9,b9,x ) by A78, A81, AFF_1:8;
then x in Line (b9,a9) by A7, A11, A24, A76, AFF_1:45, AFF_1:def 2;
then ( x = p or Line (b9,a9) = M ) by A26, A25, A35, A58, A71, AFF_1:18;
then Line (a9,c9) = Line (b9,a9) by A45, A47, A36, A80, AFF_1:45;
hence contradiction by A17, A28, AFF_1:def 2; :: thesis: verum

end;

( LIN b,c,x & a,c // p,x ) by A29, A46, A51, A40, A39, A35, A38, A71, A72, AFF_1:21, AFF_1:39;
then a,c // a9,y by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A14, A15, A16, A20, A21, A76, A78, A79, A73;
then a9,y // a9,c9 by A23, A31, AFF_1:5;
then LIN a9,y,c9 by AFF_1:def 1;
then LIN a9,c9,y by AFF_1:6;
then y in Line (a9,c9) by AFF_1:def 2;
then ( Line (a9,c9) = C or y = c9 ) by A4, A13, A34, A28, A76, AFF_1:18;
then ( a9 in C or LIN b9,c9,x ) by A77, AFF_1:6, AFF_1:15;
then x in Line (b9,c9) by A6, A9, A15, AFF_1:45, AFF_1:def 2;
then ( q in M or c9 in Line (b,c) ) by A29, A30, A43, A27, A71, A72, AFF_1:18;
then ( a,c // p,q or LIN c,c9,b ) by A29, A46, A51, A40, A39, A35, A38, AFF_1:21, AFF_1:39;
then ( a,c // p,q or b in C ) by A4, A12, A13, A53, AFF_1:25;
hence a,c // p,q by A7, A10, A24, AFF_1:45; :: thesis: verum

end;

( not M // Line (b,c) or not Line (b9,c9) // M )

proof

assume ( M // Line (b,c) & Line (b9,c9) // M ) ; :: thesis: contradiction
then Line (b9,c9) // Line (b,c) by AFF_1:44;
hence contradiction by A27, A54, AFF_1:45; :: thesis: verum

end;

hence a,c // p,q by A70, A59; :: thesis: verum