let n be Nat; :: thesis: for Pn being Element of REAL n holds Line (Pn,Pn) = {Pn}
let Pn be Element of REAL n; :: thesis: Line (Pn,Pn) = {Pn}
now :: thesis: ( ( for x being object st x in Line (Pn,Pn) holds
x in {Pn} ) & ( for x being object st x in {Pn} holds
x in Line (Pn,Pn) ) )
hereby :: thesis: for x being object st x in {Pn} holds
x in Line (Pn,Pn)
let x be object ; :: thesis: ( x in Line (Pn,Pn) implies x in {Pn} )
assume x in Line (Pn,Pn) ; :: thesis: x in {Pn}
then consider lambda being Real such that
A1: x = ((1 - lambda) * Pn) + (lambda * Pn) ;
x = ((1 - lambda) + lambda) * Pn by A1, EUCLID_4:7
.= Pn by EUCLID_4:3 ;
hence x in {Pn} by TARSKI:def 1; :: thesis: verum
end;
let x be object ; :: thesis: ( x in {Pn} implies x in Line (Pn,Pn) )
assume x in {Pn} ; :: thesis: x in Line (Pn,Pn)
then x = Pn by TARSKI:def 1;
hence x in Line (Pn,Pn) by EUCLID_4:9; :: thesis: verum
end;
then ( Line (Pn,Pn) c= {Pn} & {Pn} c= Line (Pn,Pn) ) ;
hence Line (Pn,Pn) = {Pn} ; :: thesis: verum