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