Theorem iscld2

Description: A subset of the underlying set of a topology is closed iff its complement is open. (Contributed by NM, 4-Oct-2006)

	Ref	Expression
Hypothesis	iscld.1	|- X = U. J
Assertion	iscld2	|- ( ( J e. Top /\ S C_ X ) -> ( S e. ( Clsd ` J ) <-> ( X \ S ) e. J ) )

Proof

Step	Hyp	Ref	Expression
1		iscld.1	|- X = U. J
2	1	iscld	|- ( J e. Top -> ( S e. ( Clsd ` J ) <-> ( S C_ X /\ ( X \ S ) e. J ) ) )
3	2	baibd	|- ( ( J e. Top /\ S C_ X ) -> ( S e. ( Clsd ` J ) <-> ( X \ S ) e. J ) )