let GX be TopStruct ; :: thesis: for R being Subset of GX holds
( R is open iff R ` is closed )
let R be Subset of GX; :: thesis: ( R is open iff R ` is closed )
( R ` is closed iff (R `) ` is open ) by Th3;
hence ( R is open iff R ` is closed ) ; :: thesis: verum