let GX be TopStruct ; :: thesis: for T being Subset of GX holds Fr (Fr T) c= Fr T
let T be Subset of GX; :: thesis: Fr (Fr T) c= Fr T
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Fr (Fr T) or x in Fr T )
assume x in Fr (Fr T) ; :: thesis: x in Fr T
then A1: x in Cl ((Cl T) /\ (Cl (T `))) by XBOOLE_0:def 4;
Cl ((Cl T) /\ (Cl (T `))) c= (Cl (Cl T)) /\ (Cl (Cl (T `))) by PRE_TOPC:21;
hence x in Fr T by A1; :: thesis: verum