:: PROJPL_1 semantic presentation

begin

notation
let G be ( ( ) ( ) IncProjStr ) ;
let a be ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ;
let P be ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;
antonym a |' P for a on P;
end;

definition
let G be ( ( ) ( ) IncProjStr ) ;
let a, b be ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ;
let P be ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;
pred a,b |' P means :: PROJPL_1:def 1
( a : ( ( V4() ) ( V4() ) set ) |' P : ( ( ) ( ) Element of bool [:G : ( ( ) ( ) IncStruct ) ,a : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) & b : ( ( V4() ) ( V4() ) set ) |' P : ( ( ) ( ) Element of bool [:G : ( ( ) ( ) IncStruct ) ,a : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) );
end;

definition
let G be ( ( ) ( ) IncProjStr ) ;
let a be ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ;
let P, Q be ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;
pred a on P,Q means :: PROJPL_1:def 2
( a : ( ( V4() ) ( V4() ) set ) on P : ( ( V4() ) ( V4() ) set ) & a : ( ( V4() ) ( V4() ) set ) on Q : ( ( ) ( ) Element of bool [:G : ( ( ) ( ) IncStruct ) ,a : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) );
end;

definition
let G be ( ( ) ( ) IncProjStr ) ;
let a be ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ;
let P, Q, R be ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;
pred a on P,Q,R means :: PROJPL_1:def 3
( a : ( ( V4() ) ( V4() ) set ) on P : ( ( V4() ) ( V4() ) set ) & a : ( ( V4() ) ( V4() ) set ) on Q : ( ( ) ( ) Element of bool [:G : ( ( ) ( ) IncStruct ) ,a : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) & a : ( ( V4() ) ( V4() ) set ) on R : ( ( ) ( ) Element of bool [:G : ( ( ) ( ) IncStruct ) ,P : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) );
end;

theorem :: PROJPL_1:1
for G being ( ( ) ( ) IncProjStr )
for a, b, c being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for P, Q, R being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
( ( {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( V4() ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) implies {b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( V4() ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) & ( {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 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) implies ( {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 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on P : ( ( ) ( ) 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 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on P : ( ( ) ( ) 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 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on P : ( ( ) ( ) 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 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on P : ( ( ) ( ) 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 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ) & ( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) implies a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) & ( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) implies ( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ) ) ;

definition
let IT be ( ( ) ( ) IncProjStr ) ;
attr IT is configuration means :: PROJPL_1:def 4
 for p, q being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for P, Q being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) = q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) holds
P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) = Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;
end;

theorem :: PROJPL_1:2
for G being ( ( ) ( ) IncProjStr ) holds
( G : ( ( ) ( ) IncProjStr ) is configuration iff for p, q being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for P, Q being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st {p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( V4() ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( V4() ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) = q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) holds
P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) = Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ;

theorem :: PROJPL_1:3
for G being ( ( ) ( ) IncProjStr ) holds
( G : ( ( ) ( ) IncProjStr ) is configuration iff for p, q being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for P, Q being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & not p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) = q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) holds
P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) = Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ;

theorem :: PROJPL_1:4
for G being ( ( ) ( ) IncProjStr ) holds
( G : ( ( ) ( ) IncProjStr ) is ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp) iff ( G : ( ( ) ( ) IncProjStr ) is configuration & ( for p, q being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ex P being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st {p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( V4() ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on P : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ) & ex p being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ex P being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) |' P : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & ( for P being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ex a, b, c being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st
( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) are_mutually_different & {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 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on P : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ) ) & ( for a, b, c, d, p being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for M, N, P, Q being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on M : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on N : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( V4() ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( V4() ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) |' P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) |' Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & M : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> N : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
ex q being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ) ) ;

definition
mode IncProjectivePlane is ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) IncProjSp) ;
end;

definition
let G be ( ( ) ( ) IncProjStr ) ;
let a, b, c be ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ;
pred a,b,c is_collinear means :: PROJPL_1:def 5
 ex P being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st {a : ( ( V4() ) ( V4() ) set ) ,b : ( ( V4() ) ( V4() ) set ) ,c : ( ( ) ( ) Element of bool [:G : ( ( ) ( ) IncStruct ) ,a : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( ) Element of bool the Points of G : ( ( ) ( ) IncStruct ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;
end;

notation
let G be ( ( ) ( ) IncProjStr ) ;
let a, b, c be ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ;
antonym a,b,c is_a_triangle for a,b,c is_collinear ;
end;

theorem :: PROJPL_1:5
for G being ( ( ) ( ) IncProjStr )
for a, b, c being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) holds
( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_collinear iff ex P being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st
( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ) ;

theorem :: PROJPL_1:6
for G being ( ( ) ( ) IncProjStr )
for a, b, c being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) holds
( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_triangle iff for P being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) |' P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) or b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) |' P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) or c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) |' P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ) ;

definition
let G be ( ( ) ( ) IncProjStr ) ;
let a, b, c, d be ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ;
pred a,b,c,d is_a_quadrangle means :: PROJPL_1:def 6
( a : ( ( V4() ) ( V4() ) set ) ,b : ( ( V4() ) ( V4() ) set ) ,c : ( ( ) ( ) Element of bool [:G : ( ( ) ( ) IncStruct ) ,a : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is_a_triangle & b : ( ( V4() ) ( V4() ) set ) ,c : ( ( ) ( ) Element of bool [:G : ( ( ) ( ) IncStruct ) ,a : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of bool [:G : ( ( ) ( ) IncStruct ) ,b : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is_a_triangle & c : ( ( ) ( ) Element of bool [:G : ( ( ) ( ) IncStruct ) ,a : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,d : ( ( ) ( ) Element of bool [:G : ( ( ) ( ) IncStruct ) ,b : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,a : ( ( V4() ) ( V4() ) set ) is_a_triangle & d : ( ( ) ( ) Element of bool [:G : ( ( ) ( ) IncStruct ) ,b : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,a : ( ( V4() ) ( V4() ) set ) ,b : ( ( V4() ) ( V4() ) set ) is_a_triangle );
end;

theorem :: PROJPL_1:7
for G being ( ( ) ( ) IncProjStr ) st G : ( ( ) ( ) IncProjStr ) is ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp) holds
ex A, B being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;

theorem :: PROJPL_1:8
for G being ( ( ) ( ) IncProjStr )
for a being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st G : ( ( ) ( ) IncProjStr ) is ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp) holds
ex b, c being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st
( {b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( V4() ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) 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 ) ) are_mutually_different ) ;

theorem :: PROJPL_1:9
for G being ( ( ) ( ) IncProjStr )
for a being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A, B being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st G : ( ( ) ( ) IncProjStr ) is ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp) & A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
ex b being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st
( b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) |' B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ) ;

theorem :: PROJPL_1:10
for G being ( ( ) ( ) IncProjStr )
for a1, a2, b being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st G : ( ( ) ( ) IncProjStr ) is configuration & {a1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( V4() ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> a2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) |' A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
a1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_triangle ;

theorem :: PROJPL_1:11
for G being ( ( ) ( ) IncProjStr )
for a, b, c being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_collinear holds
( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_collinear & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_collinear & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_collinear & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_collinear & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_collinear ) ;

theorem :: PROJPL_1:12
for G being ( ( ) ( ) IncProjStr )
for a, b, c being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_triangle holds
( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_triangle & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_triangle & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_triangle & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_triangle & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_triangle ) ;

theorem :: PROJPL_1:13
for G being ( ( ) ( ) IncProjStr )
for a, b, c, d being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle holds
( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle ) ;

theorem :: PROJPL_1:14
for G being ( ( ) ( ) IncProjStr )
for a1, a2, b1, b2 being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A, B being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st G : ( ( ) ( ) IncProjStr ) is configuration & {a1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( V4() ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {b1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( V4() ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) |' B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & b1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) |' A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> a2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & b1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> b2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) holds
a1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,a2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle ;

theorem :: PROJPL_1:15
for G being ( ( ) ( ) IncProjStr ) st G : ( ( ) ( ) IncProjStr ) is ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp) holds
ex a, b, c, d being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle ;

definition
let G be ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp) ;
mode Quadrangle of G -> ( ( ) ( ) Element of [: the Points of G : ( ( ) ( ) IncStruct ) : ( ( V4() ) ( V4() ) set ) , the Points of G : ( ( ) ( ) IncStruct ) : ( ( V4() ) ( V4() ) set ) , the Points of G : ( ( ) ( ) IncStruct ) : ( ( V4() ) ( V4() ) set ) , the Points of G : ( ( ) ( ) IncStruct ) : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) ) means :: PROJPL_1:def 7
it : ( ( V4() ) ( V4() ) set ) `1_4 : ( ( ) ( ) Element of the Points of G : ( ( ) ( ) IncStruct ) : ( ( V4() ) ( V4() ) set ) ) ,it : ( ( V4() ) ( V4() ) set ) `2_4 : ( ( ) ( ) Element of the Points of G : ( ( ) ( ) IncStruct ) : ( ( V4() ) ( V4() ) set ) ) ,it : ( ( V4() ) ( V4() ) set ) `3_4 : ( ( ) ( ) Element of the Points of G : ( ( ) ( ) IncStruct ) : ( ( V4() ) ( V4() ) set ) ) ,it : ( ( V4() ) ( V4() ) set ) `4_4 : ( ( ) ( ) Element of the Points of G : ( ( ) ( ) IncStruct ) : ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle ;
end;

definition
let G be ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp) ;
let a, b be ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ;
assume a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ;
func a * b -> ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) means :: PROJPL_1:def 8
{a : ( ( V4() ) ( V4() ) set ) ,b : ( ( V4() ) ( V4() ) set ) } : ( ( ) ( V4() ) Element of bool the Points of G : ( ( ) ( ) IncStruct ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on it : ( ( ) ( ) Element of bool [:G : ( ( ) ( ) IncStruct ) ,a : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: PROJPL_1:16
for G being ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp)
for a, b being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for L being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) holds
( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) = b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & ( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) implies L : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) = a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ) ;

begin

theorem :: PROJPL_1:17
for G being ( ( ) ( ) IncProjStr ) st ex a, b, c being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) is_a_triangle & ( for p, q being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ex M being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st {p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( V4() ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on M : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) holds
ex p being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ex P being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) |' P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;

theorem :: PROJPL_1:18
for G being ( ( ) ( ) IncProjStr ) st ex a, b, c, d being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle holds
ex a, b, c being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_triangle ;

theorem :: PROJPL_1:19
for G being ( ( ) ( ) IncProjStr )
for a, b, c being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for P, Q 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 ) ) is_a_triangle & {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( V4() ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( V4() ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;

theorem :: PROJPL_1:20
for G being ( ( ) ( ) IncProjStr )
for a, b, c, d being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for P, Q, R 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 ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle & {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( V4() ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( V4() ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & {a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( V4() ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_mutually_different ;

theorem :: PROJPL_1:21
for G being ( ( ) ( ) IncProjStr )
for a, p, q, r being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for P, Q, R, A being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st G : ( ( ) ( ) IncProjStr ) is configuration & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) are_mutually_different & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) |' A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,Q : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,R : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) are_mutually_different ;

theorem :: PROJPL_1:22
for G being ( ( ) ( ) IncProjStr ) st G : ( ( ) ( ) IncProjStr ) is configuration & ( for p, q being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ex M being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st {p : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( V4() ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on M : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ) & ( for P, Q being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ex a being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,Q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ) & ex a, b, c, d being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st a : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle holds
for P being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ex a, b, c being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st
( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) are_mutually_different & {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 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on P : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ;

theorem :: PROJPL_1:23
for G being ( ( ) ( ) IncProjStr ) holds
( G : ( ( ) ( ) IncProjStr ) is ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) IncProjectivePlane) iff ( G : ( ( ) ( ) IncProjStr ) is configuration & ( for p, q being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ex M being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st {p : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) } : ( ( ) ( V4() ) Element of bool the Points of b1 : ( ( ) ( ) IncProjStr ) : ( ( V4() ) ( V4() ) set ) : ( ( ) ( ) set ) ) on M : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ) & ( for P, Q being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ex a being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on P : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,Q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ) & ex a, b, c, d being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle ) ) ;

definition
let G be ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) IncProjectivePlane) ;
let A, B be ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;
assume A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;
func A * B -> ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) means :: PROJPL_1:def 9
it : ( ( ) ( ) Element of bool [:G : ( ( ) ( ) IncStruct ) ,A : ( ( V4() ) ( V4() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) on A : ( ( V4() ) ( V4() ) set ) ,B : ( ( V4() ) ( V4() ) set ) ;
end;

theorem :: PROJPL_1:24
for G being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) IncProjectivePlane)
for a being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A, B being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
( A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) * B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) * B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) * B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) = B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) * A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & ( a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) implies a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) = A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) * B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ) ) ;

theorem :: PROJPL_1:25
for G being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) IncProjectivePlane)
for a, q being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for A, B being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) |' A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) * B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) holds
( (q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) * B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & (q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) * B : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) |' A : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ;

begin

theorem :: PROJPL_1:26
for G 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 ) ) st a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_triangle holds
a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) are_mutually_different ;

theorem :: PROJPL_1:27
for G being ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp)
for a, b, c, d being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ,d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) is_a_quadrangle holds
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 ;

theorem :: PROJPL_1:28
for G being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) IncProjectivePlane)
for a, b, c, d being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) holds
( not a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) = b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) or a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) = c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) or b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) = d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) or c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) = d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) or a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) = c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ;

