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