let AP be AffinPlane; ( 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
;
AP is satisfying_DES2_3
thus
AP is
satisfying_DES2_3
verumproof
let A be
Subset of
AP;
AFF_3:def 8 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 // Clet P,
C be
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 // Clet a,
a9,
b,
b9,
c,
c9,
p,
q be
Element of
AP;
( 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
;
A // C
now A // Cset 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
;
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;
verum
end; A33:
a <> p
proof
assume
a = p
;
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;
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
;
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;
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
;
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;
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
;
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;
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)
;
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;
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)
;
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;
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)
;
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;
verum
end; A70:
a9,
c9 // p,
q
by A24, A25, A27, AFF_1:5;
A71:
not
LIN q,
c9,
c
proof
A72:
now not q = c9assume
q = c9
;
contradictionthen
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;
verum end;
assume A73:
LIN q,
c9,
c
;
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;
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;
verum end;
hence
A // C
;
verum
end;
end;
( AP is satisfying_DES2_3 implies AP is satisfying_DES2_1 )
proof
assume A77:
AP is
satisfying_DES2_3
;
AP is satisfying_DES2_1
thus
AP is
satisfying_DES2_1
verumproof
let A be
Subset of
AP;
AFF_3:def 6 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,c9let P,
C be
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,c9let a,
a9,
b,
b9,
c,
c9,
p,
q be
Element of
AP;
( 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
;
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
;
contradiction
A102:
q <> c
proof
assume A103:
q = c
;
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;
verum
end;
A106:
a <> p
proof
assume
a = p
;
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;
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
;
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;
verum
end;
A113:
not
LIN p,
a,
a9
proof
assume A114:
LIN p,
a,
a9
;
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;
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
;
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;
verum
end;
A123:
not
LIN q,
c,
c9
proof
assume A124:
LIN q,
c,
c9
;
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;
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)
;
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;
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;
verum
end;
end;
hence
( AP is satisfying_DES2_1 iff AP is satisfying_DES2_3 )
by A1; verum