let AP be AffinPlane; :: thesis:
A1: ( AP is satisfying_DES2_1 implies AP is satisfying_DES2_3 )

assume A2: AP is satisfying_DES2_1 ; :: thesis:
thus AP is satisfying_DES2_3 :: thesis:

let A be Subset of ; :: according to AFF_3:def 8 :: thesis:
let P, C be Subset of ; :: thesis:
let a, a', b, b', c, c', p, q be Element of ; :: thesis:
assume that
A3: A is being_line and
A4: P is being_line and
A5: C is being_line and
A6: A <> P and
A7: A <> C and
A8: P <> C and
A9: a in A and
A10: a' in A and
A11: b in P and
A12: b' in P and
A13: c in C and
A14: c' in C and
A15: A // P and
A16: not LIN b,a,c and
A17: not LIN b',a',c' and
A18: p <> q and
A19: c <> c' and
A20: LIN b,a,p and
A21: LIN b',a',p and
A22: LIN b,c,q and
A23: LIN b',c',q and
A24: a,c // a',c' and
A25: a,c // p,q ; :: thesis:

now

set A' = Line a,c;
set P' = Line p,q;
set C' = Line a',c';
A26: LIN p,a',b' by A21, AFF_1:15;
A27: a <> c by A16, AFF_1:16;
then A28: ( Line a,c is being_line & a in Line a,c ) by AFF_1:38;
A29: q <> c

proof

assume A30: q = c ; :: thesis:
then c,p // c,a by A25, AFF_1:13;
then LIN c,p,a by AFF_1:def 1;
then A31: LIN p,a,c by AFF_1:15;
( LIN p,a,b & LIN p,a,a ) by A20, AFF_1:15, AFF_1:16;
then a = p by A16, A31, AFF_1:17;
then LIN a,a',b' by A21, AFF_1:15;
then ( b' in A or a = a' ) by A3, A9, A10, AFF_1:39;
then a',c' // a',c by A6, A12, A15, A24, AFF_1:13, AFF_1:59;
then LIN a',c',c by AFF_1:def 1;
then LIN c,c',a' by AFF_1:15;
then A32: a' in C by A5, A13, A14, A19, AFF_1:39;
LIN c,c',b' by A23, A30, AFF_1:15;
then b' in C by A5, A13, A14, A19, AFF_1:39;
hence contradiction by A5, A14, A17, A32, AFF_1:33; :: thesis:

end;

A33: a <> p

proof

assume a = p ; :: thesis:
then LIN a,c,q by A25, AFF_1:def 1;
then A34: LIN c,q,a by AFF_1:15;
( LIN c,q,b & LIN c,q,c ) by A22, AFF_1:15, AFF_1:16;
hence contradiction by A16, A29, A34, AFF_1:17; :: thesis:

end;

A35: a <> a'

proof

