for AS being AffinSpace
for a, b being Element of AS st a <> b holds
a,b // Line (a,b) by Th1;