:: deftheorem defines configuration PROJPL_1:def 4 :
for IT being IncProjStr holds
( IT is configuration iff for p, q being POINT of IT
for P, Q being LINE of IT st p on P & q on P & p on Q & q on Q & not p = q holds
P = Q );