theorem :: CKSPACE1:24

for m being non zero Element of NAT
for k being Element of NAT
for X being non empty open Subset of (REAL m) holds 1_ (R_Algebra_of_Ck_Functions (k,X)) = X --> 1