:: deftheorem defines # ANPROJ11:def 27 :
for l being Element of ProjectiveLines real_projective_plane holds # l = l;