let n be Nat; :: thesis:
let An, Bn be Point of (TOP-REAL n); :: thesis:
let PAn, PBn be Element of REAL n; :: thesis:
assume A1: ( An = PAn & Bn = PBn ) ; :: thesis:

now :: thesis:

hereby :: thesis:

let x be object ; :: thesis:
assume x in Line (An,Bn) ; :: thesis:
then x in { (((1 - lambda) * An) + (lambda * Bn)) where lambda is Real : verum } by RLTOPSP1:def 14;
then consider l0 being Real such that
A2: x = ((1 - l0) * An) + (l0 * Bn) ;
thus x in Line (PAn,PBn) by A1, A2; :: thesis:

end;

let x be object ; :: thesis:
assume x in Line (PAn,PBn) ; :: thesis:
then consider l0 being Real such that
A3: x = ((1 - l0) * PAn) + (l0 * PBn) ;
x = ((1 - l0) * An) + (l0 * Bn) by A1, A3;
then x in { (((1 - lambda) * An) + (lambda * Bn)) where lambda is Real : verum } ;
hence x in Line (An,Bn) by RLTOPSP1:def 14; :: thesis:

end;

then ( Line (An,Bn) c= Line (PAn,PBn) & Line (PAn,PBn) c= Line (An,Bn) ) ;
hence Line (An,Bn) = Line (PAn,PBn) ; :: thesis: