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