let GX be TopStruct ; :: thesis: for R being Subset of GX holds
( R is closed iff R ` is open )
let R be Subset of GX; :: thesis: ( R is closed iff R ` is open )
( R is closed iff ([#] GX) \ R is open ) by PRE_TOPC:def 3;
hence ( R is closed iff R ` is open ) ; :: thesis: verum