let T be non empty TopSpace; :: thesis: Fr ({} T) = {}
Fr ({} T) = (Cl ({} T)) /\ (Cl (({} T) `)) by TOPS_1:def 2
.= {} /\ (Cl (({} T) `)) ;
hence Fr ({} T) = {} ; :: thesis: verum