:: by Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski

::

:: Received October 4, 1990

:: Copyright (c) 1990-2016 Association of Mizar Users

definition

let CPS be proper CollSp;

:: original: LINE

redefine mode LINE of CPS -> Subset of CPS;

coherence

for b_{1} being LINE of CPS holds b_{1} is Subset of CPS

end;
:: original: LINE

redefine mode LINE of CPS -> Subset of CPS;

coherence

for b

proof end;

definition

let CPS be proper CollSp;

{ B where B is Subset of CPS : B is LINE of CPS } is set ;

end;
func ProjectiveLines CPS -> set equals :: INCPROJ:def 1

{ B where B is Subset of CPS : B is LINE of CPS } ;

coherence { B where B is Subset of CPS : B is LINE of CPS } ;

{ B where B is Subset of CPS : B is LINE of CPS } is set ;

:: deftheorem defines ProjectiveLines INCPROJ:def 1 :

for CPS being proper CollSp holds ProjectiveLines CPS = { B where B is Subset of CPS : B is LINE of CPS } ;

for CPS being proper CollSp holds ProjectiveLines CPS = { B where B is Subset of CPS : B is LINE of CPS } ;

theorem Th1: :: INCPROJ:1

for CPS being proper CollSp

for x being set holds

( x is LINE of CPS iff x is Element of ProjectiveLines CPS )

for x being set holds

( x is LINE of CPS iff x is Element of ProjectiveLines CPS )

proof end;

definition

let CPS be proper CollSp;

ex b_{1} being Relation of the carrier of CPS,(ProjectiveLines CPS) st

for x, y being object holds

( [x,y] in b_{1} iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st

( y = Y & x in Y ) ) )

for b_{1}, b_{2} being Relation of the carrier of CPS,(ProjectiveLines CPS) st ( for x, y being object holds

( [x,y] in b_{1} iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st

( y = Y & x in Y ) ) ) ) & ( for x, y being object holds

( [x,y] in b_{2} iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st

( y = Y & x in Y ) ) ) ) holds

b_{1} = b_{2}

end;
func Proj_Inc CPS -> Relation of the carrier of CPS,(ProjectiveLines CPS) means :Def2: :: INCPROJ:def 2

for x, y being object holds

( [x,y] in it iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st

( y = Y & x in Y ) ) );

existence for x, y being object holds

( [x,y] in it iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st

( y = Y & x in Y ) ) );

ex b

for x, y being object holds

( [x,y] in b

( y = Y & x in Y ) ) )

proof end;

uniqueness for b

( [x,y] in b

( y = Y & x in Y ) ) ) ) & ( for x, y being object holds

( [x,y] in b

( y = Y & x in Y ) ) ) ) holds

b

proof end;

:: deftheorem Def2 defines Proj_Inc INCPROJ:def 2 :

for CPS being proper CollSp

for b_{2} being Relation of the carrier of CPS,(ProjectiveLines CPS) holds

( b_{2} = Proj_Inc CPS iff for x, y being object holds

( [x,y] in b_{2} iff ( x in the carrier of CPS & y in ProjectiveLines CPS & ex Y being set st

( y = Y & x in Y ) ) ) );

for CPS being proper CollSp

for b

( b

( [x,y] in b

( y = Y & x in Y ) ) ) );

definition

let CPS be proper CollSp;

