:: deftheorem defines # ANPROJ11:def 28 :
for l being LINE of (IncProjSp_of real_projective_plane) holds # l = l;