let GX be TopStruct ; :: thesis: for T being Subset of GX holds Fr (Cl T) c= Fr T
let T be Subset of GX; :: thesis: Fr (Cl T) c= Fr T
T c= Cl T by PRE_TOPC:48;
then (Cl T) ` c= T ` by SUBSET_1:31;
then Cl ((Cl T) ` ) c= Cl (T ` ) by PRE_TOPC:49;
hence Fr (Cl T) c= Fr T by XBOOLE_1:26; :: thesis: verum