let AP be AffinPlane; :: thesis: ( AP is satisfying_DES1_1 implies AP is satisfying_DES1 )
assume A1: AP is satisfying_DES1_1 ; :: thesis: AP is satisfying_DES1
let A be Subset of AP; :: according to AFF_3:def 1 :: thesis: for P, C being Subset of AP
for o, a, a', b, b', c, c', 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 & a' in A & o in P & b in P & b' in P & o in C & c in C & c' in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b',a',c' & a <> a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' holds
a,c // p,q
let P, C be Subset of AP; :: thesis: for o, a, a', b, b', c, c', 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 & a' in A & o in P & b in P & b' in P & o in C & c in C & c' in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b',a',c' & a <> a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' holds
a,c // p,q
let o, a, a', b, b', c, c', 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 & a' in A & o in P & b in P & b' in P & o in C & c in C & c' in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b',a',c' & a <> a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' implies a,c // p,q )
assume that
A2: ( A is being_line & P is being_line & C is being_line ) and
A3: ( P <> A & P <> C & A <> C ) and
A4: ( o in A & a in A & a' in A & o in P & b in P & b' in P & o in C & c in C & c' in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b',a',c' & a <> a' ) and
A5: ( LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' ) ; :: thesis: a,c // p,q
set K = Line b,a;
set M = Line b,c;
( b <> a & b <> c & a <> c ) by A4, AFF_1:16;
then A6: ( Line b,a is being_line & Line b,c is being_line & b in Line b,a & a in Line b,a & b in Line b,c & c in Line b,c & p in Line b,a & q in Line b,c ) by A5, AFF_1:26, AFF_1:def 2, AFF_1:def 3;
A7: ( a' <> b' & b' <> c' & a' <> c' ) by A4, AFF_1:16;
A8: Line b,a <> P by A2, A3, A4, A6, AFF_1:30;
A9: Line b,c <> P by A2, A3, A4, A6, AFF_1:30;
A10: ( Line b,c <> P & Line b,a <> P ) by A2, A3, A4, A6, AFF_1:30;
A11: ( b <> o & b <> a & b <> c ) by A4, AFF_1:16;
A12: Line b,a <> Line b,c by A4, A6, AFF_1:33;
A13: not LIN o,a,c

proof

assume LIN o,a,c ; :: thesis: contradiction
then c in A by A2, A4, AFF_1:39;
hence contradiction by A2, A3, A4, AFF_1:30; :: thesis: verum

end;

A14: c <> c'

proof

assume c = c' ; :: thesis: contradiction
then ( c,a // c,a' & LIN o,a,a' & not LIN o,c,a ) by A2, A4, A5, A13, AFF_1:13, AFF_1:15, AFF_1:33;
hence contradiction by A4, AFF_1:23; :: thesis: verum

end;

A15: now

assume A16: not LIN b',p,q ; :: thesis: a,c // p,q
( LIN o,a,a' & LIN b',p,a' & LIN o,c,c' & LIN b',q,c' ) by A2, A4, A5, AFF_1:15, AFF_1:33;
hence a,c // p,q by A1, A2, A4, A5, A6, A7, A10, A11, A12, A13, A14, A16, Def2; :: thesis: verum

end;

now

assume A17: LIN b',p,q ; :: thesis: a,c // p,q
set A' = Line b',a';
set C' = Line b',c';
A18: LIN b',q,p by A17, AFF_1:15;
A19: ( Line b',a' is being_line & Line b',c' is being_line & b' in Line b',a' & a' in Line b',a' & p in Line b',a' & b' in Line b',c' & c' in Line b',c' & q in Line b',c' ) by A5, A7, AFF_1:26, AFF_1:def 2, AFF_1:def 3;
then A20: Line b',a' <> Line b',c' by A4, AFF_1:33;

A21: now

assume b' <> p ; :: thesis: a,c // p,q
then A22: q in Line b',a' by A17, A19, AFF_1:39;
then A23: q = b' by A19, A20, AFF_1:30;
LIN b,c,b' by A5, A19, A20, A22, AFF_1:30;
then b' in Line b,c by AFF_1:def 2;
then A24: b = b' by A2, A4, A6, A9, AFF_1:30;
Line b',a' <> Line b,a

proof

assume Line b',a' = Line b,a ; :: thesis: contradiction
then LIN a,a',b by A6, A19, AFF_1:33;
then b in A by A2, A4, AFF_1:39;
hence contradiction by A2, A3, A4, AFF_1:30; :: thesis: verum

end;

then p = q by A6, A19, A23, A24, AFF_1:30;
hence a,c // p,q by AFF_1:12; :: thesis: verum

end;

now

assume b' <> q ; :: thesis: a,c // p,q
then A25: p in Line b',c' by A18, A19, AFF_1:39;
then A26: p = b' by A19, A20, AFF_1:30;
LIN b,a,b' by A5, A19, A20, A25, AFF_1:30;
then b' in Line b,a by AFF_1:def 2;
then A27: b = b' by A2, A4, A6, A8, AFF_1:30;
Line b',c' <> Line b,c

proof

assume Line b',c' = Line b,c ; :: thesis: contradiction
then LIN c,c',b by A6, A19, AFF_1:33;
then b in C by A2, A4, A14, AFF_1:39;
hence contradiction by A2, A3, A4, AFF_1:30; :: thesis: verum

end;

then p = q by A6, A19, A26, A27, AFF_1:30;
hence a,c // p,q by AFF_1:12; :: thesis: verum

end;

hence a,c // p,q by A4, A21; :: thesis: verum

end;

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