let T be TopStruct ; :: thesis: for x, y being Point of T
for Y, V being Subset of T st Y = {y} & x in Cl Y & V is open & x in V holds
y in V
let x, y be Point of T; :: thesis: for Y, V being Subset of T st Y = {y} & x in Cl Y & V is open & x in V holds
y in V
let Y, V be Subset of T; :: thesis: ( Y = {y} & x in Cl Y & V is open & x in V implies y in V )
assume A1: Y = {y} ; :: thesis: ( not x in Cl Y or not V is open or not x in V or y in V )
assume ( x in Cl Y & V is open & x in V ) ; :: thesis: y in V
then Y meets V by PRE_TOPC:def 7;
hence y in V by A1, ZFMISC_1:50; :: thesis: verum