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 consider L0 being Subset of (REAL n) such that
A1: ( L = L0 & ex x1, x2 being Element of REAL n st L0 = Line x1,x2 ) ;
consider x1, x2 being Element of REAL n such that
A2: L = Line x1,x2 by A1;
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 A2; :: thesis: verum