let n be Nat; :: thesis: for x1, x2 being Element of REAL n
for L being Element of line_of_REAL n st x1 in L & x2 in L holds
Line (x1,x2) c= L
let x1, x2 be Element of REAL n; :: thesis: for L being Element of line_of_REAL n st x1 in L & x2 in L holds
Line (x1,x2) c= L
let L be Element of line_of_REAL n; :: thesis: ( x1 in L & x2 in L implies Line (x1,x2) c= L )
L in line_of_REAL n ;
then ex y1, y2 being Element of REAL n st L = Line (y1,y2) ;
hence ( x1 in L & x2 in L implies Line (x1,x2) c= L ) by EUCLID_4:10; :: thesis: verum