let GX be TopStruct ; :: thesis: for T being Subset of GX holds Int T c= T
let T be Subset of GX; :: thesis: Int T c= T
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Int T or x in T )
assume A1: x in Int T ; :: thesis: x in T
then reconsider x99 = x as Point of GX ;
T ` c= Cl (T `) by PRE_TOPC:18;
then not x99 in T ` by A1, XBOOLE_0:def 5;
hence x in T by A1, XBOOLE_0:def 5; :: thesis: verum