let SUS be Semi-UniformSpace; :: thesis: ( SUS is empty implies {} in the entourages of SUS )
assume A1: SUS is empty ; :: thesis: {} in the entourages of SUS
assume A2: not {} in the entourages of SUS ; :: thesis: contradiction
not SUS is void ;
then not the entourages of SUS is empty ;
hence contradiction by A1, A2; :: thesis: verum