let AP be AffinPlane; ( AP is Pappian implies AP is Desarguesian )
assume A1:
AP is Pappian
; AP is Desarguesian
then
AP is satisfying_pap
by Th9;
then A2:
AP is satisfying_PPAP
by A1, Th10;
let A be Subset of AP; AFF_2:def 4 for P, C being Subset of AP
for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let P, C be Subset of AP; for o, a, b, c, a9, b9, c9 being Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let o, a, b, c, a9, b9, c9 be Element of AP; ( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
assume that
A3:
o in A
and
A4:
o in P
and
A5:
o in C
and
A6:
o <> a
and
A7:
o <> b
and
o <> c
and
A8:
a in A
and
A9:
a9 in A
and
A10:
b in P
and
A11:
b9 in P
and
A12:
c in C
and
A13:
c9 in C
and
A14:
A is being_line
and
A15:
P is being_line
and
A16:
C is being_line
and
A17:
A <> P
and
A18:
A <> C
and
A19:
a,b // a9,b9
and
A20:
a,c // a9,c9
; b,c // b9,c9
assume A21:
not b,c // b9,c9
; contradiction
then A22:
b <> c
by AFF_1:3;
A23:
a <> c
by A3, A5, A6, A8, A12, A14, A16, A18, AFF_1:18;
A24:
not b in C
proof
assume A25:
b in C
;
contradiction
then
b9 in C
by A4, A5, A7, A10, A11, A15, A16, AFF_1:18;
hence
contradiction
by A12, A13, A16, A21, A25, AFF_1:51;
verum
end;
A26:
a <> b
by A3, A4, A6, A8, A10, A14, A15, A17, AFF_1:18;
A27:
a <> a9
proof
assume A28:
a = a9
;
contradiction
then
LIN a,
c,
c9
by A20, AFF_1:def 1;
then
LIN c,
c9,
a
by AFF_1:6;
then A29:
(
c = c9 or
a in C )
by A12, A13, A16, AFF_1:25;
LIN a,
b,
b9
by A19, A28, AFF_1:def 1;
then
LIN b,
b9,
a
by AFF_1:6;
then
(
b = b9 or
a in P )
by A10, A11, A15, AFF_1:25;
hence
contradiction
by A3, A4, A5, A6, A8, A14, A15, A16, A17, A18, A21, A29, AFF_1:2, AFF_1:18;
verum
end;
set M = Line (b9,c9);
set N = Line (a9,b9);
set D = Line (a9,c9);
A30:
a9 <> b9
proof
A31:
a9,
c9 // c,
a
by A20, AFF_1:4;
assume A32:
a9 = b9
;
contradiction
then
a9 in C
by A3, A4, A5, A9, A11, A14, A15, A17, AFF_1:18;
then
(
a in C or
a9 = c9 )
by A12, A13, A16, A31, AFF_1:48;
hence
contradiction
by A3, A5, A6, A8, A14, A16, A18, A21, A32, AFF_1:3, AFF_1:18;
verum
end;
then A33:
Line (a9,b9) is being_line
by AFF_1:24;
A34:
a9 <> c9
proof
assume
a9 = c9
;
contradiction
then A35:
a9 in P
by A3, A4, A5, A9, A13, A14, A16, A18, AFF_1:18;
a9,
b9 // b,
a
by A19, AFF_1:4;
then
a in P
by A10, A11, A15, A30, A35, AFF_1:48;
hence
contradiction
by A3, A4, A6, A8, A14, A15, A17, AFF_1:18;
verum
end;
A36:
not LIN a9,b9,c9
proof
assume A37:
LIN a9,
b9,
c9
;
contradiction
then
a9,
b9 // a9,
c9
by AFF_1:def 1;
then
a9,
b9 // a,
c
by A20, A34, AFF_1:5;
then
a,
b // a,
c
by A19, A30, AFF_1:5;
then
LIN a,
b,
c
by AFF_1:def 1;
then
LIN b,
c,
a
by AFF_1:6;
then
b,
c // b,
a
by AFF_1:def 1;
then
b,
c // a,
b
by AFF_1:4;
then A38:
b,
c // a9,
b9
by A19, A26, AFF_1:5;
LIN b9,
c9,
a9
by A37, AFF_1:6;
then
b9,
c9 // b9,
a9
by AFF_1:def 1;
then
b9,
c9 // a9,
b9
by AFF_1:4;
hence
contradiction
by A21, A30, A38, AFF_1:5;
verum
end;
A39:
not LIN a,b,c
proof
assume
LIN a,
b,
c
;
contradiction
then
a,
b // a,
c
by AFF_1:def 1;
then
a,
b // a9,
c9
by A20, A23, AFF_1:5;
then
a9,
b9 // a9,
c9
by A19, A26, AFF_1:5;
hence
contradiction
by A36, AFF_1:def 1;
verum
end;
A40:
now b,c // A
LIN o,
a,
a9
by A3, A8, A9, A14, AFF_1:21;
then
o,
a // o,
a9
by AFF_1:def 1;
then A41:
a9,
o // a,
o
by AFF_1:4;
set M =
Line (
b,
c);
set N =
Line (
a,
b);
set D =
Line (
a,
c);
A42:
Line (
a,
b) is
being_line
by A26, AFF_1:24;
Line (
b,
c) is
being_line
by A22, AFF_1:24;
then consider K being
Subset of
AP such that A43:
o in K
and A44:
Line (
b,
c)
// K
by AFF_1:49;
A45:
K is
being_line
by A44, AFF_1:36;
A46:
a in Line (
a,
b)
by A26, AFF_1:24;
A47:
b in Line (
a,
b)
by A26, AFF_1:24;
A48:
(
b in Line (
b,
c) &
c in Line (
b,
c) )
by A22, AFF_1:24;
not
Line (
a,
b)
// K
proof
assume
Line (
a,
b)
// K
;
contradiction
then
Line (
a,
b)
// Line (
b,
c)
by A44, AFF_1:44;
then
c in Line (
a,
b)
by A48, A47, AFF_1:45;
hence
contradiction
by A39, A42, A46, A47, AFF_1:21;
verum
end; then consider p being
Element of
AP such that A49:
p in Line (
a,
b)
and A50:
p in K
by A42, A45, AFF_1:58;
A51:
b,
c // p,
o
by A48, A43, A44, A50, AFF_1:39;
A52:
o <> p
proof
assume
o = p
;
contradiction
then
LIN o,
a,
b
by A42, A46, A47, A49, AFF_1:21;
then
b in A
by A3, A6, A8, A14, AFF_1:25;
hence
contradiction
by A3, A4, A7, A10, A14, A15, A17, AFF_1:18;
verum
end; set R =
Line (
a9,
p);
A53:
p <> a9
proof
assume
p = a9
;
contradiction
then
b in A
by A8, A9, A14, A27, A42, A46, A47, A49, AFF_1:18;
hence
contradiction
by A3, A4, A7, A10, A14, A15, A17, AFF_1:18;
verum
end; then A54:
Line (
a9,
p) is
being_line
by AFF_1:24;
Line (
a,
c) is
being_line
by A23, AFF_1:24;
then consider T being
Subset of
AP such that A55:
p in T
and A56:
Line (
a,
c)
// T
by AFF_1:49;
A57:
(
a in Line (
a,
c) &
c in Line (
a,
c) )
by A23, AFF_1:24;
A58:
not
C // T
proof
assume
C // T
;
contradiction
then
C // Line (
a,
c)
by A56, AFF_1:44;
then
a in C
by A12, A57, AFF_1:45;
hence
contradiction
by A3, A5, A6, A8, A14, A16, A18, AFF_1:18;
verum
end;
T is
being_line
by A56, AFF_1:36;
then consider q being
Element of
AP such that A59:
q in C
and A60:
q in T
by A16, A58, AFF_1:58;
A61:
p,
q // a,
c
by A57, A55, A56, A60, AFF_1:39;
then A62:
b,
q // a,
o
by A2, A5, A12, A16, A42, A46, A47, A49, A59, A51;
A63:
(
a9 in Line (
a9,
p) &
p in Line (
a9,
p) )
by A53, AFF_1:24;
assume
not
b,
c // A
;
contradictionthen A64:
K <> A
by A48, A44, AFF_1:40;
not
b,
q // Line (
a9,
p)
proof
assume
b,
q // Line (
a9,
p)
;
contradiction
then A65:
a,
o // Line (
a9,
p)
by A24, A59, A62, AFF_1:32;
a,
o // A
by A3, A8, A14, AFF_1:40, AFF_1:41;
then
p in A
by A6, A9, A63, A65, AFF_1:45, AFF_1:53;
hence
contradiction
by A3, A14, A43, A45, A50, A52, A64, AFF_1:18;
verum
end; then consider r being
Element of
AP such that A66:
r in Line (
a9,
p)
and A67:
LIN b,
q,
r
by A54, AFF_1:59;
A68:
now ( r = q implies r,b // o,a9 )assume
r = q
;
r,b // o,a9then
b,
r // a,
o
by A2, A5, A12, A16, A42, A46, A47, A49, A59, A51, A61;
then A69:
r,
b // o,
a
by AFF_1:4;
LIN o,
a,
a9
by A3, A8, A9, A14, AFF_1:21;
then
o,
a // o,
a9
by AFF_1:def 1;
hence
r,
b // o,
a9
by A6, A69, AFF_1:5;
verum end;
LIN q,
r,
b
by A67, AFF_1:6;
then
q,
r // q,
b
by AFF_1:def 1;
then
r,
q // b,
q
by AFF_1:4;
then
r,
q // a,
o
by A24, A59, A62, AFF_1:5;
then A70:
a9,
o // r,
q
by A6, A41, AFF_1:5;
LIN b,
a,
p
by A42, A46, A47, A49, AFF_1:21;
then
b,
a // b,
p
by AFF_1:def 1;
then
a,
b // p,
b
by AFF_1:4;
then A71:
p,
b // a9,
b9
by A19, A26, AFF_1:5;
LIN r,
b,
q
by A67, AFF_1:6;
then
r,
b // r,
q
by AFF_1:def 1;
then
a9,
o // r,
b
by A70, A68, AFF_1:4, AFF_1:5;
then A72:
p,
o // r,
b9
by A2, A4, A10, A11, A15, A54, A63, A66, A71;
p,
q // a9,
c9
by A20, A23, A61, AFF_1:5;
then A73:
p,
o // r,
c9
by A2, A5, A13, A16, A59, A54, A63, A66, A70;
then
r,
c9 // r,
b9
by A52, A72, AFF_1:5;
then
LIN r,
c9,
b9
by AFF_1:def 1;
then
LIN c9,
b9,
r
by AFF_1:6;
then
c9,
b9 // c9,
r
by AFF_1:def 1;
then A74:
r,
c9 // b9,
c9
by AFF_1:4;
b,
c // r,
c9
by A52, A51, A73, AFF_1:5;
then
r = c9
by A21, A74, AFF_1:5;
then
p,
o // b9,
c9
by A72, AFF_1:4;
hence
contradiction
by A21, A52, A51, AFF_1:5;
verum end;
A75:
b9 in Line (a9,b9)
by A30, AFF_1:24;
A76:
b9 <> c9
by A21, AFF_1:3;
then A77:
( b9 in Line (b9,c9) & c9 in Line (b9,c9) )
by AFF_1:24;
Line (b9,c9) is being_line
by A76, AFF_1:24;
then consider K being Subset of AP such that
A78:
o in K
and
A79:
Line (b9,c9) // K
by AFF_1:49;
A80:
K is being_line
by A79, AFF_1:36;
A81:
a9 in Line (a9,b9)
by A30, AFF_1:24;
not Line (a9,b9) // K
proof
assume
Line (
a9,
b9)
// K
;
contradiction
then
Line (
a9,
b9)
// Line (
b9,
c9)
by A79, AFF_1:44;
then
c9 in Line (
a9,
b9)
by A77, A75, AFF_1:45;
hence
contradiction
by A36, A33, A81, A75, AFF_1:21;
verum
end;
then consider p being Element of AP such that
A82:
p in Line (a9,b9)
and
A83:
p in K
by A33, A80, AFF_1:58;
A84:
o <> a9
proof
assume A85:
o = a9
;
contradiction
a9,
b9 // b,
a
by A19, AFF_1:4;
then
a in P
by A4, A10, A11, A15, A30, A85, AFF_1:48;
hence
contradiction
by A3, A4, A6, A8, A14, A15, A17, AFF_1:18;
verum
end;
A86:
o <> p
proof
assume
o = p
;
contradiction
then
LIN o,
a9,
b9
by A33, A81, A75, A82, AFF_1:21;
then A87:
b9 in A
by A3, A9, A14, A84, AFF_1:25;
a9,
b9 // a,
b
by A19, AFF_1:4;
then
b in A
by A8, A9, A14, A30, A87, AFF_1:48;
hence
contradiction
by A3, A4, A7, A10, A14, A15, A17, AFF_1:18;
verum
end;
Line (a9,c9) is being_line
by A34, AFF_1:24;
then consider T being Subset of AP such that
A88:
p in T
and
A89:
Line (a9,c9) // T
by AFF_1:49;
A90:
T is being_line
by A89, AFF_1:36;
A91:
( a9 in Line (a9,c9) & c9 in Line (a9,c9) )
by A34, AFF_1:24;
not C // T
proof
assume
C // T
;
contradiction
then
C // Line (
a9,
c9)
by A89, AFF_1:44;
then
a9 in C
by A13, A91, AFF_1:45;
hence
contradiction
by A3, A5, A9, A14, A16, A18, A84, AFF_1:18;
verum
end;
then consider q being Element of AP such that
A92:
q in C
and
A93:
q in T
by A16, A90, AFF_1:58;
A94:
b9,c9 // p,o
by A77, A78, A79, A83, AFF_1:39;
A95:
o <> b9
proof
assume A96:
o = b9
;
contradiction
b9,
a9 // a,
b
by A19, AFF_1:4;
then
b in A
by A3, A8, A9, A14, A30, A96, AFF_1:48;
hence
contradiction
by A3, A4, A7, A10, A14, A15, A17, AFF_1:18;
verum
end;
A97:
b9 <> q
proof
assume
b9 = q
;
contradiction
then
P = C
by A4, A5, A11, A15, A16, A95, A92, AFF_1:18;
hence
contradiction
by A10, A11, A12, A13, A15, A21, AFF_1:51;
verum
end;
set R = Line (a,p);
A98:
p <> a
proof
assume
p = a
;
contradiction
then
b9 in A
by A8, A9, A14, A27, A33, A81, A75, A82, AFF_1:18;
hence
contradiction
by A3, A4, A11, A14, A15, A17, A95, AFF_1:18;
verum
end;
then A99:
Line (a,p) is being_line
by AFF_1:24;
A100:
p,q // a9,c9
by A91, A88, A89, A93, AFF_1:39;
then A101:
b9,q // a9,o
by A2, A5, A13, A16, A33, A81, A75, A82, A92, A94;
A102:
( a in Line (a,p) & p in Line (a,p) )
by A98, AFF_1:24;
not b9,c9 // A
by A14, A21, A40, AFF_1:31;
then A103:
K <> A
by A77, A79, AFF_1:40;
not b9,q // Line (a,p)
proof
assume
b9,
q // Line (
a,
p)
;
contradiction
then A104:
a9,
o // Line (
a,
p)
by A101, A97, AFF_1:32;
a9,
o // A
by A3, A9, A14, AFF_1:40, AFF_1:41;
then
p in A
by A8, A84, A102, A104, AFF_1:45, AFF_1:53;
hence
contradiction
by A3, A14, A78, A80, A83, A86, A103, AFF_1:18;
verum
end;
then consider r being Element of AP such that
A105:
r in Line (a,p)
and
A106:
LIN b9,q,r
by A99, AFF_1:59;
A107:
now ( r = q implies r,b9 // o,a )assume
r = q
;
r,b9 // o,athen
b9,
r // a9,
o
by A2, A5, A13, A16, A33, A81, A75, A82, A92, A94, A100;
then A108:
r,
b9 // o,
a9
by AFF_1:4;
LIN o,
a9,
a
by A3, A8, A9, A14, AFF_1:21;
then
o,
a9 // o,
a
by AFF_1:def 1;
hence
r,
b9 // o,
a
by A84, A108, AFF_1:5;
verum end;
LIN b9,a9,p
by A33, A81, A75, A82, AFF_1:21;
then
b9,a9 // b9,p
by AFF_1:def 1;
then
p,b9 // a9,b9
by AFF_1:4;
then A109:
p,b9 // a,b
by A19, A30, AFF_1:5;
LIN o,a,a9
by A3, A8, A9, A14, AFF_1:21;
then
o,a // o,a9
by AFF_1:def 1;
then A110:
a,o // a9,o
by AFF_1:4;
LIN q,r,b9
by A106, AFF_1:6;
then
q,r // q,b9
by AFF_1:def 1;
then
r,q // b9,q
by AFF_1:4;
then
r,q // a9,o
by A101, A97, AFF_1:5;
then A111:
a,o // r,q
by A84, A110, AFF_1:5;
LIN r,b9,q
by A106, AFF_1:6;
then
r,b9 // r,q
by AFF_1:def 1;
then
a,o // r,b9
by A111, A107, AFF_1:4, AFF_1:5;
then A112:
p,o // r,b
by A2, A4, A10, A11, A15, A99, A102, A105, A109;
p,q // a,c
by A20, A34, A100, AFF_1:5;
then A113:
p,o // r,c
by A2, A5, A12, A16, A92, A99, A102, A105, A111;
then
r,c // r,b
by A86, A112, AFF_1:5;
then
LIN r,c,b
by AFF_1:def 1;
then
LIN c,b,r
by AFF_1:6;
then
c,b // c,r
by AFF_1:def 1;
then A114:
b,c // r,c
by AFF_1:4;
b9,c9 // r,c
by A86, A94, A113, AFF_1:5;
then
r = c
by A21, A114, AFF_1:5;
then
b,c // p,o
by A112, AFF_1:4;
hence
contradiction
by A21, A86, A94, AFF_1:5; verum