let AP be AffinPlane; :: thesis: ( AP is satisfying_DES2 iff AP is satisfying_DES2_2 )
A1: ( AP is satisfying_DES2 implies AP is satisfying_DES2_2 )
proof
assume A2: AP is satisfying_DES2 ; :: thesis: AP is satisfying_DES2_2
thus AP is satisfying_DES2_2 :: thesis: verum
proof
let A be Subset of AP; :: according to AFF_3:def 7 :: 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 // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & 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
A // P
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 // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & 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
A // P
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 // C & not LIN b,a,c & not LIN b9,a9,c9 & p <> q & 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 A // P )
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 & a9 in A ) and
A10: ( b in P & b9 in P ) and
A11: c in C and
A12: c9 in C and
A13: A // C and
A14: not LIN b,a,c and
A15: not LIN b9,a9,c9 and
A16: p <> q and
A17: a <> a9 and
A18: LIN b,a,p and
A19: LIN b9,a9,p and
A20: LIN b,c,q and
A21: LIN b9,c9,q and
A22: a,c // a9,c9 and
A23: a,c // p,q ; :: thesis: A // P
A24: LIN q,c9,b9 by A21, AFF_1:6;
A25: c <> c9
proof
assume c = c9 ; :: thesis: contradiction
then c,a // c,a9 by A22, AFF_1:4;
then LIN c,a,a9 by AFF_1:def 1;
then LIN a,a9,c by AFF_1:6;
then c in A by A3, A9, A17, AFF_1:25;
hence contradiction by A7, A11, A13, AFF_1:45; :: thesis: verum
end;
A26: b <> b9
proof
A27: now :: thesis: ( b = p implies not b in C )
assume that
A28: b = p and
b in C ; :: thesis: contradiction
LIN p,q,c by A20, A28, AFF_1:6;
then p,q // p,c by AFF_1:def 1;
then a,c // p,c by A16, A23, 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 A14, A28, AFF_1:6; :: thesis: verum
end;
A29: ( LIN b,p,a & LIN b,p,b ) by A18, AFF_1:6, AFF_1:7;
assume A30: b = b9 ; :: thesis: contradiction
then LIN b,p,a9 by A19, AFF_1:6;
then A31: ( b = p or b in A ) by A3, A9, A17, A29, AFF_1:8, AFF_1:25;
A32: ( LIN b,q,c & LIN b,q,b ) by A20, AFF_1:6, AFF_1:7;
LIN b,q,c9 by A21, A30, AFF_1:6;
then A33: ( b = q or b in C ) by A5, A11, A12, A25, A32, AFF_1:8, AFF_1:25;
then LIN q,p,a by A7, A13, A18, A31, A27, AFF_1:6, AFF_1:45;
then q,p // q,a by AFF_1:def 1;
then p,q // q,a by AFF_1:4;
then a,c // q,a by A16, A23, AFF_1:5;
then a,c // a,q by AFF_1:4;
then LIN a,c,q by AFF_1:def 1;
hence contradiction by A7, A13, A14, A31, A33, A27, AFF_1:6, AFF_1:45; :: thesis: verum
end;
A34: a <> p
proof
assume A35: a = p ; :: thesis: contradiction
then LIN a,c,q by A23, AFF_1:def 1;
then A36: LIN c,q,a by AFF_1:6;
( LIN c,q,b & LIN c,q,c ) by A20, AFF_1:6, AFF_1:7;
then q = c by A14, A36, AFF_1:8;
then LIN c,c9,b9 by A21, AFF_1:6;
then A37: ( c = c9 or b9 in C ) by A5, A11, A12, AFF_1:25;
LIN a,a9,b9 by A19, A35, AFF_1:6;
then b9 in A by A3, A9, A17, AFF_1:25;
then c,a // c,a9 by A7, A13, A22, A37, AFF_1:4, AFF_1:45;
then LIN c,a,a9 by AFF_1:def 1;
then LIN a,a9,c by AFF_1:6;
then c in A by A3, A9, A17, AFF_1:25;
hence contradiction by A7, A11, A13, AFF_1:45; :: thesis: verum
end;
A38: q <> c
proof
assume q = c ; :: thesis: contradiction
then c,p // c,a by A23, AFF_1:4;
then LIN c,p,a by AFF_1:def 1;
then A39: LIN p,a,c by AFF_1:6;
( LIN p,a,b & LIN p,a,a ) by A18, AFF_1:6, AFF_1:7;
hence contradiction by A14, A34, A39, AFF_1:8; :: thesis: verum
end;
A40: LIN q,c,b by A20, AFF_1:6;
set A9 = Line (a,c);
set P9 = Line (p,q);
set C9 = Line (a9,c9);
A41: a <> c by A14, AFF_1:7;
then A42: c in Line (a,c) by AFF_1:24;
A43: a9 <> p
proof
assume A44: a9 = p ; :: thesis: contradiction
a9,c9 // p,q by A22, A23, A41, AFF_1:5;
then LIN a9,c9,q by A44, AFF_1:def 1;
then A45: LIN c9,q,a9 by AFF_1:6;
( LIN c9,q,b9 & LIN c9,q,c9 ) by A21, AFF_1:6, AFF_1:7;
then q = c9 by A15, A45, AFF_1:8;
then LIN c,c9,b by A20, AFF_1:6;
then A46: b in C by A5, A11, A12, A25, AFF_1:25;
LIN a,a9,b by A18, A44, AFF_1:6;
then b in A by A3, A9, A17, AFF_1:25;
hence contradiction by A7, A13, A46, AFF_1:45; :: thesis: verum
end;
A47: c9 <> q
proof
assume c9 = q ; :: thesis: contradiction
then a9,c9 // p,c9 by A22, A23, A41, AFF_1:5;
then c9,a9 // c9,p by AFF_1:4;
then LIN c9,a9,p by AFF_1:def 1;
then A48: LIN p,a9,c9 by AFF_1:6;
( LIN p,a9,b9 & LIN p,a9,a9 ) by A19, AFF_1:6, AFF_1:7;
hence contradiction by A15, A43, A48, AFF_1:8; :: thesis: verum
end;
A49: not LIN q,c9,c
proof
A50: LIN q,c,c by AFF_1:7;
assume A51: LIN q,c9,c ; :: thesis: contradiction
LIN q,c9,c9 by AFF_1:7;
then A52: b9 in C by A5, A11, A12, A25, A47, A24, A51, AFF_1:8, AFF_1:25;
LIN q,c,c9 by A51, AFF_1:6;
then b in C by A5, A11, A12, A38, A25, A40, A50, AFF_1:8, AFF_1:25;
hence contradiction by A4, A5, A8, A10, A26, A52, AFF_1:18; :: thesis: verum
end;
A53: LIN p,a,b by A18, AFF_1:6;
A54: LIN p,a9,b9 by A19, AFF_1:6;
A55: not LIN p,a9,a
proof
A56: LIN p,a,a by AFF_1:7;
assume A57: LIN p,a9,a ; :: thesis: contradiction
LIN p,a9,a9 by AFF_1:7;
then A58: b9 in A by A3, A9, A17, A43, A54, A57, AFF_1:8, AFF_1:25;
LIN p,a,a9 by A57, AFF_1:6;
then b in A by A3, A9, A17, A34, A53, A56, AFF_1:8, AFF_1:25;
hence contradiction by A3, A4, A6, A10, A26, A58, AFF_1:18; :: thesis: verum
end;
A59: a9,a // c9,c by A9, A11, A12, A13, AFF_1:39;
A60: q in Line (p,q) by A16, AFF_1:24;
A61: a9 <> c9 by A15, AFF_1:7;
then A62: a9 in Line (a9,c9) by AFF_1:24;
A63: ( Line (a,c) is being_line & a in Line (a,c) ) by A41, AFF_1:24;
A64: Line (a9,c9) <> Line (a,c)
proof
assume Line (a9,c9) = Line (a,c) ; :: thesis: contradiction
then LIN a,a9,c by A63, A42, A62, AFF_1:21;
then c in A by A3, A9, A17, AFF_1:25;
hence contradiction by A7, A11, A13, AFF_1:45; :: thesis: verum
end;
A65: p in Line (p,q) by A16, AFF_1:24;
A66: Line (p,q) <> Line (a,c)
proof
assume Line (p,q) = Line (a,c) ; :: thesis: contradiction
then A67: ( LIN p,a,c & LIN p,a,a ) by A63, A42, A65, AFF_1:21;
LIN p,a,b by A18, AFF_1:6;
hence contradiction by A14, A34, A67, AFF_1:8; :: thesis: verum
end;
A68: c9 in Line (a9,c9) by A61, AFF_1:24;
A69: Line (p,q) is being_line by A16, AFF_1:24;
A70: Line (a9,c9) <> Line (p,q)
proof
assume Line (a9,c9) = Line (p,q) ; :: thesis: contradiction
then A71: ( LIN p,a9,c9 & LIN p,a9,a9 ) by A69, A65, A62, A68, AFF_1:21;
LIN p,a9,b9 by A19, AFF_1:6;
hence contradiction by A15, A43, A71, AFF_1:8; :: thesis: verum
end;
A72: Line (a9,c9) is being_line by A61, AFF_1:24;
a9,c9 // p,q by A22, A23, A41, AFF_1:5;
then A73: Line (a9,c9) // Line (p,q) by A16, A61, A69, A72, A65, A60, A62, A68, AFF_1:38;
Line (a9,c9) // Line (a,c) by A22, A41, A61, A72, A63, A42, A62, A68, AFF_1:38;
then a9,a // b9,b by A2, A61, A26, A69, A72, A63, A42, A65, A60, A62, A68, A73, A64, A70, A66, A54, A53, A24, A40, A55, A49, A59;
hence A // P by A3, A4, A9, A10, A17, A26, AFF_1:38; :: thesis: verum
end;
end;
( AP is satisfying_DES2_2 implies AP is satisfying_DES2 )
proof
assume A74: AP is satisfying_DES2_2 ; :: thesis: AP is satisfying_DES2
thus AP is satisfying_DES2 :: thesis: verum
proof
let A be Subset of AP; :: according to AFF_3:def 5 :: 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 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds
a,c // p,q
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 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds
a,c // p,q
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 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 implies a,c // p,q )
assume that
A75: A is being_line and
P is being_line and
A76: C is being_line and
A77: A <> P and
A78: A <> C and
A79: P <> C and
A80: ( a in A & a9 in A ) and
A81: b in P and
A82: b9 in P and
A83: c in C and
A84: c9 in C and
A85: A // P and
A86: A // C and
A87: not LIN b,a,c and
A88: not LIN b9,a9,c9 and
A89: p <> q and
A90: a <> a9 and
A91: LIN b,a,p and
A92: LIN b9,a9,p and
A93: LIN b,c,q and
A94: LIN b9,c9,q and
A95: a,c // a9,c9 ; :: thesis: a,c // p,q
A96: LIN p,a,b by A91, AFF_1:6;
set A9 = Line (a,c);
set P9 = Line (p,q);
set C9 = Line (a9,c9);
A97: q in Line (p,q) by A89, AFF_1:24;
A98: a <> p
proof
assume a = p ; :: thesis: contradiction
then LIN a,a9,b9 by A92, AFF_1:6;
then b9 in A by A75, A80, A90, AFF_1:25;
hence contradiction by A77, A82, A85, AFF_1:45; :: thesis: verum
end;
A99: not LIN p,a,a9
proof
A100: LIN p,a,a by AFF_1:7;
assume LIN p,a,a9 ; :: thesis: contradiction
then b in A by A75, A80, A90, A98, A96, A100, AFF_1:8, AFF_1:25;
hence contradiction by A77, A81, A85, AFF_1:45; :: thesis: verum
end;
A101: ( LIN q,c9,b9 & LIN p,a9,b9 ) by A92, A94, AFF_1:6;
A102: a <> c by A87, AFF_1:7;
then A103: Line (a,c) is being_line by AFF_1:24;
A104: C // P by A85, A86, AFF_1:44;
then A105: c,c9 // b,b9 by A81, A82, A83, A84, AFF_1:39;
A106: c <> c9
proof
assume c = c9 ; :: thesis: contradiction
then c,a // c,a9 by A95, AFF_1:4;
then LIN c,a,a9 by AFF_1:def 1;
then LIN a,a9,c by AFF_1:6;
then c in A by A75, A80, A90, AFF_1:25;
hence contradiction by A78, A83, A86, AFF_1:45; :: thesis: verum
end;
A107: b <> b9
proof
A108: ( LIN b,p,a & LIN b,p,b ) by A91, AFF_1:6, AFF_1:7;
assume A109: b = b9 ; :: thesis: contradiction
then LIN b,p,a9 by A92, AFF_1:6;
then A110: ( b = p or b in A ) by A75, A80, A90, A108, AFF_1:8, AFF_1:25;
A111: ( LIN b,q,c & LIN b,q,b ) by A93, AFF_1:6, AFF_1:7;
LIN b,q,c9 by A94, A109, AFF_1:6;
then ( b = q or b in C ) by A76, A83, A84, A106, A111, AFF_1:8, AFF_1:25;
hence contradiction by A77, A79, A81, A85, A89, A104, A110, AFF_1:45; :: thesis: verum
end;
A112: ( a in Line (a,c) & c in Line (a,c) ) by A102, AFF_1:24;
A113: ( Line (p,q) is being_line & c,c9 // a,a9 ) by A80, A83, A84, A86, A89, AFF_1:24, AFF_1:39;
A114: p in Line (p,q) by A89, AFF_1:24;
A115: a9 <> c9 by A88, AFF_1:7;
then A116: a9 in Line (a9,c9) by AFF_1:24;
A117: Line (a,c) <> Line (a9,c9)
proof
assume Line (a,c) = Line (a9,c9) ; :: thesis: contradiction
then LIN a,a9,c by A103, A112, A116, AFF_1:21;
then c in A by A75, A80, A90, AFF_1:25;
hence contradiction by A78, A83, A86, AFF_1:45; :: thesis: verum
end;
A118: q <> c
proof
assume q = c ; :: thesis: contradiction
then LIN c,c9,b9 by A94, AFF_1:6;
then b9 in C by A76, A83, A84, A106, AFF_1:25;
hence contradiction by A79, A82, A104, AFF_1:45; :: thesis: verum
end;
A119: Line (a,c) <> Line (p,q)
proof
assume Line (a,c) = Line (p,q) ; :: thesis: contradiction
then A120: ( LIN c,q,a & LIN c,q,c ) by A103, A112, A97, AFF_1:21;
LIN c,q,b by A93, AFF_1:6;
hence contradiction by A87, A118, A120, AFF_1:8; :: thesis: verum
end;
A121: LIN q,c,b by A93, AFF_1:6;
A122: not LIN q,c,c9
proof
A123: LIN q,c,c by AFF_1:7;
assume LIN q,c,c9 ; :: thesis: contradiction
then b in C by A76, A83, A84, A106, A118, A121, A123, AFF_1:8, AFF_1:25;
hence contradiction by A79, A81, A104, AFF_1:45; :: thesis: verum
end;
A124: ( Line (a9,c9) is being_line & c9 in Line (a9,c9) ) by A115, AFF_1:24;
then Line (a,c) // Line (a9,c9) by A95, A102, A115, A103, A112, A116, AFF_1:38;
then Line (a,c) // Line (p,q) by A74, A102, A107, A103, A112, A114, A97, A116, A124, A113, A105, A121, A96, A101, A119, A117, A122, A99;
hence a,c // p,q by A112, A114, A97, AFF_1:39; :: thesis: verum
end;
end;
hence ( AP is satisfying_DES2 iff AP is satisfying_DES2_2 ) by A1; :: thesis: verum