theorem :: TOPREALC:58

for n, m being Nat st n in Seg m holds
PROJ (m,n) is open