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 ;
A ^b = ((A `) ^i) ` by Th16;
hence A ` is open by A1; :: thesis: verum