let T be non empty TopSpace; :: thesis: for A being Subset of T holds

( A is closed iff Der A c= A )

let A be Subset of T; :: thesis: ( A is closed iff Der A c= A )

Cl A = A \/ (Der A) by TOPGEN_1:29

.= A by A2, XBOOLE_1:12 ;

hence A is closed ; :: thesis: verum

( A is closed iff Der A c= A )

let A be Subset of T; :: thesis: ( A is closed iff Der A c= A )

hereby :: thesis: ( Der A c= A implies A is closed )

assume A2:
Der A c= A
; :: thesis: A is closed assume
A is closed
; :: thesis: Der A c= A

then A1: A = Cl A by PRE_TOPC:22;

Cl A = A \/ (Der A) by TOPGEN_1:29;

hence Der A c= A by A1, XBOOLE_1:7; :: thesis: verum

end;then A1: A = Cl A by PRE_TOPC:22;

Cl A = A \/ (Der A) by TOPGEN_1:29;

hence Der A c= A by A1, XBOOLE_1:7; :: thesis: verum

Cl A = A \/ (Der A) by TOPGEN_1:29

.= A by A2, XBOOLE_1:12 ;

hence A is closed ; :: thesis: verum