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

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