:: deftheorem Def12 defines Inc_of_Dir AFPROJ:def 12 :
for AS being AffinSpace
for b₂ being Relation of (Dir_of_Lines AS),(Dir_of_Planes AS) holds
( b₂ = Inc_of_Dir AS iff for x, y being object holds
( [x,y] in b₂ iff ex A, X being Subset of AS st
( x = LDir A & y = PDir X & A is being_line & X is being_plane & A '||' X ) ) );