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 by Def16;
A ^i = ((A `) ^b) ` by Th23;
hence A ` is closed by A1, Def17; :: thesis: verum