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

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