let GX be TopStruct ; :: thesis: for R being Subset of GX st R is closed holds
Fr R c= R
let R be Subset of GX; :: thesis: ( R is closed implies Fr R c= R )
assume R is closed ; :: thesis: Fr R c= R
then A1: Cl R = R by PRE_TOPC:52;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Fr R or x in R )
thus ( not x in Fr R or x in R ) by A1, XBOOLE_0:def 4; :: thesis: verum