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, a', b, b', c, c', 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 & a' in A & b in P & b' in P & c in C & c' in C & A // P & A // C & not LIN b,a,c & not LIN b',a',c' & p <> q & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // p,q holds
a,c // a',c'
let P, C be Subset of AP; :: thesis: for 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 & A <> P & A <> C & P <> C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A // P & A // C & not LIN b,a,c & not LIN b',a',c' & p <> q & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // p,q holds
a,c // a',c'
let 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 & A <> P & A <> C & P <> C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A // P & A // C & not LIN b,a,c & not LIN b',a',c' & p <> q & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // p,q implies a,c // a',c' )
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: a' in A and
A10: b in P and
A11: b' in P and
A12: c in C and
A13: c' in C and
A14: A // P and
A15: A // C and
A16: not LIN b,a,c and
A17: not LIN b',a',c' and
A18: p <> q and
A19: LIN b,a,p and
A20: LIN b',a',p and
A21: LIN b,c,q and
A22: LIN b',c',q and
A23: a,c // p,q ; :: thesis: a,c // a',c'
assume A24: not a,c // a',c' ; :: thesis: contradiction
A25: ( a <> b & b <> c & a <> c & a' <> b' & a' <> c' & b' <> c' ) by A16, A17, AFF_1:16;
A26: P // C by A14, A15, AFF_1:58;
A27: c <> q

proof

assume A28: c = q ; :: thesis: contradiction
then LIN c,c',b' by A22, AFF_1:15;
then A29: ( c = c' or b' in C ) by A4, A12, A13, AFF_1:39;
c,a // c,p by A23, A28, AFF_1:13;
then LIN c,a,p by AFF_1:def 1;
then ( LIN p,a,c & LIN p,a,b & LIN p,a,a ) by A19, AFF_1:15, AFF_1:16;
then p = a by A16, AFF_1:17;
then LIN a,a',b' by A20, AFF_1:15;
then ( a = a' or b' in A ) by A2, A8, A9, AFF_1:39;
hence contradiction by A5, A7, A11, A14, A24, A26, A29, AFF_1:11, AFF_1:59; :: thesis: verum

end;

A30: c <> c'

proof

assume A31: c = c' ; :: thesis: contradiction
then ( LIN q,c,b & LIN q,c,b' & LIN q,c,c ) by A21, A22, AFF_1:15, AFF_1:16;
then ( b = b' or c in P ) by A3, A10, A11, A27, AFF_1:17, AFF_1:39;
then A32: ( LIN p,b,a' & LIN p,b,a & LIN p,b,b ) by A7, A12, A19, A20, A26, AFF_1:15, AFF_1:16, AFF_1:59;

now

assume A33: p = b ; :: thesis: contradiction
then ( a,c // b,q & LIN b,q,c ) by A21, A23, AFF_1:15;
then ( a,c // b,q & b,q // b,c ) by AFF_1:def 1;
then ( a,c // b,c or b = q ) by AFF_1:14;
then c,a // c,b by A18, A33, AFF_1:13;
then LIN c,a,b by AFF_1:def 1;
hence contradiction by A16, AFF_1:15; :: thesis: verum

end;

then ( a = a' or b in A ) by A2, A8, A9, A32, AFF_1:17, AFF_1:39;
hence contradiction by A5, A10, A14, A24, A31, AFF_1:11, AFF_1:59; :: thesis: verum

end;

set K = Line p,q;
set M = Line a,c;
set N = Line a',c';
A34: ( Line p,q is being_line & Line a,c is being_line & Line a',c' is being_line & p in Line p,q & q in Line p,q & a in Line a,c & c in Line a,c & a' in Line a',c' & c' in Line a',c' ) by A18, A25, AFF_1:38;
then A35: Line a,c // Line p,q by A18, A23, A25, AFF_1:52;
consider x being Element of AP such that
A36: ( x in Line a,c & x in Line a',c' ) by A34, AFF_1:72, A24, AFF_1:53;
( C // P & C // A ) by A14, A15, AFF_1:58;
then A37: ( c,c' // b,b' & c,c' // a,a' ) by A8, A9, A10, A11, A12, A13, AFF_1:53;
A38: ( LIN q,c,b & LIN q,c',b' & LIN p,a,b & LIN p,a',b' ) by A19, A20, A21, A22, AFF_1:15;
A39: b <> b'

proof

assume b = b' ; :: thesis: contradiction
then ( LIN q,b,c & LIN q,b,c' & LIN q,b,b ) by A21, A22, AFF_1:15, AFF_1:16;
then A40: ( q = b or b in C ) by A4, A12, A13, A30, AFF_1:17, AFF_1:39;
then ( a,c // p,b & b,a // b,p ) by A7, A10, A19, A23, A26, AFF_1:59, AFF_1:def 1;
then ( a,c // p,b & a,b // p,b ) by AFF_1:13;
then ( a,c // a,b or p = b ) by AFF_1:14;
then LIN a,c,b by A7, A10, A18, A26, A40, AFF_1:59, AFF_1:def 1;
hence contradiction by A16, AFF_1:15; :: thesis: verum

end;

A41: p <> a

proof

assume p = a ; :: thesis: contradiction
then LIN a,c,q by A23, AFF_1:def 1;
then ( LIN c,q,a & LIN c,q,b & LIN c,q,c ) by A21, AFF_1:15, AFF_1:16;
hence contradiction by A16, A27, AFF_1:17; :: thesis: verum

end;

A42: now

assume Line a,c = Line p,q ; :: thesis: contradiction
then ( LIN q,c,a & LIN q,c,b & LIN q,c,c ) by A21, A34, AFF_1:15, AFF_1:33;
hence contradiction by A16, A27, AFF_1:17; :: thesis: verum

end;

A43: Line a,c <> Line a',c' by A24, A34, AFF_1:65;

A44: now

assume x = c ; :: thesis: contradiction
then Line a',c' = C by A4, A12, A13, A30, A34, A36, AFF_1:30;
hence contradiction by A6, A9, A15, A34, AFF_1:59; :: thesis: verum

end;

A45: now

assume x = c' ; :: thesis: contradiction
then Line a,c = C by A4, A12, A13, A30, A34, A36, AFF_1:30;
hence contradiction by A6, A8, A15, A34, AFF_1:59; :: thesis: verum

end;

A46: not LIN q,c,c'

proof

assume LIN q,c,c' ; :: thesis: contradiction
then ( LIN q,c,c' & LIN q,c,b & LIN q,c,c ) by A21, AFF_1:15, AFF_1:16;
then b in C by A4, A12, A13, A27, A30, AFF_1:17, AFF_1:39;
hence contradiction by A7, A10, A26, AFF_1:59; :: thesis: verum

end;

not LIN p,a,a'

proof

assume LIN p,a,a' ; :: thesis: contradiction
then ( LIN p,a,a' & LIN p,a,b & LIN p,a,a ) by A19, AFF_1:15, AFF_1:16;
then ( a = a' or b in A ) by A2, A8, A9, A41, AFF_1:17, AFF_1:39;
then ( LIN p,a,b & LIN p,a,b' & LIN p,a,a ) by A5, A10, A14, A19, A20, AFF_1:15, AFF_1:16, AFF_1:59;
then a in P by A3, A10, A11, A39, A41, AFF_1:17, AFF_1:39;
hence contradiction by A5, A8, A14, AFF_1:59; :: thesis: verum

end;

then x in Line p,q by A1, A18, A25, A34, A36, A37, A38, A39, A43, A44, A45, A46, Def4;
hence contradiction by A35, A36, A42, AFF_1:59; :: thesis: verum