let FMT be non empty FMT_Space_Str ; :: thesis: for A being Subset of FMT st A ` is Fo_open holds
A is Fo_closed
let A be Subset of FMT; :: thesis: ( A ` is Fo_open implies A is Fo_closed )
assume A ` is Fo_open ; :: thesis: A is Fo_closed
then A1: A ` = (A `) ^Foi ;
(((A `) ^Foi) `) ` = (A ^Fob) ` by Th38;
hence A is Fo_closed by A1; :: thesis: verum