theorem :: AFPROJ:7

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