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

A is open

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

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

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

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

.= (A ^i) ` ;

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

.= A ^i ;

hence A is open ; :: thesis: verum

A is open

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

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

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

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

.= (A ^i) ` ;

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

.= A ^i ;

hence A is open ; :: thesis: verum