begin
theorem
for
IPP being ( (
V22()
partial up-2-dimensional up-3-rank V73() ) (
V22()
partial up-2-dimensional up-3-rank V73() )
IncProjSp)
for
a,
b,
c being ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
for
A being ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) st
{a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73() ) (
V22()
partial up-2-dimensional up-3-rank V73() )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on A : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) holds
(
{a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73() ) (
V22()
partial up-2-dimensional up-3-rank V73() )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on A : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
{b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73() ) (
V22()
partial up-2-dimensional up-3-rank V73() )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on A : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
{b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73() ) (
V22()
partial up-2-dimensional up-3-rank V73() )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on A : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
{c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73() ) (
V22()
partial up-2-dimensional up-3-rank V73() )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on A : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
{c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73() ) (
V22()
partial up-2-dimensional up-3-rank V73() )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on A : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) ) ;
theorem
for
IPP being ( (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian )
IncProjSp)
for
o,
b1,
a1,
b2,
a2,
b3,
a3,
r,
s,
t being ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
for
C1,
C2,
C3,
A1,
A2,
A3,
B1,
B2,
B3 being ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) st
{o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on C1 : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
{o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on C2 : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
{o : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a3 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b3 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on C3 : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
{a3 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,t : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on A1 : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
{a3 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on A2 : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
{a2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,s : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on A3 : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
{t : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b3 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on B1 : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
{b1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b3 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on B2 : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
{b1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,s : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on B3 : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
C1 : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) ,
C2 : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) ,
C3 : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) )
are_mutually_different &
o : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
<> a3 : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) &
o : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
<> b1 : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) &
o : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
<> b2 : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) &
a2 : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
<> b2 : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) holds
ex
O being ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) st
{r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,s : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,t : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on O : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) ;
theorem
for
IPP being ( (
V22()
partial up-2-dimensional up-3-rank V73() ) (
V22()
partial up-2-dimensional up-3-rank V73() )
IncProjSp) st ex
A being ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) ex
a,
b,
c,
d being ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) st
(
a : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on A : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
b : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on A : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
c : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on A : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
d : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on A : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
a : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) ,
b : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) ,
c : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) ,
d : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
are_mutually_different ) holds
for
B being ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) ex
p,
q,
r,
s being ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) st
(
p : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on B : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
q : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on B : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
r : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on B : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
s : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on B : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
p : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) ,
q : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) ,
r : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) ,
s : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
are_mutually_different ) ;
theorem
for
IPP being ( (
V22()
partial up-2-dimensional up-3-rank V73()
Fanoian ) (
V22()
partial up-2-dimensional up-3-rank V73()
Fanoian )
IncProjSp) ex
p,
q,
r,
s,
a,
b,
c being ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) ex
A,
B,
C,
Q,
L,
R,
S,
D being ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) st
( not
q : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on L : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) & not
r : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on L : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) & not
p : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on Q : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) & not
s : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on Q : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) & not
p : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on R : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) & not
r : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on R : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) & not
q : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on S : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) & not
s : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on S : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
{a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,s : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
Fanoian ) (
V22()
partial up-2-dimensional up-3-rank V73()
Fanoian )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on L : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
{a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
Fanoian ) (
V22()
partial up-2-dimensional up-3-rank V73()
Fanoian )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on Q : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
{b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,s : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
Fanoian ) (
V22()
partial up-2-dimensional up-3-rank V73()
Fanoian )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on R : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
{b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
Fanoian ) (
V22()
partial up-2-dimensional up-3-rank V73()
Fanoian )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on S : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
{c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
Fanoian ) (
V22()
partial up-2-dimensional up-3-rank V73()
Fanoian )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on A : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
{c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,s : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
Fanoian ) (
V22()
partial up-2-dimensional up-3-rank V73()
Fanoian )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on B : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
{a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
Fanoian ) (
V22()
partial up-2-dimensional up-3-rank V73()
Fanoian )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) )
on C : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) & not
c : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on C : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) ) ;
theorem
for
IPP being ( (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian )
IncProjSp)
for
p,
q being ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
for
K,
L,
R being ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) st not
p : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on K : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) & not
p : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on L : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) & not
q : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on L : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) & not
q : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on R : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) holds
(
dom ((IncProj (L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) PartFunc of ,) * (IncProj (K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) PartFunc of ,) ) : ( (
Relation-like ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set )
= dom (IncProj (K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( (
Function-like ) (
Relation-like the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set )
-defined the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set )
-valued Function-like )
PartFunc of ,) : ( ( ) ( )
Element of
bool the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set ) : ( ( ) ( )
set ) ) &
rng ((IncProj (L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) PartFunc of ,) * (IncProj (K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( ( Function-like ) ( Relation-like the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -defined the Points of b1 : ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional Desarguesian ) IncProjSp) : ( ( V4() ) ( V4() ) set ) -valued Function-like ) PartFunc of ,) ) : ( (
Relation-like ) (
Relation-like Function-like )
set ) : ( ( ) ( )
set )
= rng (IncProj (L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( (
Function-like ) (
Relation-like the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set )
-defined the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set )
-valued Function-like )
PartFunc of ,) : ( ( ) ( )
set ) ) ;
theorem
for
IPP being ( (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian )
IncProjSp)
for
p being ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
for
K,
L being ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) )
for
a1,
b1,
a2,
b2 being ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) st not
p : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on K : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) & not
p : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on L : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
a1 : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on K : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
b1 : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on K : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
(IncProj (K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( (
Function-like ) (
Relation-like the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set )
-defined the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set )
-valued Function-like )
PartFunc of ,)
. a1 : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) : ( ( ) ( )
set )
= a2 : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) &
(IncProj (K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( (
Function-like ) (
Relation-like the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set )
-defined the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set )
-valued Function-like )
PartFunc of ,)
. b1 : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) : ( ( ) ( )
set )
= b2 : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) &
a2 : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
= b2 : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) holds
a1 : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
= b1 : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) ;
theorem
for
IPP being ( (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian )
IncProjSp)
for
p,
q,
c being ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
for
K,
L,
R being ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) st not
p : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on K : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) & not
p : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on L : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) & not
q : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on L : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) & not
q : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on R : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
c : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on K : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
c : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on L : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
c : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on R : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
K : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) )
<> R : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) holds
ex
o being ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) st
( not
o : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on K : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) & not
o : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) )
on R : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) &
(IncProj (L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( (
Function-like ) (
Relation-like the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set )
-defined the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set )
-valued Function-like )
PartFunc of ,)
* (IncProj (K : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) )) : ( (
Function-like ) (
Relation-like the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set )
-defined the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set )
-valued Function-like )
PartFunc of ,) : ( (
Relation-like ) (
Relation-like Function-like )
set )
= IncProj (
K : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) ,
o : ( ( ) ( )
POINT of ( (
V4() ) (
V4() )
set ) ) ,
R : ( ( ) ( )
LINE of ( (
V4() ) (
V4() )
set ) ) ) : ( (
Function-like ) (
Relation-like the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set )
-defined the
Points of
b1 : ( (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian ) (
V22()
partial up-2-dimensional up-3-rank V73()
2-dimensional Desarguesian )
IncProjSp) : ( (
V4() ) (
V4() )
set )
-valued Function-like )
PartFunc of ,) ) ;