let n be Nat; :: thesis: for L being Element of line_of_REAL n ex x being Element of REAL n st x in L
let L be Element of line_of_REAL n; :: thesis: ex x being Element of REAL n st x in L
consider x1, x2 being Element of REAL n such that
A1: L = Line (x1,x2) by Th51;
take x1 ; :: thesis: x1 in L
thus x1 in L by A1, EUCLID_4:9; :: thesis: verum