let AS be AffinSpace; ( IncProjSp_of AS is Pappian implies AS is Pappian )
set XX = IncProjSp_of AS;
assume A1:
IncProjSp_of AS is Pappian
; AS is Pappian
for M, N being Subset of AS
for o, a, b, c, a9, b9, c9 being Element of AS st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9
proof
let M,
N be
Subset of
AS;
for o, a, b, c, a9, b9, c9 being Element of AS st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds
a,c9 // c,a9let o,
a,
b,
c,
a9,
b9,
c9 be
Element of
AS;
( M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 implies a,c9 // c,a9 )
assume that A2:
M is
being_line
and A3:
N is
being_line
and A4:
M <> N
and A5:
o in M
and A6:
o in N
and A7:
o <> a
and A8:
o <> a9
and A9:
o <> b
and A10:
o <> b9
and A11:
o <> c
and A12:
o <> c9
and A13:
a in M
and A14:
b in M
and A15:
c in M
and A16:
a9 in N
and A17:
b9 in N
and A18:
c9 in N
and A19:
a,
b9 // b,
a9
and A20:
b,
c9 // c,
b9
;
a,c9 // c,a9
A21:
b <> c9
by A2, A3, A4, A5, A6, A9, A14, A18, AFF_1:18;
then A22:
Line (
b,
c9) is
being_line
by AFF_1:def 3;
c <> a9
by A2, A3, A4, A5, A6, A8, A15, A16, AFF_1:18;
then A23:
Line (
c,
a9) is
being_line
by AFF_1:def 3;
A24:
b <> a9
by A2, A3, A4, A5, A6, A8, A14, A16, AFF_1:18;
then A25:
Line (
b,
a9) is
being_line
by AFF_1:def 3;
A26:
c <> b9
by A2, A3, A4, A5, A6, A10, A15, A17, AFF_1:18;
then A27:
Line (
c,
b9) is
being_line
by AFF_1:def 3;
reconsider A3 =
[M,1],
B3 =
[N,1] as
Element of the
Lines of
(IncProjSp_of AS) by A2, A3, Th23;
reconsider p =
o,
a1 =
a9,
a2 =
c9,
a3 =
b9,
b1 =
a,
b2 =
c,
b3 =
b as
Element of the
Points of
(IncProjSp_of AS) by Th20;
A28:
p on A3
by A2, A5, Th26;
A29:
a <> b9
by A2, A3, A4, A5, A6, A7, A13, A17, AFF_1:18;
then A30:
Line (
a,
b9) is
being_line
by AFF_1:def 3;
then reconsider c1 =
LDir (Line (b,c9)),
c2 =
LDir (Line (a,b9)) as
Element of the
Points of
(IncProjSp_of AS) by A22, Th20;
A31:
b1 on A3
by A2, A13, Th26;
a <> c9
by A2, A3, A4, A5, A6, A7, A13, A18, AFF_1:18;
then A32:
Line (
a,
c9) is
being_line
by AFF_1:def 3;
then reconsider A1 =
[(Line (b,c9)),1],
A2 =
[(Line (b,a9)),1],
B1 =
[(Line (a,b9)),1],
B2 =
[(Line (c,b9)),1],
C1 =
[(Line (c,a9)),1],
C2 =
[(Line (a,c9)),1] as
Element of the
Lines of
(IncProjSp_of AS) by A30, A25, A22, A27, A23, Th23;
A33:
c2 on B1
by A30, Th30;
A34:
b3 on A3
by A2, A14, Th26;
A35:
b2 on A3
by A2, A15, Th26;
consider Y being
Subset of
AS such that A36:
M c= Y
and A37:
N c= Y
and A38:
Y is
being_plane
by A2, A3, A5, A6, AFF_4:38;
reconsider C39 =
[(PDir Y),2] as
Element of the
Lines of
(IncProjSp_of AS) by A38, Th23;
A39:
c1 on C39
by A14, A18, A36, A37, A38, A21, A22, Th31, AFF_4:19;
A40:
c2 on C39
by A13, A17, A36, A37, A38, A29, A30, Th31, AFF_4:19;
A41:
a1 on B3
by A3, A16, Th26;
A42:
a3 on B3
by A3, A17, Th26;
A43:
p on B3
by A3, A6, Th26;
b9 in Line (
a,
b9)
by AFF_1:15;
then A44:
a3 on B1
by A30, Th26;
a in Line (
a,
b9)
by AFF_1:15;
then A45:
b1 on B1
by A30, Th26;
A46:
c in Line (
c,
a9)
by AFF_1:15;
then A47:
b2 on C1
by A23, Th26;
Line (
b,
c9)
// Line (
c,
b9)
by A20, A21, A26, AFF_1:37;
then
Line (
b,
c9)
'||' Line (
c,
b9)
by A22, A27, AFF_4:40;
then A48:
c1 on B2
by A22, A27, Th28;
A49:
c9 in Line (
a,
c9)
by AFF_1:15;
then A50:
a2 on C2
by A32, Th26;
b9 in Line (
c,
b9)
by AFF_1:15;
then A51:
a3 on B2
by A27, Th26;
c in Line (
c,
b9)
by AFF_1:15;
then A52:
b2 on B2
by A27, Th26;
c9 in Line (
b,
c9)
by AFF_1:15;
then A53:
a2 on A1
by A22, Th26;
b in Line (
b,
c9)
by AFF_1:15;
then A54:
b3 on A1
by A22, Th26;
A55:
a2 on B3
by A3, A18, Th26;
Line (
a,
b9)
// Line (
b,
a9)
by A19, A29, A24, AFF_1:37;
then
Line (
a,
b9)
'||' Line (
b,
a9)
by A30, A25, AFF_4:40;
then A56:
c2 on A2
by A30, A25, Th28;
A57:
a in Line (
a,
c9)
by AFF_1:15;
then A58:
b1 on C2
by A32, Th26;
a9 in Line (
b,
a9)
by AFF_1:15;
then A59:
a1 on A2
by A25, Th26;
b in Line (
b,
a9)
by AFF_1:15;
then A60:
b3 on A2
by A25, Th26;
A61:
a9 in Line (
c,
a9)
by AFF_1:15;
then A62:
a1 on C1
by A23, Th26;
A63:
c1 on A1
by A22, Th30;
now ( b1 <> b2 & b2 <> b3 & b3 <> b1 implies a,c9 // c,a9 )A64:
A3 <> B3
proof
assume
A3 = B3
;
contradiction
then M =
[N,1] `1
.=
N
;
hence
contradiction
by A4;
verum
end;
( not
p on C1 & not
p on C2 )
proof
assume
(
p on C1 or
p on C2 )
;
contradiction
then
(
a1 on A3 or
a2 on A3 )
by A7, A11, A28, A31, A35, A58, A50, A47, A62, Lm2;
hence
contradiction
by A8, A12, A28, A43, A41, A55, A64, INCPROJ:def 4;
verum
end; then consider c3 being
Element of the
Points of
(IncProjSp_of AS) such that A65:
c3 on C1
and A66:
c3 on C2
by A28, A31, A35, A43, A41, A55, A58, A50, A47, A62, A64, INCPROJ:def 8;
A67:
{a2,b1,c3} on C2
by A58, A50, A66, INCSP_1:2;
A68:
{a1,b3,c2} on A2
by A60, A59, A56, INCSP_1:2;
A69:
{a3,b1,c2} on B1
by A45, A44, A33, INCSP_1:2;
assume that A70:
b1 <> b2
and A71:
b2 <> b3
and A72:
b3 <> b1
;
a,c9 // c,a9A73:
p,
b1,
b2,
b3 are_mutually_distinct
by A7, A9, A11, A70, A71, A72, ZFMISC_1:def 6;
(
a1 <> a2 &
a2 <> a3 &
a1 <> a3 )
proof
A74:
now not a9 = c9assume
a9 = c9
;
contradictionthen
a,
b9 // c,
b9
by A19, A20, A24, AFF_1:5;
hence
contradiction
by A2, A3, A4, A5, A6, A7, A10, A13, A15, A17, A70, AFF_4:9;
verum end;
assume
( not
a1 <> a2 or not
a2 <> a3 or not
a1 <> a3 )
;
contradiction
hence
contradiction
by A2, A3, A4, A5, A6, A7, A9, A10, A13, A14, A15, A17, A19, A20, A71, A72, A74, AFF_4:9;
verum
end; then A75:
p,
a1,
a2,
a3 are_mutually_distinct
by A8, A10, A12, ZFMISC_1:def 6;
A76:
{a1,a2,a3} on B3
by A41, A55, A42, INCSP_1:2;
A77:
{b1,b2,b3} on A3
by A31, A35, A34, INCSP_1:2;
A78:
{a3,b2,c1} on B2
by A51, A52, A48, INCSP_1:2;
A79:
{a2,b3,c1} on A1
by A53, A54, A63, INCSP_1:2;
A80:
p on B3
by A3, A6, Th26;
A81:
p on A3
by A2, A5, Th26;
A82:
{c1,c2} on C39
by A39, A40, INCSP_1:1;
{a1,b2,c3} on C1
by A47, A62, A65, INCSP_1:2;
then
c3 on C39
by A1, A75, A73, A64, A81, A80, A79, A69, A68, A78, A67, A77, A76, A82, INCPROJ:def 14;
then
c3 is not
Element of
AS
by Th27;
then consider Y being
Subset of
AS such that A83:
c3 = LDir Y
and A84:
Y is
being_line
by Th20;
Y '||' Line (
c,
a9)
by A23, A65, A83, A84, Th28;
then A85:
Y // Line (
c,
a9)
by A23, A84, AFF_4:40;
Y '||' Line (
a,
c9)
by A32, A66, A83, A84, Th28;
then
Y // Line (
a,
c9)
by A32, A84, AFF_4:40;
then
Line (
a,
c9)
// Line (
c,
a9)
by A85, AFF_1:44;
hence
a,
c9 // c,
a9
by A57, A49, A46, A61, AFF_1:39;
verum end;
hence
a,
c9 // c,
a9
by A2, A3, A4, A5, A6, A9, A10, A12, A14, A15, A16, A17, A18, A19, A20, Th48;
verum
end;
hence
AS is Pappian
by AFF_2:def 2; verum