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

proof

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

proof

let A be Subset of AP; :: according to AFF_3:def 8 :: 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 & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & c <> c9 & 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
A // C
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 & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & c <> c9 & 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
A // C
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 & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & c <> c9 & 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 A // C )
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: a9 in A and
A11: b in P and
A12: b9 in P and
A13: c in C and
A14: c9 in C and
A15: A // P and
A16: not LIN b,a,c and
A17: not LIN b9,a9,c9 and
A18: p <> q and
A19: c <> c9 and
A20: LIN b,a,p and
A21: LIN b9,a9,p and
A22: LIN b,c,q and
A23: LIN b9,c9,q and
A24: a,c // a9,c9 and
A25: a,c // p,q ; :: thesis: A // C

now :: thesis: A // C

set A9 = Line (a,c);
set P9 = Line (p,q);
set C9 = Line (a9,c9);
A26: LIN p,a9,b9 by A21, AFF_1:6;
A27: a <> c by A16, AFF_1:7;
then A28: ( Line (a,c) is being_line & a in Line (a,c) ) by AFF_1:24;
A29: q <> c

proof

assume A30: q = c ; :: thesis: contradiction
then c,p // c,a by A25, AFF_1:4;
then LIN c,p,a by AFF_1:def 1;
then A31: LIN p,a,c by AFF_1:6;
( LIN p,a,b & LIN p,a,a ) by A20, AFF_1:6, AFF_1:7;
then a = p by A16, A31, AFF_1:8;
then LIN a,a9,b9 by A21, AFF_1:6;
then ( b9 in A or a = a9 ) by A3, A9, A10, AFF_1:25;
then a9,c9 // a9,c by A6, A12, A15, A24, AFF_1:4, AFF_1:45;
then LIN a9,c9,c by AFF_1:def 1;
then LIN c,c9,a9 by AFF_1:6;
then A32: a9 in C by A5, A13, A14, A19, AFF_1:25;
LIN c,c9,b9 by A23, A30, AFF_1:6;
then b9 in C by A5, A13, A14, A19, AFF_1:25;
hence contradiction by A5, A14, A17, A32, AFF_1:21; :: thesis: verum

end;

A33: a <> p

proof

assume a = p ; :: thesis: contradiction
then LIN a,c,q by A25, AFF_1:def 1;
then A34: LIN c,q,a by AFF_1:6;
( LIN c,q,b & LIN c,q,c ) by A22, AFF_1:6, AFF_1:7;
hence contradiction by A16, A29, A34, AFF_1:8; :: thesis: verum

end;

A35: a <> a9

proof

A36: ( LIN p,a,b & LIN p,a,a ) by A20, AFF_1:6, AFF_1:7;
assume A37: a = a9 ; :: thesis: contradiction
then LIN a,c,c9 by A24, AFF_1:def 1;
then LIN c,c9,a by AFF_1:6;
then A38: a in C by A5, A13, A14, A19, AFF_1:25;
LIN p,a,b9 by A21, A37, AFF_1:6;
then ( b = b9 or a in P ) by A4, A11, A12, A33, A36, AFF_1:8, AFF_1:25;
then A39: LIN q,b,c9 by A6, A9, A15, A23, AFF_1:6, AFF_1:45;
( LIN q,b,c & LIN q,b,b ) by A22, AFF_1:6, AFF_1:7;
then A40: ( q = b or LIN c,c9,b ) by A39, AFF_1:8;
not b in C by A5, A13, A16, A38, AFF_1:21;
then LIN p,q,a by A5, A13, A14, A19, A20, A40, AFF_1:6, AFF_1:25;
then p,q // p,a by AFF_1:def 1;
then a,c // p,a by A18, A25, AFF_1:5;
then a,c // a,p by AFF_1:4;
then LIN a,c,p by AFF_1:def 1;
then A41: p in C by A5, A13, A27, A38, AFF_1:25;
LIN p,a,b by A20, AFF_1:6;
then b in C by A5, A33, A38, A41, AFF_1:25;
hence contradiction by A5, A13, A16, A38, AFF_1:21; :: thesis: verum

