let T be TopSpace; :: thesis: for F being Subset-Family of T st F = {} holds
Fr F = {}
let F be Subset-Family of T; :: thesis: ( F = {} implies Fr F = {} )
assume A1: F = {} ; :: thesis: Fr F = {}
assume Fr F <> {} ; :: thesis: contradiction
then consider x being object such that
A2: x in Fr F by XBOOLE_0:def 1;
ex B being Subset of T st
( x = Fr B & B in F ) by A2, Def1;
hence contradiction by A1; :: thesis: verum