let AP be AffinPlane; ( 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
;
AP is satisfying_DES2_2
thus
AP is
satisfying_DES2_2
verumproof
let A be
Subset of
AP;
AFF_3:def 7 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 // Plet 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 // 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 // Plet 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 // 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
;
A // P
A24:
LIN q,
c9,
b9
by A21, AFF_1:6;
A25:
c <> c9
proof
assume
c = c9
;
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;
verum
end;
A26:
b <> b9
proof
A27:
now ( b = p implies not b in C )assume that A28:
b = p
and
b in C
;
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;
verum end;
A29:
(
LIN b,
p,
a &
LIN b,
p,
b )
by A18, AFF_1:6, AFF_1:7;
assume A30:
b = b9
;
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;
verum
end;
A34:
a <> p
proof
assume A35:
a = p
;
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;
verum
end;
A38:
q <> c
proof
assume
q = c
;
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;
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
;
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;
verum
end;
A47:
c9 <> q
proof
assume
c9 = q
;
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;
verum
end;
A49:
not
LIN q,
c9,
c
proof
A50:
LIN q,
c,
c
by AFF_1:7;
assume A51:
LIN q,
c9,
c
;
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;
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
;
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;
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)
;
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;
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)
;
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;
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)
;
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;
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;
verum
end;
end;
( AP is satisfying_DES2_2 implies AP is satisfying_DES2 )
proof
assume A74:
AP is
satisfying_DES2_2
;
AP is satisfying_DES2
thus
AP is
satisfying_DES2
verumproof
let A be
Subset of
AP;
AFF_3:def 5 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,qlet 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 & 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,qlet 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 & 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
;
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
A99:
not
LIN p,
a,
a9
proof
A100:
LIN p,
a,
a
by AFF_1:7;
assume
LIN p,
a,
a9
;
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;
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
;
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;
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
;
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;
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)
;
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;
verum
end;
A118:
q <> c
proof
assume
q = c
;
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;
verum
end;
A119:
Line (
a,
c)
<> Line (
p,
q)
proof
assume
Line (
a,
c)
= Line (
p,
q)
;
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;
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
;
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;
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;
verum
end;
end;
hence
( AP is satisfying_DES2 iff AP is satisfying_DES2_2 )
by A1; verum