let GX be TopStruct ; :: thesis: for T being Subset of GX holds Fr (Int T) c= Fr T
let T be Subset of GX; :: thesis: Fr (Int T) c= Fr T
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Fr (Int T) or x in Fr T )
assume x in Fr (Int T) ; :: thesis: x in Fr T
then A1: ( x in Cl ((Cl (T ` )) ` ) & x in Cl (T ` ) ) by XBOOLE_0:def 4;
Int T = (Cl (T ` )) ` ;
then Cl ((Cl (T ` )) ` ) c= Cl T by Th44, PRE_TOPC:49;
hence x in Fr T by A1, XBOOLE_0:def 4; :: thesis: verum