end;

A42: b <> b9

proof

A43: p,q // c,a by A25, AFF_1:4;
A44: ( LIN q,b,c & LIN q,b,b ) by A22, AFF_1:6, AFF_1:7;
A45: ( LIN p,b,a & LIN p,b,b ) by A20, AFF_1:6, AFF_1:7;
assume A46: b = b9 ; :: thesis: contradiction
then LIN p,b,a9 by A21, AFF_1:6;
then A47: ( p = b or b in A ) by A3, A9, A10, A35, A45, AFF_1:8, AFF_1:25;
LIN q,b,c9 by A23, A46, AFF_1:6;
then ( b = q or LIN c,c9,b ) by A44, AFF_1:8;
then A48: b in C by A5, A6, A11, A13, A14, A15, A18, A19, A47, AFF_1:25, AFF_1:45;
then q in C by A5, A6, A11, A13, A15, A16, A20, A22, A47, AFF_1:25, AFF_1:45;
then a in C by A5, A6, A11, A13, A15, A18, A47, A48, A43, AFF_1:45, AFF_1:48;
hence contradiction by A5, A13, A16, A48, AFF_1:21; :: thesis: verum

end;

then A49: a9,a // b9,b by A3, A4, A9, A10, A11, A12, A15, A35, AFF_1:38;
A50: a9 <> c9 by A17, AFF_1:7;
then A51: Line (a9,c9) is being_line by AFF_1:24;
A52: c9 in Line (a9,c9) by A50, AFF_1:24;
A53: LIN p,a,b by A20, AFF_1:6;
A54: not LIN p,a9,a

proof

assume LIN p,a9,a ; :: thesis: contradiction
then A55: LIN p,a,a9 by AFF_1:6;
LIN p,a,a by AFF_1:7;
then b in A by A3, A9, A10, A33, A35, A53, A55, AFF_1:8, AFF_1:25;
hence contradiction by A6, A11, A15, AFF_1:45; :: thesis: verum

end;

A56: LIN q,c9,b9 by A23, AFF_1:6;
A57: a9 in Line (a9,c9) by A50, AFF_1:24;
A58: c in Line (a,c) by A27, AFF_1:24;
then A59: Line (a9,c9) // Line (a,c) by A24, A27, A50, A51, A28, A57, A52, AFF_1:38;
A60: Line (a,c) <> Line (a9,c9)

proof

assume A61: Line (a,c) = Line (a9,c9) ; :: thesis: contradiction
then LIN a,a9,c9 by A28, A57, A52, AFF_1:21;
then A62: c9 in A by A3, A9, A10, A35, AFF_1:25;
LIN a,a9,c by A28, A58, A57, A61, AFF_1:21;
then c in A by A3, A9, A10, A35, AFF_1:25;
hence contradiction by A3, A5, A7, A13, A14, A19, A62, AFF_1:18; :: thesis: verum

end;

A63: LIN q,c,b by A22, AFF_1:6;
A64: p in Line (p,q) by A18, AFF_1:24;
A65: Line (a,c) <> Line (p,q)

proof

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

end;

A67: Line (p,q) is being_line by A18, AFF_1:24;
A68: Line (p,q) <> Line (a9,c9)

proof

assume Line (p,q) = Line (a9,c9) ; :: thesis: contradiction
then A69: ( LIN p,a9,c9 & LIN p,a9,a9 ) by A67, A64, A57, A52, AFF_1:21;
LIN p,a9,b9 by A21, AFF_1:6;
then p = a9 by A17, A69, AFF_1:8;
then LIN a,a9,b by A20, AFF_1:6;
then b in A by A3, A9, A10, A35, AFF_1:25;
hence contradiction by A6, A11, A15, AFF_1:45; :: thesis: verum

