theorem Th23: :: AFPROJ:23

for AS being AffinSpace
for x being set holds
( x is LINE of (IncProjSp_of AS) iff ex X being Subset of AS st
( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) )