let FT be non empty RelStr ; :: thesis: for A being Subset of FT st A ` is open holds

A is closed

let A be Subset of FT; :: thesis: ( A ` is open implies A is closed )

assume A ` is open ; :: thesis: A is closed

then A1: A ` = (A `) ^i ;

(A `) ^i = (((A `) `) ^b) ` by FIN_TOPO:17

.= (A ^b) ` ;

then A = ((A ^b) `) ` by A1

.= A ^b ;

hence A is closed ; :: thesis: verum

A is closed

let A be Subset of FT; :: thesis: ( A ` is open implies A is closed )

assume A ` is open ; :: thesis: A is closed

then A1: A ` = (A `) ^i ;

(A `) ^i = (((A `) `) ^b) ` by FIN_TOPO:17

.= (A ^b) ` ;

then A = ((A ^b) `) ` by A1

.= A ^b ;

hence A is closed ; :: thesis: verum