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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in Fr (Int T) or x in Fr T )
assume A1: x in Fr (Int T) ; :: thesis: x in Fr T
then A2: x in Cl (T `) by XBOOLE_0:def 4;
Int T = (Cl (T `)) ` ;
then A3: Cl ((Cl (T `)) `) c= Cl T by Th16, PRE_TOPC:19;
x in Cl ((Cl (T `)) `) by A1, XBOOLE_0:def 4;
hence x in Fr T by A2, A3, XBOOLE_0:def 4; :: thesis: verum