IncProjStr(# the carrier of CPS,(ProjectiveLines CPS),(Proj_Inc CPS) #) is IncProjStr ;

end;
func IncProjSp_of CPS -> IncProjStr equals :: INCPROJ:def 3

IncProjStr(# the carrier of CPS,(ProjectiveLines CPS),(Proj_Inc CPS) #);

coherence IncProjStr(# the carrier of CPS,(ProjectiveLines CPS),(Proj_Inc CPS) #);

IncProjStr(# the carrier of CPS,(ProjectiveLines CPS),(Proj_Inc CPS) #) is IncProjStr ;

:: deftheorem defines IncProjSp_of INCPROJ:def 3 :

for CPS being proper CollSp holds IncProjSp_of CPS = IncProjStr(# the carrier of CPS,(ProjectiveLines CPS),(Proj_Inc CPS) #);

for CPS being proper CollSp holds IncProjSp_of CPS = IncProjStr(# the carrier of CPS,(ProjectiveLines CPS),(Proj_Inc CPS) #);

theorem :: INCPROJ:2

for CPS being proper CollSp holds

( the Points of (IncProjSp_of CPS) = the carrier of CPS & the Lines of (IncProjSp_of CPS) = ProjectiveLines CPS & the Inc of (IncProjSp_of CPS) = Proj_Inc CPS ) ;

( the Points of (IncProjSp_of CPS) = the carrier of CPS & the Lines of (IncProjSp_of CPS) = ProjectiveLines CPS & the Inc of (IncProjSp_of CPS) = Proj_Inc CPS ) ;

theorem :: INCPROJ:3

theorem :: INCPROJ:4

theorem Th5: :: INCPROJ:5

for CPS being proper CollSp

for p being POINT of (IncProjSp_of CPS)

for P being LINE of (IncProjSp_of CPS)

for p9 being Point of CPS

for P9 being LINE of CPS st p = p9 & P = P9 holds

( p on P iff p9 in P9 )

for p being POINT of (IncProjSp_of CPS)

for P being LINE of (IncProjSp_of CPS)

for p9 being Point of CPS

for P9 being LINE of CPS st p = p9 & P = P9 holds

( p on P iff p9 in P9 )

proof end;

theorem Th8: :: INCPROJ:8

for CPS being proper CollSp

for p, q being POINT of (IncProjSp_of CPS)

for P, Q being LINE of (IncProjSp_of CPS) st p on P & q on P & p on Q & q on Q & not p = q holds

P = Q

for p, q being POINT of (IncProjSp_of CPS)

for P, Q being LINE of (IncProjSp_of CPS) st p on P & q on P & p on Q & q on Q & not p = q holds

P = Q

proof end;

theorem Th9: :: INCPROJ:9

for CPS being proper CollSp

for p, q being POINT of (IncProjSp_of CPS) ex P being LINE of (IncProjSp_of CPS) st

( p on P & q on P )

for p, q being POINT of (IncProjSp_of CPS) ex P being LINE of (IncProjSp_of CPS) st

( p on P & q on P )

proof end;

theorem Th10: :: INCPROJ:10

for CPS being proper CollSp

for a, b, c being POINT of (IncProjSp_of CPS)

for a9, b9, c9 being Point of CPS st a = a9 & b = b9 & c = c9 holds

( a9,b9,c9 are_collinear iff ex P being LINE of (IncProjSp_of CPS) st

( a on P & b on P & c on P ) )

for a, b, c being POINT of (IncProjSp_of CPS)

for a9, b9, c9 being Point of CPS st a = a9 & b = b9 & c = c9 holds

( a9,b9,c9 are_collinear iff ex P being LINE of (IncProjSp_of CPS) st

( a on P & b on P & c on P ) )

proof end;

theorem Th11: :: INCPROJ:11

for CPS being proper CollSp holds

not for p being POINT of (IncProjSp_of CPS)

for P being LINE of (IncProjSp_of CPS) holds p on P

not for p being POINT of (IncProjSp_of CPS)

for P being LINE of (IncProjSp_of CPS) holds p on P

proof end;

theorem Th12: :: INCPROJ:12

for CPS being CollProjectiveSpace

for P being LINE of (IncProjSp_of CPS) ex a, b, c being POINT of (IncProjSp_of CPS) st

( a <> b & b <> c & c <> a & a on P & b on P & c on P )

for P being LINE of (IncProjSp_of CPS) ex a, b, c being POINT of (IncProjSp_of CPS) st

( a <> b & b <> c & c <> a & a on P & b on P & c on P )

proof end;

theorem Th13: :: INCPROJ:13

for CPS being CollProjectiveSpace

for a, b, c, d, p being POINT of (IncProjSp_of CPS)

for P, Q, M, N being LINE of (IncProjSp_of CPS) 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 (IncProjSp_of CPS) st

( q on P & q on Q )

for a, b, c, d, p being POINT of (IncProjSp_of CPS)

for P, Q, M, N being LINE of (IncProjSp_of CPS) 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 (IncProjSp_of CPS) st

( q on P & q on Q )

proof end;

theorem Th14: :: INCPROJ:14

for CPS being CollProjectiveSpace st ( for a9, b9, c9, d9 being Point of CPS ex p9 being Point of CPS st

( a9,b9,p9 are_collinear & c9,d9,p9 are_collinear ) ) holds

for M, N being LINE of (IncProjSp_of CPS) ex q being POINT of (IncProjSp_of CPS) st

( q on M & q on N )

( a9,b9,p9 are_collinear & c9,d9,p9 are_collinear ) ) holds

for M, N being LINE of (IncProjSp_of CPS) ex q being POINT of (IncProjSp_of CPS) st

( q on M & q on N )

proof end;

theorem Th15: :: INCPROJ:15

for CPS being CollProjectiveSpace st ex p, p1, r, r1 being Point of CPS st

for s being Point of CPS holds

( not p,p1,s are_collinear or not r,r1,s are_collinear ) holds

ex M, N being LINE of (IncProjSp_of CPS) st

for q being POINT of (IncProjSp_of CPS) holds

( not q on M or not q on N )

for s being Point of CPS holds

( not p,p1,s are_collinear or not r,r1,s are_collinear ) holds

ex M, N being LINE of (IncProjSp_of CPS) st

for q being POINT of (IncProjSp_of CPS) holds

( not q on M or not q on N )

proof end;

theorem Th16: :: INCPROJ:16

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 are_collinear & p1,q1,r1 are_collinear & r2,r,r1 are_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 )

( p,q,r are_collinear & p1,q1,r1 are_collinear & r2,r,r1 are_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 )

proof end;

theorem Th17: :: INCPROJ:17

for CPS being CollProjectiveSpace st ( for p1, r2, q, r1, q1, p, r being Point of CPS st p1,r2,q are_collinear & r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p are_collinear & p1,q1,r are_collinear & r2,r1,r are_collinear & p,q,r are_collinear & not p1,r2,q1 are_collinear & not p1,r2,r1 are_collinear & not p1,r1,q1 are_collinear holds

r2,r1,q1 are_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

r2,r1,q1 are_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

proof end;

theorem Th18: :: INCPROJ:18

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 are_collinear & not o,p1,p3 are_collinear & not o,p2,p3 are_collinear & p1,p2,r3 are_collinear & q1,q2,r3 are_collinear & p2,p3,r1 are_collinear & q2,q3,r1 are_collinear & p1,p3,r2 are_collinear & q1,q3,r2 are_collinear & o,p1,q1 are_collinear & o,p2,q2 are_collinear & o,p3,q3 are_collinear holds

r1,r2,r3 are_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_distinct & 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

r1,r2,r3 are_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_distinct & 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

proof end;

theorem Th19: :: INCPROJ:19

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 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear holds

r1,r2,r3 are_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_distinct & o,b1,b2,b3 are_mutually_distinct & 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

r1,r2,r3 are_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_distinct & o,b1,b2,b3 are_mutually_distinct & 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

proof end;

definition

let S be IncProjStr ;

( S is linear iff for p, q being POINT of S ex P being LINE of S st

( p on P & q on P ) )

end;
attr S is partial means :: INCPROJ:def 4

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 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;

redefine attr S is linear means :: INCPROJ:def 5

for p, q being POINT of S ex P being LINE of S st

( p on P & q on P );

compatibility for p, q being POINT of S ex P being LINE of S st

( p on P & q on P );

( S is linear iff for p, q being POINT of S ex P being LINE of S st

( p on P & q on P ) )

proof end;

:: deftheorem defines partial INCPROJ:def 4 :

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 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 );

:: deftheorem defines linear INCPROJ:def 5 :

for S being IncProjStr holds

( S is linear iff for p, q being POINT of S ex P being LINE of S st

( p on P & q on P ) );

for S being IncProjStr holds

( S is linear iff for p, q being POINT of S ex P being LINE of S st

( p on P & q on P ) );

definition

let S be IncProjStr ;

end;
attr S is up-2-dimensional means :: INCPROJ:def 6

not for p being POINT of S

for P being LINE of S holds p on P;

not for p being POINT of S

for P being LINE of S holds p on P;

:: deftheorem defines up-2-dimensional INCPROJ:def 6 :

for S being IncProjStr holds

( S is up-2-dimensional iff not for p being POINT of S

for P being LINE of S holds p on P );

for S being IncProjStr holds

( S is up-2-dimensional iff not for p being POINT of S

for P being LINE of S holds p on P );

:: deftheorem defines up-3-rank INCPROJ:def 7 :

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 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 ) );

:: deftheorem defines Vebleian INCPROJ:def 8 :

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 ) );

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 ) );

