[STATEMENT]
lemma closure_of_eq_topspace:
   "X closure_of S = topspace X \<longleftrightarrow> X interior_of (topspace X - S) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (X closure_of S = topspace X) = (X interior_of (topspace X - S) = {})
[PROOF STEP]
using closure_of_subset_topspace [of X S] interior_of_complement
[PROOF STATE]
proof (prove)
using this:
X closure_of S \<subseteq> topspace X
?X interior_of (topspace ?X - ?S) = topspace ?X - ?X closure_of ?S

goal (1 subgoal):
 1. (X closure_of S = topspace X) = (X interior_of (topspace X - S) = {})
[PROOF STEP]
by fastforce