reconsider SF = {{}} as Subset-Family of [:{},{}:] by ZFMISC_1:1;
set US = UniformSpaceStr(# {},SF #);

now :: thesis: ( UniformSpaceStr(# {},SF #) is upper & UniformSpaceStr(# {},SF #) is cap-closed & UniformSpaceStr(# {},SF #) is axiom_U1 & UniformSpaceStr(# {},SF #) is axiom_U2 & UniformSpaceStr(# {},SF #) is axiom_U3 )

the entourages of UniformSpaceStr(# {},SF #) is upper ;
hence UniformSpaceStr(# {},SF #) is upper ; :: thesis: ( UniformSpaceStr(# {},SF #) is cap-closed & UniformSpaceStr(# {},SF #) is axiom_U1 & UniformSpaceStr(# {},SF #) is axiom_U2 & UniformSpaceStr(# {},SF #) is axiom_U3 )
the entourages of UniformSpaceStr(# {},SF #) is cap-closed ;
hence UniformSpaceStr(# {},SF #) is cap-closed ; :: thesis: ( UniformSpaceStr(# {},SF #) is axiom_U1 & UniformSpaceStr(# {},SF #) is axiom_U2 & UniformSpaceStr(# {},SF #) is axiom_U3 )
for S being Element of the entourages of UniformSpaceStr(# {},SF #) holds id the carrier of UniformSpaceStr(# {},SF #) c= S ;
hence UniformSpaceStr(# {},SF #) is axiom_U1 ; :: thesis: ( UniformSpaceStr(# {},SF #) is axiom_U2 & UniformSpaceStr(# {},SF #) is axiom_U3 )

now :: thesis: for S being Element of the entourages of UniformSpaceStr(# {},SF #) holds S ~ in the entourages of UniformSpaceStr(# {},SF #)

let S be Element of the entourages of UniformSpaceStr(# {},SF #); :: thesis: S ~ in the entourages of UniformSpaceStr(# {},SF #)
S [~] = {} ;
hence S ~ in the entourages of UniformSpaceStr(# {},SF #) by TARSKI:def 1; :: thesis: verum

end;

hence UniformSpaceStr(# {},SF #) is axiom_U2 ; :: thesis: UniformSpaceStr(# {},SF #) is axiom_U3

now :: thesis: for S being Element of the entourages of UniformSpaceStr(# {},SF #) ex W being Element of the entourages of UniformSpaceStr(# {},SF #) st W * W c= S

let S be Element of the entourages of UniformSpaceStr(# {},SF #); :: thesis: ex W being Element of the entourages of UniformSpaceStr(# {},SF #) st W * W c= S
S [*] S = {} ;
then S * S = S by TARSKI:def 1;
hence ex W being Element of the entourages of UniformSpaceStr(# {},SF #) st W * W c= S ; :: thesis: verum

end;

hence UniformSpaceStr(# {},SF #) is axiom_U3 ; :: thesis: verum

end;

hence ex b₁ being UniformSpace st b₁ is strict ; :: thesis: verum