let n, m be Nat; :: thesis: ( n in Seg m implies PROJ m,n is open )
set f = PROJ m,n;
assume A1: n in Seg m ; :: thesis: PROJ m,n is open
for p being Point of (TOP-REAL m)
for r being real positive number ex s being real positive number 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); :: thesis: for r being real positive number ex s being real positive number st ].(((PROJ m,n) . p) - s),(((PROJ m,n) . p) + s).[ c= (PROJ m,n) .: (Ball p,r)
let r be real positive number ; :: thesis: ex s being real positive number st ].(((PROJ m,n) . p) - s),(((PROJ m,n) . p) + s).[ c= (PROJ m,n) .: (Ball p,r)
take r ; :: thesis: ].(((PROJ m,n) . p) - r),(((PROJ m,n) . p) + r).[ c= (PROJ m,n) .: (Ball p,r)
A2: dom p = Seg m by EUCLID:3;
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; :: thesis: verum

end;

hence PROJ m,n is open by TOPS_4:13; :: thesis: verum