theorem Th18: :: AFPROJ:18

for AS being AffinSpace
for x being set holds
( x in [:(AfLines AS),{1}:] iff ex X being Subset of AS st
( x = [X,1] & X is being_line ) )