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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in Fr (Fr T) or x in Fr T )
assume A1: x in Fr (Fr T) ; :: thesis: x in Fr T
A2: Cl ((Cl T) /\ (Cl (T ` ))) c= (Cl (Cl T)) /\ (Cl (Cl (T ` ))) by PRE_TOPC:51;
x in Cl ((Cl T) /\ (Cl (T ` ))) by A1, XBOOLE_0:def 4;
hence x in Fr T by A2; :: thesis: verum