let n be Nat; :: thesis: for p1, p2 being Point of (TOP-REAL n) holds
( p1 in Line (p1,p2) & p2 in Line (p1,p2) )
let p1, p2 be Point of (TOP-REAL n); :: thesis: ( p1 in Line (p1,p2) & p2 in Line (p1,p2) )
ex x1, x2 being Element of REAL n st
( x1 = p1 & x2 = p2 & Line (x1,x2) = Line (p1,p2) ) by Lm8;
hence ( p1 in Line (p1,p2) & p2 in Line (p1,p2) ) by Th10; :: thesis: verum