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:18;
then (Cl T) ` c= T ` by SUBSET_1:12;
then Cl ((Cl T) `) c= Cl (T `) by PRE_TOPC:19;
hence Fr (Cl T) c= Fr T by XBOOLE_1:26; :: thesis: verum