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