:: Incidence Projective Spaces :: by Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski :: :: Received October 4, 1990 :: Copyright (c) 1990 Association of Mizar Users
for S being IncProjStr holds ( S is partial iff for p, q being POINT of S for P, Q being LINE of S st p on P & q on P & p on Q & q on Q & not p = q holds P = Q );
for S being IncProjStr holds ( S is up-3-rank iff for P being LINE of S ex a, b, c being POINT of S st ( a <> b & b <> c & c <> a & a on P & b on P & c on P ) );
for S being IncProjStr holds ( S is Vebleian iff for a, b, c, d, p, q being POINT of S for M, N, P, Q being LINE of S st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds ex q being POINT of S st ( q on P & q on Q ) );
let IT be IncProjStr ; attrIT is Fanoian means :Def18: :: INCPROJ:def 18 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;
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 );
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 );