theorem Th20: :: AFPROJ:20

for AS being AffinSpace
for x being set holds
( x is POINT of (IncProjSp_of AS) iff ( x is Element of AS or ex X being Subset of AS st
( x = LDir X & X is being_line ) ) )