theorem Th14: :: AFPROJ:14

for AS being AffinSpace
for x being set holds
( x in Dir_of_Lines AS iff ex X being Subset of AS st
( x = LDir X & X is being_line ) )