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

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