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