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