for n being Element of NAT
for X being Subset of (TOP-REAL n) holds 1 (.) X = X