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