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 by Def17;
(A ` ) ^Fob = (((A ` ) ` ) ^Foi ) ` by Th39
.= (A ^Foi ) ` ;
then A = ((A ^Foi ) ` ) ` by A1
.= A ^Foi ;
hence A is Fo_open by Def16; :: thesis: verum