end;

A70: a9,c9 // p,q by A24, A25, A27, AFF_1:5;
A71: not LIN q,c9,c

proof

A72: now :: thesis: not q = c9

assume q = c9 ; :: thesis: contradiction
then c9,a9 // c9,p by A70, AFF_1:4;
then LIN c9,a9,p by AFF_1:def 1;
then p in Line (a9,c9) by A50, A51, A57, A52, AFF_1:25;
then ( p = a9 or b9 in Line (a9,c9) ) by A51, A57, A26, AFF_1:25;
then LIN a,a9,b by A17, A20, A51, A57, A52, AFF_1:6, AFF_1:21;
then b in A by A3, A9, A10, A35, AFF_1:25;
hence contradiction by A6, A11, A15, AFF_1:45; :: thesis: verum

end;

assume A73: LIN q,c9,c ; :: thesis: contradiction
LIN q,c9,c9 by AFF_1:7;
then A74: b9 in C by A5, A13, A14, A19, A56, A73, A72, AFF_1:8, AFF_1:25;
A75: LIN q,c,c by AFF_1:7;
LIN q,c,c9 by A73, AFF_1:6;
then b in C by A5, A13, A14, A19, A29, A63, A75, AFF_1:8, AFF_1:25;
hence contradiction by A4, A5, A8, A11, A12, A42, A74, AFF_1:18; :: thesis: verum

end;

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

end;

hence A // C ; :: thesis: verum

end;

end;

( AP is satisfying_DES2_3 implies AP is satisfying_DES2_1 )

proof

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

proof

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
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: a9 in A and
A85: b in P and
A86: b9 in P and
A87: c in C and
A88: c9 in C and
A89: A // P and
A90: A // C and
A91: not LIN b,a,c and
A92: not LIN b9,a9,c9 and
A93: p <> q and
A94: LIN b,a,p and
A95: LIN b9,a9,p and
A96: LIN b,c,q and
A97: LIN b9,c9,q and
A98: a,c // p,q ; :: thesis: a,c // a9,c9
A99: C // P by A89, A90, AFF_1:44;
then A100: c,c9 // b,b9 by A85, A86, A87, A88, AFF_1:39;
assume A101: not a,c // a9,c9 ; :: thesis: contradiction
A102: q <> c

proof

assume A103: q = c ; :: thesis: contradiction
then c,p // c,a by A98, AFF_1:4;
then LIN c,p,a by AFF_1:def 1;
then A104: LIN p,a,c by AFF_1:6;
( LIN p,a,b & LIN p,a,a ) by A94, AFF_1:6, AFF_1:7;
then a = p by A91, A104, AFF_1:8;
then LIN a,a9,b9 by A95, AFF_1:6;
then A105: ( b9 in A or a = a9 ) by A78, A83, A84, AFF_1:25;
LIN c,c9,b9 by A97, A103, AFF_1:6;
then ( c = c9 or b9 in C ) by A80, A87, A88, AFF_1:25;
hence contradiction by A81, A82, A86, A89, A101, A99, A105, AFF_1:2, AFF_1:45; :: thesis: verum

end;

A106: a <> p

proof

assume a = p ; :: thesis: contradiction
then LIN a,c,q by A98, AFF_1:def 1;
then A107: LIN c,q,a by AFF_1:6;
( LIN c,q,b & LIN c,q,c ) by A96, AFF_1:6, AFF_1:7;
hence contradiction by A91, A102, A107, AFF_1:8; :: thesis: verum

end;

A108: a <> a9

proof

