let n, m be Nat; ( n in Seg m implies PROJ (m,n) is open )
set f = PROJ (m,n);
assume A1:
n in Seg m
; PROJ (m,n) is open
for p being Point of (TOP-REAL m)
for r being positive Real ex s being positive Real st ].(((PROJ (m,n)) . p) - s),(((PROJ (m,n)) . p) + s).[ c= (PROJ (m,n)) .: (Ball (p,r))
proof
let p be
Point of
(TOP-REAL m);
for r being positive Real ex s being positive Real st ].(((PROJ (m,n)) . p) - s),(((PROJ (m,n)) . p) + s).[ c= (PROJ (m,n)) .: (Ball (p,r))let r be
positive Real;
ex s being positive Real st ].(((PROJ (m,n)) . p) - s),(((PROJ (m,n)) . p) + s).[ c= (PROJ (m,n)) .: (Ball (p,r))
take
r
;
].(((PROJ (m,n)) . p) - r),(((PROJ (m,n)) . p) + r).[ c= (PROJ (m,n)) .: (Ball (p,r))
A2:
dom p = Seg m
by FINSEQ_1:89;
p /. n = (PROJ (m,n)) . p
by Def6;
hence
].(((PROJ (m,n)) . p) - r),(((PROJ (m,n)) . p) + r).[ c= (PROJ (m,n)) .: (Ball (p,r))
by A2, A1, Th55;
verum
end;
hence
PROJ (m,n) is open
by TOPS_4:13; verum