[STATEMENT]
lemma (in topology) frontier_closed [iff]:
  "frontier s closed"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frontier s closed
[PROOF STEP]
by (unfold frt_def)
(intro closure_closed core_open closed_diff_open)