:: deftheorem defines being_point EUCLID12:def 1 :
for n being Nat
for S being Subset of (REAL n) holds
( S is being_point iff ex Pn being Element of REAL n st S = {Pn} );