theorem Th3: :: EUCLID12:3

for n being Nat
for Pn being Element of REAL n holds Line (Pn,Pn) = {Pn}