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
A3: t in Int N by CONNSP_2:def 1;
A4: Int N c= N by TOPS_1:44;
M is open by A2, TOPS_2:32;
then Int M = M by TOPS_1:55;
then z in Int M by A1, A2, A3, A4, XBOOLE_0:def 4;
hence M is open a_neighborhood of z by A2, CONNSP_2:def 1, TOPS_2:32; :: thesis: verum