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