let TS be TopSpace; :: thesis: for GX being TopStruct
for P being Subset of TS
for R being Subset of GX holds
( ( R is open implies Int R = R ) & ( Int P = P implies P is open ) )
let GX be TopStruct ; :: thesis: for P being Subset of TS
for R being Subset of GX holds
( ( R is open implies Int R = R ) & ( Int P = P implies P is open ) )
let P be Subset of TS; :: thesis: for R being Subset of GX holds
( ( R is open implies Int R = R ) & ( Int P = P implies P is open ) )
let R be Subset of GX; :: thesis: ( ( R is open implies Int R = R ) & ( Int P = P implies P is open ) )

hereby :: thesis: ( Int P = P implies P is open )

assume R is open ; :: thesis: Int R = R
then R ` is closed by Th4;
then Cl (R `) = R ` by PRE_TOPC:22;
hence Int R = R ; :: thesis: verum

end;

thus ( Int P = P implies P is open ) ; :: thesis: verum