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 A1: R is closed ; :: thesis: Fr R c= R
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Fr R or x in R )
Cl R = R by A1, PRE_TOPC:22;
hence ( not x in Fr R or x in R ) by XBOOLE_0:def 4; :: thesis: verum