assume not the entourages of USS is with_non-empty_elements ; :: thesis: contradiction
then A1: {} in the entourages of USS by SETFAM_1:def 8;
USS is axiom_U1 ;
then id the carrier of USS c= {} by A1;
hence contradiction ; :: thesis: verum