let FT be non empty RelStr ; :: thesis: for P being Subset of FT holds

( P is closed iff P ` is open )

let P be Subset of FT; :: thesis: ( P is closed iff P ` is open )

( P ` is open implies (P `) ` is closed ) by FIN_TOPO:23;

hence ( P is closed iff P ` is open ) by FIN_TOPO:24; :: thesis: verum

( P is closed iff P ` is open )

let P be Subset of FT; :: thesis: ( P is closed iff P ` is open )

( P ` is open implies (P `) ` is closed ) by FIN_TOPO:23;

hence ( P is closed iff P ` is open ) by FIN_TOPO:24; :: thesis: verum