let T be non empty TopSpace; :: thesis: for Z being non empty SubSpace of T
for t being Point of T
for z being Point of Z
for N being open a_neighborhood of t
for M being Subset of Z st t = z & M = N /\ ([#] Z) holds
M is open a_neighborhood of z
let Z be non empty SubSpace of T; :: thesis: for t being Point of T
for z being Point of Z
for N being open a_neighborhood of t
for M being Subset of Z st t = z & M = N /\ ([#] Z) holds
M is open a_neighborhood of z
let t be Point of T; :: thesis: for z being Point of Z
for N being open a_neighborhood of t
for M being Subset of Z st t = z & M = N /\ ([#] Z) holds
M is open a_neighborhood of z
let z be Point of Z; :: thesis: for N being open a_neighborhood of t
for M being Subset of Z st t = z & M = N /\ ([#] Z) holds
M is open a_neighborhood of z
let N be open a_neighborhood of t; :: thesis: for M being Subset of Z st t = z & M = N /\ ([#] Z) holds
M is open a_neighborhood of z
let M be Subset of Z; :: thesis: ( t = z & M = N /\ ([#] Z) implies M is open a_neighborhood of z )
assume that
A1: t = z and
A2: M = N /\ ([#] Z) ; :: thesis: M is open a_neighborhood of z
M is open by A2, TOPS_2:24;
then A3: Int M = M by TOPS_1:23;
( t in Int N & Int N c= N ) by CONNSP_2:def 1, TOPS_1:16;
then z in Int M by A1, A2, A3, XBOOLE_0:def 4;
hence M is open a_neighborhood of z by A2, CONNSP_2:def 1, TOPS_2:24; :: thesis: verum