theorem :: PROJPL_1:29
for G being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) IncProjectivePlane)
for a, b, c, d being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) holds
( not a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) = b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) or a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) = c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) or b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) = d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) or c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) = d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) or a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * d : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ;

theorem :: PROJPL_1:30
for G being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) IncProjectivePlane)
for e, m, m9 being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for I being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st m : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on I : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & m9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on I : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & m : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> m9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & e : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) |' I : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
( m : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * e : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> m9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * e : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & e : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * m : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> e : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * m9 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ;

theorem :: PROJPL_1:31
for G being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) IncProjectivePlane)
for e being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for I, L1, L2 being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st e : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & e : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on L2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & L1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> L2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & e : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) |' I : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
( I : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) * L1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> I : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) * L2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & L1 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) * I : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> L2 : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) * I : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ) ;

theorem :: PROJPL_1:32
for G being ( ( V22() partial up-2-dimensional up-3-rank V73() ) ( V22() partial up-2-dimensional up-3-rank V73() ) IncProjSp)
for a, b, q, q1 being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * q1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & q : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & q1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) holds
q1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;

theorem :: PROJPL_1:33
for G 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 ) ) st c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) holds
b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;

theorem :: PROJPL_1:34
for G being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) IncProjectivePlane)
for q1, q2, r1, r2 being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for H being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st r1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> r2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & r1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on H : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & r2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on H : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & q1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) |' H : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & q2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) |' H : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
q1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * r1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) <> q2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * r2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ;

theorem :: PROJPL_1:35
for G being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) IncProjectivePlane)
for a, b, c being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) holds
( not a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) or a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) = c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) or b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) = c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) or b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ;

theorem :: PROJPL_1:36
for G being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) IncProjectivePlane)
for a, b, c being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) holds
( not a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) or b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) = a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) or b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) = c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) or c : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on b : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * a : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) ) ;

theorem :: PROJPL_1:37
for G being ( ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) ( V22() partial up-2-dimensional up-3-rank V73() 2-dimensional ) IncProjectivePlane)
for e, x1, x2, p1, p2 being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) )
for H, I being ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) st x1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on I : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & x2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on I : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & e : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) |' I : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & x1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> x2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & p1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> e : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & p2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> e : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) & p1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on e : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * x1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & p2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on e : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * x2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) holds
ex r being ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) st
( r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on p1 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) * p2 : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) on H : ( ( ) ( ) LINE of ( ( V4() ) ( V4() ) set ) ) & r : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) <> e : ( ( ) ( ) POINT of ( ( V4() ) ( V4() ) set ) ) ) ;