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 V288() ;
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 b1 being UniformSpace st b1 is strict ; :: thesis: verum