let n be Nat; :: thesis: for An, Bn being Point of (TOP-REAL n)

for PAn, PBn being Element of REAL n st An = PAn & Bn = PBn holds

Line (An,Bn) = Line (PAn,PBn)

let An, Bn be Point of (TOP-REAL n); :: thesis: for PAn, PBn being Element of REAL n st An = PAn & Bn = PBn holds

Line (An,Bn) = Line (PAn,PBn)

let PAn, PBn be Element of REAL n; :: thesis: ( An = PAn & Bn = PBn implies Line (An,Bn) = Line (PAn,PBn) )

assume A1: ( An = PAn & Bn = PBn ) ; :: thesis: Line (An,Bn) = Line (PAn,PBn)

hence Line (An,Bn) = Line (PAn,PBn) ; :: thesis: verum

for PAn, PBn being Element of REAL n st An = PAn & Bn = PBn holds

Line (An,Bn) = Line (PAn,PBn)

let An, Bn be Point of (TOP-REAL n); :: thesis: for PAn, PBn being Element of REAL n st An = PAn & Bn = PBn holds

Line (An,Bn) = Line (PAn,PBn)

let PAn, PBn be Element of REAL n; :: thesis: ( An = PAn & Bn = PBn implies Line (An,Bn) = Line (PAn,PBn) )

assume A1: ( An = PAn & Bn = PBn ) ; :: thesis: Line (An,Bn) = Line (PAn,PBn)

now :: thesis: ( ( for x being object st x in Line (An,Bn) holds

x in Line (PAn,PBn) ) & ( for x being object st x in Line (PAn,PBn) holds

x in Line (An,Bn) ) )

assume x in Line (PAn,PBn) ; :: thesis: x in Line (An,Bn)

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: verum

end;

then
( Line (An,Bn) c= Line (PAn,PBn) & Line (PAn,PBn) c= Line (An,Bn) )
;x in Line (PAn,PBn) ) & ( for x being object st x in Line (PAn,PBn) holds

x in Line (An,Bn) ) )

hereby :: thesis: for x being object st x in Line (PAn,PBn) holds

x in Line (An,Bn)

let x be object ; :: thesis: ( x in Line (PAn,PBn) implies x in Line (An,Bn) )x in Line (An,Bn)

let x be object ; :: thesis: ( x in Line (An,Bn) implies x in Line (PAn,PBn) )

assume x in Line (An,Bn) ; :: thesis: x in Line (PAn,PBn)

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: verum

end;assume x in Line (An,Bn) ; :: thesis: x in Line (PAn,PBn)

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: verum

assume x in Line (PAn,PBn) ; :: thesis: x in Line (An,Bn)

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: verum

hence Line (An,Bn) = Line (PAn,PBn) ; :: thesis: verum