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