:: deftheorem defines on PROJPL_1:def 2 :
for G being IncProjStr
for a being POINT of G
for P, Q being LINE of G holds
( a on P,Q iff ( a on P & a on Q ) );