set a = the Element of AS;
consider b being Element of AS such that
A1: the Element of AS <> b by SUBSET_1:50;
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; :: thesis: verum