let n be Element of 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 ex L0 being Subset of (REAL n) st
( L = L0 & ex x1, x2 being Element of REAL n st L0 = Line x1,x2 ) ;
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