let T be TopStruct ; :: thesis: for x, y being Point of T
for X, Y being Subset of T st X = {x} & Cl X c= Cl Y holds
x in Cl Y
let x, y be Point of T; :: thesis: for X, Y being Subset of T st X = {x} & Cl X c= Cl Y holds
x in Cl Y
let X, Y be Subset of T; :: thesis: ( X = {x} & Cl X c= Cl Y implies x in Cl Y )
assume that
A1: X = {x} and
A2: Cl X c= Cl Y ; :: thesis: x in Cl Y
X c= Cl X by PRE_TOPC:18;
then A3: X c= Cl Y by A2;
x in X by A1, TARSKI:def 1;
hence x in Cl Y by A3; :: thesis: verum