let V be RealLinearSpace; :: thesis: for L being line of V
for x1, x2 being Element of V st x1 <> x2 & x1 in L & x2 in L holds
L = Line (x1,x2)
let L be line of V; :: thesis: for x1, x2 being Element of V st x1 <> x2 & x1 in L & x2 in L holds
L = Line (x1,x2)
ex x3, x4 being Element of V st L = Line (x3,x4) by Def15;
hence for x1, x2 being Element of V st x1 <> x2 & x1 in L & x2 in L holds
L = Line (x1,x2) by Th75; :: thesis: verum