:: deftheorem Def11 defines Proj_Inc AFPROJ:def 11 :
for AS being AffinSpace
for b₂ being Relation of (ProjectivePoints AS),(ProjectiveLines AS) holds
( b₂ = Proj_Inc AS iff for x, y being object holds
( [x,y] in b₂ iff ( ex K being Subset of AS st
( K is being_line & y = [K,1] & ( ( x in the carrier of AS & x in K ) or x = LDir K ) ) or ex K, X being Subset of AS st
( K is being_line & X is being_plane & x = LDir K & y = [(PDir X),2] & K '||' X ) ) ) );