registration

let CPS be CollProjectiveSpace;

coherence

( IncProjSp_of CPS is partial & IncProjSp_of CPS is linear & IncProjSp_of CPS is up-2-dimensional & IncProjSp_of CPS is up-3-rank & IncProjSp_of CPS is Vebleian ) by Th13, Th11, Th12, Th8, Th9;

end;
coherence

( IncProjSp_of CPS is partial & IncProjSp_of CPS is linear & IncProjSp_of CPS is up-2-dimensional & IncProjSp_of CPS is up-3-rank & IncProjSp_of CPS is Vebleian ) by Th13, Th11, Th12, Th8, Th9;

registration

existence

ex b_{1} being IncProjStr st

( b_{1} is strict & b_{1} is partial & b_{1} is linear & b_{1} is up-2-dimensional & b_{1} is up-3-rank & b_{1} is Vebleian )

end;
ex b

( b

proof end;

registration

let CPS be CollProjectiveSpace;

coherence

( IncProjSp_of CPS is partial & IncProjSp_of CPS is linear & IncProjSp_of CPS is up-2-dimensional & IncProjSp_of CPS is up-3-rank & IncProjSp_of CPS is Vebleian ) ;

end;
coherence

( IncProjSp_of CPS is partial & IncProjSp_of CPS is linear & IncProjSp_of CPS is up-2-dimensional & IncProjSp_of CPS is up-3-rank & IncProjSp_of CPS is Vebleian ) ;

definition

let IT be IncProjSp;

end;
attr IT is 2-dimensional means :: INCPROJ:def 9

for M, N being LINE of IT ex q being POINT of IT st

( q on M & q on N );

for M, N being LINE of IT ex q being POINT of IT st

( q on M & q on N );

:: deftheorem defines 2-dimensional INCPROJ:def 9 :

for IT being IncProjSp holds

( IT is 2-dimensional iff for M, N being LINE of IT ex q being POINT of IT st

( q on M & q on N ) );

for IT being IncProjSp holds

( IT is 2-dimensional iff for M, N being LINE of IT ex q being POINT of IT st

( q on M & q on N ) );

:: deftheorem defines at_most-3-dimensional INCPROJ:def 10 :

for IT being IncProjStr holds

( IT is at_most-3-dimensional iff for a being POINT of IT

for M, N being LINE of IT ex b, c being POINT of IT ex S being LINE of IT st

( a on S & b on S & c on S & b on M & c on N ) );

for IT being IncProjStr holds

( IT is at_most-3-dimensional iff for a being POINT of IT

for M, N being LINE of IT ex b, c being POINT of IT ex S being LINE of IT st

( a on S & b on S & c on S & b on M & c on N ) );

definition

let IT be IncProjSp;

end;
attr IT is 3-dimensional means :: INCPROJ:def 11

( IT is at_most-3-dimensional & IT is up-3-dimensional );

( IT is at_most-3-dimensional & IT is up-3-dimensional );

:: deftheorem defines 3-dimensional INCPROJ:def 11 :

for IT being IncProjSp holds

( IT is 3-dimensional iff ( IT is at_most-3-dimensional & IT is up-3-dimensional ) );

for IT being IncProjSp holds

( IT is 3-dimensional iff ( IT is at_most-3-dimensional & IT is up-3-dimensional ) );

definition

let IT be IncProjStr ;

end;
attr IT is Fanoian means :: INCPROJ:def 12

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 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;

:: deftheorem 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 );

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 ;

