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