:: deftheorem defines AfLines AFPROJ:def 1 :
for AS being AffinSpace holds AfLines AS = { A where A is Subset of AS : A is being_line } ;