end;
attr IT is Desarguesian means :: INCPROJ:def 13

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_distinct & 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;

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_distinct & 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;

:: deftheorem 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_distinct & 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 );

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_distinct & 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 ;

end;
attr IT is Pappian means :: INCPROJ:def 14

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_distinct & o,b1,b2,b3 are_mutually_distinct & 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;

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_distinct & o,b1,b2,b3 are_mutually_distinct & 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;

:: deftheorem 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_distinct & o,b1,b2,b3 are_mutually_distinct & 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 );

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_distinct & o,b1,b2,b3 are_mutually_distinct & 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 );

registration

ex b_{1} being IncProjSp st

( b_{1} is Desarguesian & b_{1} is Fanoian & b_{1} is at_most-3-dimensional & b_{1} is up-3-dimensional )
end;

cluster linear partial up-2-dimensional up-3-rank Vebleian up-3-dimensional at_most-3-dimensional Fanoian Desarguesian for IncProjStr ;

existence ex b

( b

proof end;

registration

ex b_{1} being IncProjSp st

( b_{1} is Pappian & b_{1} is Fanoian & b_{1} is at_most-3-dimensional & b_{1} is up-3-dimensional )
end;

cluster linear partial up-2-dimensional up-3-rank Vebleian up-3-dimensional at_most-3-dimensional Fanoian Pappian for IncProjStr ;

existence ex b

( b

proof end;

registration

ex b_{1} being IncProjSp st

( b_{1} is Desarguesian & b_{1} is Fanoian & b_{1} is 2-dimensional )
end;

cluster linear partial up-2-dimensional up-3-rank Vebleian 2-dimensional Fanoian Desarguesian for IncProjStr ;

existence ex b

( b

proof end;

registration

ex b_{1} being IncProjSp st

( b_{1} is Pappian & b_{1} is Fanoian & b_{1} is 2-dimensional )
end;

cluster linear partial up-2-dimensional up-3-rank Vebleian 2-dimensional Fanoian Pappian for IncProjStr ;

existence ex b

( b

proof end;