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 by FIN_TOPO:def 17;
(A ` ) ^b = (((A ` ) ` ) ^i ) ` by FIN_TOPO:22
.= (A ^i ) ` ;
then A = ((A ^i ) ` ) ` by A1
.= A ^i ;
hence A is open by FIN_TOPO:def 16; :: thesis: verum