let FT be non empty RelStr ; :: thesis: for A being Subset of FT st A ` is open holds
A is closed
let A be Subset of FT; :: thesis: ( A ` is open implies A is closed )
assume A ` is open ; :: thesis: A is closed
then A1: A ` = (A `) ^i ;
(A `) ^i = (((A `) `) ^b) ` by FIN_TOPO:17
.= (A ^b) ` ;
then A = ((A ^b) `) ` by A1
.= A ^b ;
hence A is closed ; :: thesis: verum