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 set ; :: 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 x'' = x as Point of GX ;
A2: not GX is empty by A1;
T ` c= Cl (T ` ) by PRE_TOPC:48;
then not x'' in T ` by A1, XBOOLE_0:def 5;
hence x in T by A2, Lm2; :: thesis: verum