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}

hence Line (Pn,Pn) = {Pn} ; :: thesis: verum

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) ) )

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) )
;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 {Pn} implies x in Line (Pn,Pn) )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;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

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

hence Line (Pn,Pn) = {Pn} ; :: thesis: verum