let AP be AffinPlane; :: thesis: ( AP is satisfying_DES1_3 implies AP is satisfying_DES2_1 )
assume A1: AP is satisfying_DES1_3 ; :: thesis: AP is satisfying_DES2_1
let A be Subset of AP; :: according to AFF_3:def 6 :: 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 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds
a,c // a9,c9
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 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds
a,c // a9,c9
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 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q implies a,c // a9,c9 )
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: LIN b,a,p and
A20: LIN b9,a9,p and
A21: LIN b,c,q and
A22: LIN b9,c9,q and
A23: a,c // p,q ; :: thesis: a,c // a9,c9
A24: P // C by A14, A15, AFF_1:44;
set K = Line (p,q);
set M = Line (a,c);
set N = Line (a9,c9);
A25: a <> c by A16, AFF_1:7;
then A26: a in Line (a,c) by AFF_1:24;
A27: ( c,c9 // a,a9 & LIN q,c,b ) by A8, A9, A12, A13, A15, A21, AFF_1:6, AFF_1:39;
A28: LIN p,a9,b9 by A20, AFF_1:6;
C // P by A14, A15, AFF_1:44;
then A29: c,c9 // b,b9 by A10, A11, A12, A13, AFF_1:39;
A30: ( LIN q,c9,b9 & LIN p,a,b ) by A19, A22, AFF_1:6;
A31: c in Line (a,c) by A25, AFF_1:24;
assume A32: not a,c // a9,c9 ; :: thesis: contradiction
A33: c <> q
proof
assume A34: c = q ; :: thesis: contradiction
then c,a // c,p by A23, AFF_1:4;
then LIN c,a,p by AFF_1:def 1;
then A35: LIN p,a,c by AFF_1:6;
( LIN p,a,b & LIN p,a,a ) by A19, AFF_1:6, AFF_1:7;
then p = a by A16, A35, AFF_1:8;
then LIN a,a9,b9 by A20, AFF_1:6;
then A36: ( a = a9 or b9 in A ) by A2, A8, A9, AFF_1:25;
LIN c,c9,b9 by A22, A34, AFF_1:6;
then ( c = c9 or b9 in C ) by A4, A12, A13, AFF_1:25;
hence contradiction by A5, A7, A11, A14, A32, A24, A36, AFF_1:2, AFF_1:45; :: thesis: verum
end;
A37: c <> c9
proof
A38: now :: thesis: not p = b
assume A39: p = b ; :: thesis: contradiction
LIN b,q,c by A21, AFF_1:6;
then b,q // b,c by AFF_1:def 1;
then ( a,c // b,c or b = q ) by A23, A39, AFF_1:5;
then c,a // c,b by A18, A39, AFF_1:4;
then LIN c,a,b by AFF_1:def 1;
hence contradiction by A16, AFF_1:6; :: thesis: verum
end;
A40: ( LIN q,c,b & LIN q,c,c ) by A21, AFF_1:6, AFF_1:7;
assume A41: c = c9 ; :: thesis: contradiction
then LIN q,c,b9 by A22, AFF_1:6;
then ( b = b9 or c in P ) by A3, A10, A11, A33, A40, AFF_1:8, AFF_1:25;
then A42: LIN p,b,a9 by A7, A12, A20, A24, AFF_1:6, AFF_1:45;
( LIN p,b,a & LIN p,b,b ) by A19, AFF_1:6, AFF_1:7;
then ( a = a9 or b in A ) by A2, A8, A9, A42, A38, AFF_1:8, AFF_1:25;
hence contradiction by A5, A10, A14, A32, A41, AFF_1:2, AFF_1:45; :: thesis: verum
end;
A43: b <> b9
proof
assume b = b9 ; :: thesis: contradiction
then A44: LIN q,b,c9 by A22, AFF_1:6;
( LIN q,b,c & LIN q,b,b ) by A21, AFF_1:6, AFF_1:7;
then A45: ( q = b or b in C ) by A4, A12, A13, A37, A44, AFF_1:8, AFF_1:25;
b,a // b,p by A19, AFF_1:def 1;
then a,b // p,b by AFF_1:4;
then ( a,c // a,b or p = b ) by A7, A10, A23, A24, A45, AFF_1:5, AFF_1:45;
then LIN a,c,b by A7, A10, A18, A24, A45, AFF_1:45, AFF_1:def 1;
hence contradiction by A16, AFF_1:6; :: thesis: verum
end;
A46: not LIN q,c,c9
proof
assume A47: LIN q,c,c9 ; :: thesis: contradiction
( LIN q,c,b & LIN q,c,c ) by A21, AFF_1:6, AFF_1:7;
then b in C by A4, A12, A13, A33, A37, A47, AFF_1:8, AFF_1:25;
hence contradiction by A7, A10, A24, AFF_1:45; :: thesis: verum
end;
A48: a9 <> c9 by A17, AFF_1:7;
then A49: Line (a9,c9) is being_line by AFF_1:24;
A50: p <> a
proof
assume p = a ; :: thesis: contradiction
then LIN a,c,q by A23, AFF_1:def 1;
then A51: LIN c,q,a by AFF_1:6;
( LIN c,q,b & LIN c,q,c ) by A21, AFF_1:6, AFF_1:7;
hence contradiction by A16, A33, A51, AFF_1:8; :: thesis: verum
end;
A52: not LIN p,a,a9
proof
assume A53: LIN p,a,a9 ; :: thesis: contradiction
( LIN p,a,b & LIN p,a,a ) by A19, AFF_1:6, AFF_1:7;
then ( a = a9 or b in A ) by A2, A8, A9, A50, A53, AFF_1:8, AFF_1:25;
then A54: LIN p,a,b9 by A5, A10, A14, A20, AFF_1:6, AFF_1:45;
( LIN p,a,b & LIN p,a,a ) by A19, AFF_1:6, AFF_1:7;
then a in P by A3, A10, A11, A43, A50, A54, AFF_1:8, AFF_1:25;
hence contradiction by A5, A8, A14, AFF_1:45; :: thesis: verum
end;
A55: Line (a,c) is being_line by A25, AFF_1:24;
A56: ( Line (p,q) is being_line & q in Line (p,q) ) by A18, AFF_1:24;
A57: now :: thesis: not Line (a,c) = Line (p,q)
assume Line (a,c) = Line (p,q) ; :: thesis: contradiction
then A58: ( LIN q,c,a & LIN q,c,c ) by A56, A26, A31, AFF_1:21;
LIN q,c,b by A21, AFF_1:6;
hence contradiction by A16, A33, A58, AFF_1:8; :: thesis: verum
end;
A59: c9 in Line (a9,c9) by A48, AFF_1:24;
A60: a9 in Line (a9,c9) by A48, AFF_1:24;
then consider x being Element of AP such that
A61: x in Line (a,c) and
A62: x in Line (a9,c9) by A32, A55, A49, A26, A31, A59, AFF_1:39, AFF_1:58;
A63: now :: thesis: not x = c
assume x = c ; :: thesis: contradiction
then Line (a9,c9) = C by A4, A12, A13, A37, A49, A59, A62, AFF_1:18;
hence contradiction by A6, A9, A15, A60, AFF_1:45; :: thesis: verum
end;
A64: p in Line (p,q) by A18, AFF_1:24;
then A65: Line (a,c) // Line (p,q) by A18, A23, A25, A55, A56, A26, A31, AFF_1:38;
A66: now :: thesis: not x = c9
assume x = c9 ; :: thesis: contradiction
then Line (a,c) = C by A4, A12, A13, A37, A55, A31, A61, AFF_1:18;
hence contradiction by A6, A8, A15, A26, AFF_1:45; :: thesis: verum
end;
Line (a,c) <> Line (a9,c9) by A32, A55, A26, A31, A60, A59, AFF_1:51;
then x in Line (p,q) by A1, A18, A25, A55, A49, A64, A56, A26, A31, A60, A59, A61, A62, A29, A27, A30, A28, A43, A63, A66, A46, A52;
hence contradiction by A65, A61, A57, AFF_1:45; :: thesis: verum