:: Incidence Projective Spaces :: by Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski :: :: Received October 4, 1990 :: Copyright (c) 1990 Association of Mizar Users
for CPS being properCollSp for p being POINT of for P being LINE of for p' being Point of for P' being LINE of CPS st p = p' & P = P' holds ( p on P iff p' in P' )
for CPS being properCollSp for a, b, c being POINT of for a', b', c' being Point of st a = a' & b = b' & c = c' holds ( a',b',c' is_collinear iff ex P being LINE of st ( a on P & b on P & c on P ) )
for CPS being CollProjectiveSpace for a, b, c, d, p being POINT of for M, N, P, Q being LINE of 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 st ( q on P & q on Q )
for S being IncProjStr holds ( S is partial iff for p, q being POINT of for P, Q being LINE of 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 Vebleian iff for a, b, c, d, p, q being POINT of for M, N, P, Q being LINE of 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 st ( q on P & q on Q ) );
for IT being IncProjStr holds ( IT is Fanoian iff for p, q, r, s, a, b, c being POINT of for L, Q, R, S, A, B, C being LINE of 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 for C1, C2, C3, A1, A2, A3, B1, B2, B3 being LINE of 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 st {r,s,t}on O );