:: Incidence Projective Spaces :: by Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski :: :: Received October 4, 1990 :: Copyright (c) 1990-2011 Association of Mizar Users
:: deftheorem Def13 defines VebleianINCPROJ:def 13 : 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;
end;
:: deftheorem Def18 defines FanoianINCPROJ:def 18 : 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 );