begin
theorem Th16:
for
CPS being
CollProjectiveSpace st ( for
p,
p1,
q,
q1,
r2 being
Point of
CPS ex
r,
r1 being
Point of
CPS st
(
p,
q,
r is_collinear &
p1,
q1,
r1 is_collinear &
r2,
r,
r1 is_collinear ) ) holds
for
a being
POINT of
(IncProjSp_of CPS) for
M,
N being
LINE of
(IncProjSp_of CPS) ex
b,
c being
POINT of
(IncProjSp_of CPS) ex
S being
LINE of
(IncProjSp_of CPS) st
(
a on S &
b on S &
c on S &
b on M &
c on N )
theorem Th17:
for
CPS being
CollProjectiveSpace st ( for
p1,
r2,
q,
r1,
q1,
p,
r being
Point of
CPS st
p1,
r2,
q is_collinear &
r1,
q1,
q is_collinear &
p1,
r1,
p is_collinear &
r2,
q1,
p is_collinear &
p1,
q1,
r is_collinear &
r2,
r1,
r is_collinear &
p,
q,
r is_collinear & not
p1,
r2,
q1 is_collinear & not
p1,
r2,
r1 is_collinear & not
p1,
r1,
q1 is_collinear holds
r2,
r1,
q1 is_collinear ) holds
for
p,
q,
r,
s,
a,
b,
c being
POINT of
(IncProjSp_of CPS) for
L,
Q,
R,
S,
A,
B,
C being
LINE of
(IncProjSp_of CPS) st not
q on L & not
r on L & not
p on Q & not
s on Q & not
p on R & not
r on R &
{a,p,s} on L &
{a,q,r} on Q &
{b,q,s} on R &
{b,p,r} on S &
{c,p,q} on A &
{c,r,s} on B &
{a,b} on C holds
not
c on C
theorem Th18:
for
CPS being
CollProjectiveSpace st ( for
o,
p1,
p2,
p3,
q1,
q2,
q3,
r1,
r2,
r3 being
Point of
CPS st
o <> q1 &
p1 <> q1 &
o <> q2 &
p2 <> q2 &
o <> q3 &
p3 <> q3 & not
o,
p1,
p2 is_collinear & not
o,
p1,
p3 is_collinear & not
o,
p2,
p3 is_collinear &
p1,
p2,
r3 is_collinear &
q1,
q2,
r3 is_collinear &
p2,
p3,
r1 is_collinear &
q2,
q3,
r1 is_collinear &
p1,
p3,
r2 is_collinear &
q1,
q3,
r2 is_collinear &
o,
p1,
q1 is_collinear &
o,
p2,
q2 is_collinear &
o,
p3,
q3 is_collinear holds
r1,
r2,
r3 is_collinear ) holds
for
o,
b1,
a1,
b2,
a2,
b3,
a3,
r,
s,
t being
POINT of
(IncProjSp_of CPS) for
C1,
C2,
C3,
A1,
A2,
A3,
B1,
B2,
B3 being
LINE of
(IncProjSp_of CPS) st
{o,b1,a1} on C1 &
{o,a2,b2} on C2 &
{o,a3,b3} on C3 &
{a3,a2,t} on A1 &
{a3,r,a1} on A2 &
{a2,s,a1} on A3 &
{t,b2,b3} on B1 &
{b1,r,b3} on B2 &
{b1,s,b2} on B3 &
C1,
C2,
C3 are_mutually_different &
o <> a1 &
o <> a2 &
o <> a3 &
o <> b1 &
o <> b2 &
o <> b3 &
a1 <> b1 &
a2 <> b2 &
a3 <> b3 holds
ex
O being
LINE of
(IncProjSp_of CPS) st
{r,s,t} on O
theorem Th19:
for
CPS being
CollProjectiveSpace st ( for
o,
p1,
p2,
p3,
q1,
q2,
q3,
r1,
r2,
r3 being
Point of
CPS st
o <> p2 &
o <> p3 &
p2 <> p3 &
p1 <> p2 &
p1 <> p3 &
o <> q2 &
o <> q3 &
q2 <> q3 &
q1 <> q2 &
q1 <> q3 & not
o,
p1,
q1 is_collinear &
o,
p1,
p2 is_collinear &
o,
p1,
p3 is_collinear &
o,
q1,
q2 is_collinear &
o,
q1,
q3 is_collinear &
p1,
q2,
r3 is_collinear &
q1,
p2,
r3 is_collinear &
p1,
q3,
r2 is_collinear &
p3,
q1,
r2 is_collinear &
p2,
q3,
r1 is_collinear &
p3,
q2,
r1 is_collinear holds
r1,
r2,
r3 is_collinear ) holds
for
o,
a1,
a2,
a3,
b1,
b2,
b3,
c1,
c2,
c3 being
POINT of
(IncProjSp_of CPS) for
A1,
A2,
A3,
B1,
B2,
B3,
C1,
C2,
C3 being
LINE of
(IncProjSp_of CPS) st
o,
a1,
a2,
a3 are_mutually_different &
o,
b1,
b2,
b3 are_mutually_different &
A3 <> B3 &
o on A3 &
o on B3 &
{a2,b3,c1} on A1 &
{a3,b1,c2} on B1 &
{a1,b2,c3} on C1 &
{a1,b3,c2} on A2 &
{a3,b2,c1} on B2 &
{a2,b1,c3} on C2 &
{b1,b2,b3} on A3 &
{a1,a2,a3} on B3 &
{c1,c2} on C3 holds
c3 on C3
definition
let IT be
IncProjStr ;
attr IT is
Fanoian means :
Def12:
for
p,
q,
r,
s,
a,
b,
c being
POINT of
IT for
L,
Q,
R,
S,
A,
B,
C being
LINE of
IT st not
q on L & not
r on L & not
p on Q & not
s on Q & not
p on R & not
r on R & not
q on S & not
s on S &
{a,p,s} on L &
{a,q,r} on Q &
{b,q,s} on R &
{b,p,r} on S &
{c,p,q} on A &
{c,r,s} on B &
{a,b} on C holds
not
c on C;
end;
::
deftheorem Def12 defines
Fanoian INCPROJ:def 12 :
for IT being IncProjStr holds
( IT is Fanoian iff for p, q, r, s, a, b, c being POINT of IT
for L, Q, R, S, A, B, C being LINE of IT st not q on L & not r on L & not p on Q & not s on Q & not p on R & not r on R & not q on S & not s on S & {a,p,s} on L & {a,q,r} on Q & {b,q,s} on R & {b,p,r} on S & {c,p,q} on A & {c,r,s} on B & {a,b} on C holds
not c on C );
definition
let IT be
IncProjStr ;
attr IT is
Desarguesian means :
Def13:
for
o,
b1,
a1,
b2,
a2,
b3,
a3,
r,
s,
t being
POINT of
IT for
C1,
C2,
C3,
A1,
A2,
A3,
B1,
B2,
B3 being
LINE of
IT st
{o,b1,a1} on C1 &
{o,a2,b2} on C2 &
{o,a3,b3} on C3 &
{a3,a2,t} on A1 &
{a3,r,a1} on A2 &
{a2,s,a1} on A3 &
{t,b2,b3} on B1 &
{b1,r,b3} on B2 &
{b1,s,b2} on B3 &
C1,
C2,
C3 are_mutually_different &
o <> a1 &
o <> a2 &
o <> a3 &
o <> b1 &
o <> b2 &
o <> b3 &
a1 <> b1 &
a2 <> b2 &
a3 <> b3 holds
ex
O being
LINE of
IT st
{r,s,t} on O;
end;
::
deftheorem Def13 defines
Desarguesian INCPROJ:def 13 :
for IT being IncProjStr holds
( IT is Desarguesian iff for o, b1, a1, b2, a2, b3, a3, r, s, t being POINT of IT
for C1, C2, C3, A1, A2, A3, B1, B2, B3 being LINE of IT st {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_different & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a1 <> b1 & a2 <> b2 & a3 <> b3 holds
ex O being LINE of IT st {r,s,t} on O );
definition
let IT be
IncProjStr ;
attr IT is
Pappian means :
Def14:
for
o,
a1,
a2,
a3,
b1,
b2,
b3,
c1,
c2,
c3 being
POINT of
IT for
A1,
A2,
A3,
B1,
B2,
B3,
C1,
C2,
C3 being
LINE of
IT st
o,
a1,
a2,
a3 are_mutually_different &
o,
b1,
b2,
b3 are_mutually_different &
A3 <> B3 &
o on A3 &
o on B3 &
{a2,b3,c1} on A1 &
{a3,b1,c2} on B1 &
{a1,b2,c3} on C1 &
{a1,b3,c2} on A2 &
{a3,b2,c1} on B2 &
{a2,b1,c3} on C2 &
{b1,b2,b3} on A3 &
{a1,a2,a3} on B3 &
{c1,c2} on C3 holds
c3 on C3;
end;
::
deftheorem Def14 defines
Pappian INCPROJ:def 14 :
for IT being IncProjStr holds
( IT is Pappian iff for o, a1, a2, a3, b1, b2, b3, c1, c2, c3 being POINT of IT
for A1, A2, A3, B1, B2, B3, C1, C2, C3 being LINE of IT st o,a1,a2,a3 are_mutually_different & o,b1,b2,b3 are_mutually_different & A3 <> B3 & o on A3 & o on B3 & {a2,b3,c1} on A1 & {a3,b1,c2} on B1 & {a1,b2,c3} on C1 & {a1,b3,c2} on A2 & {a3,b2,c1} on B2 & {a2,b1,c3} on C2 & {b1,b2,b3} on A3 & {a1,a2,a3} on B3 & {c1,c2} on C3 holds
c3 on C3 );