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 Th17;
hence A ` is closed by A1; :: thesis: verum