:: deftheorem defines # ANPROJ11:def 23 :
for P being Point of real_projective_plane holds # P = P;