begin
theorem
for
CPS being ( ( non
empty V116()
V117()
proper Vebleian at_least_3rank ) ( non
empty V116()
V117()
proper Vebleian at_least_3rank )
CollProjectiveSpace) st ( for
p,
p1,
q,
q1,
r2 being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ex
r,
r1 being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) st
(
p : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) ,
r : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
p1 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) ,
q1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r1 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
is_collinear &
r2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) ,
r1 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
is_collinear ) ) holds
for
a being ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
for
M,
N being ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) ex
b,
c being ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ex
S being ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) st
(
a : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on S : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
b : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on S : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
c : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on S : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
b : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on M : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
c : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on N : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) ) ;
theorem
for
CPS being ( ( non
empty V116()
V117()
proper Vebleian at_least_3rank ) ( non
empty V116()
V117()
proper Vebleian at_least_3rank )
CollProjectiveSpace) st ( for
p1,
r2,
q,
r1,
q1,
p,
r being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) st
p1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
r1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
p1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
p : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
r2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
p : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
p1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
r2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
p : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear & not
p1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear & not
p1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear & not
p1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear holds
r2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear ) holds
for
p,
q,
r,
s,
a,
b,
c being ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
for
L,
Q,
R,
S,
A,
B,
C being ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) st not
q : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on L : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) & not
r : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on L : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) & not
p : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on Q : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) & not
s : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on Q : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) & not
p : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on R : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) & not
r : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on R : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,p : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,s : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on L : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,q : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,r : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on Q : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{b : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,q : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,s : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on R : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{b : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,p : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,r : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on S : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{c : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,p : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,q : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on A : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{c : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,r : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,s : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on B : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on C : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) holds
not
c : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on C : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) ;
theorem
for
CPS being ( ( non
empty V116()
V117()
proper Vebleian at_least_3rank ) ( non
empty V116()
V117()
proper Vebleian at_least_3rank )
CollProjectiveSpace) st ( for
o,
p1,
p2,
p3,
q1,
q2,
q3,
r1,
r2,
r3 being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) st
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> q1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
p1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> q1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> q2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
p2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> q2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> q3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
p3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> q3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) & not
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
p1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
p2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear & not
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
p1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
p3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear & not
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
p2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
p3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
p1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
p2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
q1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
p2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
p3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
q2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
p1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
p3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
q1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
p1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
p2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
p3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear holds
r1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear ) holds
for
o,
b1,
a1,
b2,
a2,
b3,
a3,
r,
s,
t being ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
for
C1,
C2,
C3,
A1,
A2,
A3,
B1,
B2,
B3 being ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) st
{o : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,a1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on C1 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{o : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,a2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on C2 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{o : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,a3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on C3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,a2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,t : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on A1 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,r : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,a1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on A2 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,s : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,a1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on A3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{t : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on B1 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{b1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,r : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on B2 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{b1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,s : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on B3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
C1 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) ,
C2 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) ,
C3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) )
are_mutually_different &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> a1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> a2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> a3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> b1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> b2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> b3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
a1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> b1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
a2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> b2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
a3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> b3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) holds
ex
O being ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) st
{r : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,s : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,t : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on O : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) ;
theorem
for
CPS being ( ( non
empty V116()
V117()
proper Vebleian at_least_3rank ) ( non
empty V116()
V117()
proper Vebleian at_least_3rank )
CollProjectiveSpace) st ( for
o,
p1,
p2,
p3,
q1,
q2,
q3,
r1,
r2,
r3 being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) st
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> p2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> p3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
p2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> p3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
p1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> p2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
p1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> p3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> q2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> q3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
q2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> q3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
q1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> q2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
q1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> q3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) & not
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
p1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
p1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
p2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
p1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
p3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
p1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
q1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
p2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
p1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
p3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
p2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear &
p3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
q2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear holds
r1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
r3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
is_collinear ) holds
for
o,
a1,
a2,
a3,
b1,
b2,
b3,
c1,
c2,
c3 being ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
for
A1,
A2,
A3,
B1,
B2,
B3,
C1,
C2,
C3 being ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) st
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
a1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
a2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
a3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
are_mutually_different &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
b1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
b2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
b3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
are_mutually_different &
A3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) )
<> B3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on A3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on B3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,c1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on A1 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,c2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on B1 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,c3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on C1 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,c2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on A2 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,c1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on B2 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,c3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on C2 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{b1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on A3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,a2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,a3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on B3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{c1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,c2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
(IncProjSp_of b1 : ( ( non empty V116() V117() proper Vebleian at_least_3rank ) ( non empty V116() V117() proper Vebleian at_least_3rank ) CollProjectiveSpace) ) : ( ( ) (
strict )
IncProjStr ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on C3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) holds
c3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on C3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) ;
definition
let IT be ( ( ) ( )
IncProjStr ) ;
attr IT is
Fanoian means
for
p,
q,
r,
s,
a,
b,
c being ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
for
L,
Q,
R,
S,
A,
B,
C being ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) st not
q : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on L : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) & not
r : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on L : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) & not
p : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on Q : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) & not
s : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on Q : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) & not
p : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on R : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) & not
r : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on R : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) & not
q : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on S : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) & not
s : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on S : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,p : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,s : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on L : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,q : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,r : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on Q : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{b : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,q : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,s : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on R : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{b : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,p : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,r : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on S : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{c : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,p : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,q : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on A : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{c : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,r : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,s : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on B : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on C : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) holds
not
c : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on C : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) ;
end;
definition
let IT be ( ( ) ( )
IncProjStr ) ;
attr IT is
Desarguesian means
for
o,
b1,
a1,
b2,
a2,
b3,
a3,
r,
s,
t being ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
for
C1,
C2,
C3,
A1,
A2,
A3,
B1,
B2,
B3 being ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) st
{o : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,a1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on C1 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{o : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,a2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on C2 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{o : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,a3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on C3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,a2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,t : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on A1 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,r : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,a1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on A2 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,s : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,a1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on A3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{t : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on B1 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{b1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,r : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on B2 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{b1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,s : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on B3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
C1 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) ,
C2 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) ,
C3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) )
are_mutually_different &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> a1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> a2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> a3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> b1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> b2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> b3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
a1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> b1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
a2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> b2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) &
a3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
<> b3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) holds
ex
O being ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) st
{r : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,s : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,t : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on O : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) ;
end;
definition
let IT be ( ( ) ( )
IncProjStr ) ;
attr IT is
Pappian means
for
o,
a1,
a2,
a3,
b1,
b2,
b3,
c1,
c2,
c3 being ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
for
A1,
A2,
A3,
B1,
B2,
B3,
C1,
C2,
C3 being ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) st
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
a1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
a2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
a3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
are_mutually_different &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
b1 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
b2 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) ) ,
b3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
are_mutually_different &
A3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) )
<> B3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on A3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
o : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on B3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,c1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on A1 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,c2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on B1 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,c3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on C1 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,c2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on A2 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,c1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on B2 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,c3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on C2 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{b1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on A3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{a1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,a2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,a3 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on B3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) &
{c1 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) ,c2 : ( ( ) ( ) POINT of ( ( non empty ) ( non empty ) set ) ) } : ( ( ) ( )
Element of
bool the
Points of
IT : ( (
V49() ) (
V49() )
set ) : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( )
set ) )
on C3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) holds
c3 : ( ( ) ( )
POINT of ( ( non
empty ) ( non
empty )
set ) )
on C3 : ( ( ) ( )
LINE of ( ( non
empty ) ( non
empty )
set ) ) ;
end;