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

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