A36: ( LIN p,a,b & LIN p,a,a ) by A20, AFF_1:15, AFF_1:16;
assume A37: a = a' ; :: thesis:
then LIN a,c,c' by A24, AFF_1:def 1;
then LIN c,c',a by AFF_1:15;
then A38: a in C by A5, A13, A14, A19, AFF_1:39;
LIN p,a,b' by A21, A37, AFF_1:15;
then ( b = b' or a in P ) by A4, A11, A12, A33, A36, AFF_1:17, AFF_1:39;
then A39: LIN q,b,c' by A6, A9, A15, A23, AFF_1:15, AFF_1:59;
( LIN q,b,c & LIN q,b,b ) by A22, AFF_1:15, AFF_1:16;
then A40: ( q = b or LIN c,c',b ) by A39, AFF_1:17;
not b in C by A5, A13, A16, A38, AFF_1:33;
then LIN p,q,a by A5, A13, A14, A19, A20, A40, AFF_1:15, AFF_1:39;
then p,q // p,a by AFF_1:def 1;
then a,c // p,a by A18, A25, AFF_1:14;
then a,c // a,p by AFF_1:13;
then LIN a,c,p by AFF_1:def 1;
then A41: p in C by A5, A13, A27, A38, AFF_1:39;
LIN p,a,b by A20, AFF_1:15;
then b in C by A5, A33, A38, A41, AFF_1:39;
hence contradiction by A5, A13, A16, A38, AFF_1:33; :: thesis:

end;

A42: b <> b'

proof

A43: p,q // c,a by A25, AFF_1:13;
A44: ( LIN q,b,c & LIN q,b,b ) by A22, AFF_1:15, AFF_1:16;
A45: ( LIN p,b,a & LIN p,b,b ) by A20, AFF_1:15, AFF_1:16;
assume A46: b = b' ; :: thesis:
then LIN p,b,a' by A21, AFF_1:15;
then A47: ( p = b or b in A ) by A3, A9, A10, A35, A45, AFF_1:17, AFF_1:39;
LIN q,b,c' by A23, A46, AFF_1:15;
then ( b = q or LIN c,c',b ) by A44, AFF_1:17;
then A48: b in C by A5, A6, A11, A13, A14, A15, A18, A19, A47, AFF_1:39, AFF_1:59;
then q in C by A5, A6, A11, A13, A15, A16, A20, A22, A47, AFF_1:39, AFF_1:59;
then a in C by A5, A6, A11, A13, A15, A18, A47, A48, A43, AFF_1:59, AFF_1:62;
hence contradiction by A5, A13, A16, A48, AFF_1:33; :: thesis:

end;

then A49: a',a // b',b by A3, A4, A9, A10, A11, A12, A15, A35, AFF_1:52;
A50: a' <> c' by A17, AFF_1:16;
then A51: Line a',c' is being_line by AFF_1:38;
A52: c' in Line a',c' by A50, AFF_1:38;
A53: LIN p,a,b by A20, AFF_1:15;
A54: not LIN p,a',a

proof

assume LIN p,a',a ; :: thesis:
then A55: LIN p,a,a' by AFF_1:15;
LIN p,a,a by AFF_1:16;
then b in A by A3, A9, A10, A33, A35, A53, A55, AFF_1:17, AFF_1:39;
hence contradiction by A6, A11, A15, AFF_1:59; :: thesis:

end;

A56: LIN q,c',b' by A23, AFF_1:15;
A57: a' in Line a',c' by A50, AFF_1:38;
A58: c in Line a,c by A27, AFF_1:38;
then A59: Line a',c' // Line a,c by A24, A27, A50, A51, A28, A57, A52, AFF_1:52;
A60: Line a,c <> Line a',c'

proof

assume A61: Line a,c = Line a',c' ; :: thesis:
then LIN a,a',c' by A28, A57, A52, AFF_1:33;
then A62: c' in A by A3, A9, A10, A35, AFF_1:39;
LIN a,a',c by A28, A58, A57, A61, AFF_1:33;
then c in A by A3, A9, A10, A35, AFF_1:39;
hence contradiction by A3, A5, A7, A13, A14, A19, A62, AFF_1:30; :: thesis:

end;

A63: LIN q,c,b by A22, AFF_1:15;
A64: p in Line p,q by A18, AFF_1:38;
A65: Line a,c <> Line p,q

proof

assume Line a,c = Line p,q ; :: thesis:
then A66: ( LIN p,a,c & LIN p,a,a ) by A28, A58, A64, AFF_1:33;
LIN p,a,b by A20, AFF_1:15;
hence contradiction by A16, A33, A66, AFF_1:17; :: thesis:

end;

A67: Line p,q is being_line by A18, AFF_1:38;
A68: Line p,q <> Line a',c'

proof

assume Line p,q = Line a',c' ; :: thesis:
then A69: ( LIN p,a',c' & LIN p,a',a' ) by A67, A64, A57, A52, AFF_1:33;
LIN p,a',b' by A21, AFF_1:15;
then p = a' by A17, A69, AFF_1:17;
then LIN a,a',b by A20, AFF_1:15;
then b in A by A3, A9, A10, A35, AFF_1:39;
hence contradiction by A6, A11, A15, AFF_1:59; :: thesis:

end;

A70: a',c' // p,q by A24, A25, A27, AFF_1:14;
A71: not LIN q,c',c

proof

A72: now

assume q = c' ; :: thesis:
then c',a' // c',p by A70, AFF_1:13;
then LIN c',a',p by AFF_1:def 1;
then p in Line a',c' by A50, A51, A57, A52, AFF_1:39;
then ( p = a' or b' in Line a',c' ) by A51, A57, A26, AFF_1:39;
then LIN a,a',b by A17, A20, A51, A57, A52, AFF_1:15, AFF_1:33;
then b in A by A3, A9, A10, A35, AFF_1:39;
hence contradiction by A6, A11, A15, AFF_1:59; :: thesis:

end;

assume A73: LIN q,c',c ; :: thesis:
LIN q,c',c' by AFF_1:16;
then A74: b' in C by A5, A13, A14, A19, A56, A73, A72, AFF_1:17, AFF_1:39;
A75: LIN q,c,c by AFF_1:16;
LIN q,c,c' by A73, AFF_1:15;
then b in C by A5, A13, A14, A19, A29, A63, A75, AFF_1:17, AFF_1:39;
hence contradiction by A4, A5, A8, A11, A12, A42, A74, AFF_1:30; :: thesis:

end;

A76: q in Line p,q by A18, AFF_1:38;
then Line a',c' // Line p,q by A18, A50, A67, A51, A64, A57, A52, A70, AFF_1:52;
then a',a // c',c by A2, A67, A51, A28, A58, A64, A76, A57, A52, A42, A65, A60, A68, A59, A49, A53, A26, A63, A56, A54, A71, Def6;
hence A // C by A3, A5, A9, A10, A13, A14, A19, A35, AFF_1:52; :: thesis:

end;

hence A // C ; :: thesis:

end;

( AP is satisfying_DES2_3 implies AP is satisfying_DES2_1 )

proof

assume A77: AP is satisfying_DES2_3 ; :: thesis:
thus AP is satisfying_DES2_1 :: thesis:

proof

let A be Subset of ; :: according to AFF_3:def 6 :: thesis:
let P, C be Subset of ; :: thesis:
let a, a', b, b', c, c', p, q be Element of ; :: thesis:
assume that
A78: A is being_line and
A79: P is being_line and
A80: C is being_line and
A81: A <> P and
A <> C and
A82: P <> C and
A83: a in A and
A84: a' in A and
A85: b in P and
A86: b' in P and
A87: c in C and
A88: c' in C and
A89: A // P and
A90: A // C and
A91: not LIN b,a,c and
A92: not LIN b',a',c' and
A93: p <> q and
A94: LIN b,a,p and
A95: LIN b',a',p and
A96: LIN b,c,q and
A97: LIN b',c',q and
A98: a,c // p,q ; :: thesis:
A99: C // P by A89, A90, AFF_1:58;
then A100: c,c' // b,b' by A85, A86, A87, A88, AFF_1:53;
assume A101: not a,c // a',c' ; :: thesis:
A102: q <> c

proof

assume A103: q = c ; :: thesis:
then c,p // c,a by A98, AFF_1:13;
then LIN c,p,a by AFF_1:def 1;
then A104: LIN p,a,c by AFF_1:15;
( LIN p,a,b & LIN p,a,a ) by A94, AFF_1:15, AFF_1:16;
then a = p by A91, A104, AFF_1:17;
then LIN a,a',b' by A95, AFF_1:15;
then A105: ( b' in A or a = a' ) by A78, A83, A84, AFF_1:39;
LIN c,c',b' by A97, A103, AFF_1:15;
then ( c = c' or b' in C ) by A80, A87, A88, AFF_1:39;
hence contradiction by A81, A82, A86, A89, A101, A99, A105, AFF_1:11, AFF_1:59; :: thesis:

end;

A106: a <> p

proof

assume a = p ; :: thesis:
then LIN a,c,q by A98, AFF_1:def 1;
then A107: LIN c,q,a by AFF_1:15;
( LIN c,q,b & LIN c,q,c ) by A96, AFF_1:15, AFF_1:16;
hence contradiction by A91, A102, A107, AFF_1:17; :: thesis:

end;

A108: a <> a'

proof

A109: ( LIN p,a,b & LIN p,a,a ) by A94, AFF_1:15, AFF_1:16;
assume A110: a = a' ; :: thesis:
then LIN p,a,b' by A95, AFF_1:15;
then ( a in P or b = b' ) by A79, A85, A86, A106, A109, AFF_1:17, AFF_1:39;
then A111: LIN b,q,c' by A81, A83, A89, A97, AFF_1:15, AFF_1:59;
( LIN b,q,c & LIN b,q,b ) by A96, AFF_1:15, AFF_1:16;
then ( b = q or c = c' or b in C ) by A80, A87, A88, A111, AFF_1:17, AFF_1:39;
then LIN p,q,a by A82, A85, A94, A101, A99, A110, AFF_1:11, AFF_1:15, AFF_1:59;
then p,q // p,a by AFF_1:def 1;
then a,c // p,a by A93, A98, AFF_1:14;
then a,c // a,p by AFF_1:13;
then LIN a,c,p by AFF_1:def 1;
then A112: LIN p,a,c by AFF_1:15;
( LIN p,a,b & LIN p,a,a ) by A94, AFF_1:15, AFF_1:16;
hence contradiction by A91, A106, A112, AFF_1:17; :: thesis:

end;

A113: not LIN p,a,a'

proof

assume A114: LIN p,a,a' ; :: thesis:
( LIN p,a,b & LIN p,a,a ) by A94, AFF_1:15, AFF_1:16;
then b in A by A78, A83, A84, A106, A108, A114, AFF_1:17, AFF_1:39;
hence contradiction by A81, A85, A89, AFF_1:59; :: thesis:

end;

set A' = Line a,c;
set P' = Line p,q;
set C' = Line a',c';
A115: a <> c by A91, AFF_1:16;
then A116: Line a,c is being_line by AFF_1:38;
A117: ( c,c' // a,a' & LIN q,c,b ) by A83, A84, A87, A88, A90, A96, AFF_1:15, AFF_1:53;
A118: LIN p,a',b' by A95, AFF_1:15;
A119: ( a in Line a,c & c in Line a,c ) by A115, AFF_1:38;
A120: b <> b'

proof

assume b = b' ; :: thesis:
then A121: LIN b,p,a' by A95, AFF_1:15;
( LIN b,p,a & LIN b,p,b ) by A94, AFF_1:15, AFF_1:16;
then A122: ( b = p or b in A ) by A78, A83, A84, A108, A121, AFF_1:17, AFF_1:39;
then LIN p,q,c by A81, A85, A89, A96, AFF_1:15, AFF_1:59;
then p,q // p,c by AFF_1:def 1;
then a,c // p,c by A93, A98, AFF_1:14;
then c,a // c,p by AFF_1:13;
then LIN c,a,p by AFF_1:def 1;
hence contradiction by A81, A85, A89, A91, A122, AFF_1:15, AFF_1:59; :: thesis:

end;

A123: not LIN q,c,c'

proof

assume A124: LIN q,c,c' ; :: thesis:
( LIN q,c,b & LIN q,c,c ) by A96, AFF_1:15, AFF_1:16;
then ( c = c' or b in C ) by A80, A87, A88, A102, A124, AFF_1:17, AFF_1:39;
then A125: LIN q,c,b' by A82, A85, A97, A99, AFF_1:15, AFF_1:59;
( LIN q,c,b & LIN q,c,c ) by A96, AFF_1:15, AFF_1:16;
then c in P by A79, A85, A86, A102, A120, A125, AFF_1:17, AFF_1:39;
hence contradiction by A82, A87, A99, AFF_1:59; :: thesis:

end;

A126: ( LIN q,c',b' & LIN p,a,b ) by A94, A97, AFF_1:15;
A127: a' <> c' by A92, AFF_1:16;
then A128: Line a',c' is being_line by AFF_1:38;
A129: p in Line p,q by A93, AFF_1:38;
A130: Line a,c <> Line p,q

proof

assume Line a,c = Line p,q ; :: thesis:
then A131: ( LIN p,a,c & LIN p,a,a ) by A116, A119, A129, AFF_1:33;
LIN p,a,b by A94, AFF_1:15;
hence contradiction by A91, A106, A131, AFF_1:17; :: thesis:

end;

A132: ( Line p,q is being_line & q in Line p,q ) by A93, AFF_1:38;
then A133: Line a,c // Line p,q by A93, A98, A115, A116, A119, A129, AFF_1:52;
A134: ( a' in Line a',c' & c' in Line a',c' ) by A127, AFF_1:38;
then Line a,c <> Line a',c' by A101, A116, A119, AFF_1:65;
then Line a,c // Line a',c' by A77, A127, A116, A128, A119, A129, A132, A134, A100, A133, A130, A120, A123, A113, A117, A126, A118, Def8;
hence contradiction by A101, A119, A134, AFF_1:53; :: thesis:

end;

hence ( AP is satisfying_DES2_1 iff AP is satisfying_DES2_3 ) by A1; :: thesis: