let T be TopStruct ; :: thesis: for x, y being Element of T
for X, Y being Subset of T st X = {x} & Y = {y} holds
( x in Cl Y iff Cl X c= Cl Y )
let x, y be Element of T; :: thesis: for X, Y being Subset of T st X = {x} & Y = {y} holds
( x in Cl Y iff Cl X c= Cl Y )
let X, Y be Subset of T; :: thesis: ( X = {x} & Y = {y} implies ( x in Cl Y iff Cl X c= Cl Y ) )
assume that
A1: X = {x} and
A2: Y = {y} ; :: thesis: ( x in Cl Y iff Cl X c= Cl Y )

hereby :: thesis: ( Cl X c= Cl Y implies x in Cl Y )

assume x in Cl Y ; :: thesis: Cl X c= Cl Y
then for V being Subset of T st V is open & x in V holds
y in V by A2, YELLOW14:21;
hence Cl X c= Cl Y by A1, A2, YELLOW14:22; :: thesis: verum

end;

assume Cl X c= Cl Y ; :: thesis: x in Cl Y
hence x in Cl Y by A1, YELLOW14:20; :: thesis: verum