assume the entourages of USS is empty ; :: thesis: contradiction
then reconsider S = {} as Element of the entourages of USS by SUBSET_1:def 1;
USS is axiom_U1 ;
then id the carrier of USS c= S ;
hence contradiction ; :: thesis: verum