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