consider a being Element of AS;
consider b being Element of AS such that
A1: a <> b by Th10;
take Line (a,b) ; :: thesis: Line (a,b) is being_line
thus Line (a,b) is being_line by A1, Def3; :: thesis: verum