let US be strict UniformSpaceStr ; :: thesis: ( US is empty implies US is axiom_U1 )
assume US is empty ; :: thesis: US is axiom_U1
hence for S being Element of the entourages of US holds id the carrier of US c= S ; :: according to UNIFORM2:def 9 :: thesis: verum