A109: ( LIN p,a,b & LIN p,a,a ) by A94, AFF_1:6, AFF_1:7;
assume A110: a = a9 ; :: thesis: contradiction
then LIN p,a,b9 by A95, AFF_1:6;
then ( a in P or b = b9 ) by A79, A85, A86, A106, A109, AFF_1:8, AFF_1:25;
then A111: LIN b,q,c9 by A81, A83, A89, A97, AFF_1:6, AFF_1:45;
( LIN b,q,c & LIN b,q,b ) by A96, AFF_1:6, AFF_1:7;
then ( b = q or c = c9 or b in C ) by A80, A87, A88, A111, AFF_1:8, AFF_1:25;
then LIN p,q,a by A82, A85, A94, A101, A99, A110, AFF_1:2, AFF_1:6, AFF_1:45;
then p,q // p,a by AFF_1:def 1;
then a,c // p,a by A93, A98, AFF_1:5;
then a,c // a,p by AFF_1:4;
then LIN a,c,p by AFF_1:def 1;
then A112: LIN p,a,c by AFF_1:6;
( LIN p,a,b & LIN p,a,a ) by A94, AFF_1:6, AFF_1:7;
hence contradiction by A91, A106, A112, AFF_1:8; :: thesis: verum

end;

A113: not LIN p,a,a9

proof

assume A114: LIN p,a,a9 ; :: thesis: contradiction
( LIN p,a,b & LIN p,a,a ) by A94, AFF_1:6, AFF_1:7;
then b in A by A78, A83, A84, A106, A108, A114, AFF_1:8, AFF_1:25;
hence contradiction by A81, A85, A89, AFF_1:45; :: thesis: verum

end;

set A9 = Line (a,c);
set P9 = Line (p,q);
set C9 = Line (a9,c9);
A115: a <> c by A91, AFF_1:7;
then A116: Line (a,c) is being_line by AFF_1:24;
A117: ( c,c9 // a,a9 & LIN q,c,b ) by A83, A84, A87, A88, A90, A96, AFF_1:6, AFF_1:39;
A118: LIN p,a9,b9 by A95, AFF_1:6;
A119: ( a in Line (a,c) & c in Line (a,c) ) by A115, AFF_1:24;
A120: b <> b9

proof

assume b = b9 ; :: thesis: contradiction
then A121: LIN b,p,a9 by A95, AFF_1:6;
( LIN b,p,a & LIN b,p,b ) by A94, AFF_1:6, AFF_1:7;
then A122: ( b = p or b in A ) by A78, A83, A84, A108, A121, AFF_1:8, AFF_1:25;
then LIN p,q,c by A81, A85, A89, A96, AFF_1:6, AFF_1:45;
then p,q // p,c by AFF_1:def 1;
then a,c // p,c by A93, A98, AFF_1:5;
then c,a // c,p by AFF_1:4;
then LIN c,a,p by AFF_1:def 1;
hence contradiction by A81, A85, A89, A91, A122, AFF_1:6, AFF_1:45; :: thesis: verum

end;

A123: not LIN q,c,c9

proof

assume A124: LIN q,c,c9 ; :: thesis: contradiction
( LIN q,c,b & LIN q,c,c ) by A96, AFF_1:6, AFF_1:7;
then ( c = c9 or b in C ) by A80, A87, A88, A102, A124, AFF_1:8, AFF_1:25;
then A125: LIN q,c,b9 by A82, A85, A97, A99, AFF_1:6, AFF_1:45;
( LIN q,c,b & LIN q,c,c ) by A96, AFF_1:6, AFF_1:7;
then c in P by A79, A85, A86, A102, A120, A125, AFF_1:8, AFF_1:25;
hence contradiction by A82, A87, A99, AFF_1:45; :: thesis: verum

end;

A126: ( LIN q,c9,b9 & LIN p,a,b ) by A94, A97, AFF_1:6;
A127: a9 <> c9 by A92, AFF_1:7;
then A128: Line (a9,c9) is being_line by AFF_1:24;
A129: p in Line (p,q) by A93, AFF_1:24;
A130: Line (a,c) <> Line (p,q)

proof

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

end;

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

end;

end;

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