set US = TrivialUniformSpace ;
set E = the entourages of TrivialUniformSpace;
A1: the entourages of TrivialUniformSpace = {{}} by ENUMSET1:29;
the entourages of TrivialUniformSpace is upper ;
hence TrivialUniformSpace is upper ; :: thesis: ( TrivialUniformSpace is cap-closed & TrivialUniformSpace is axiom_U1 & TrivialUniformSpace is axiom_U2 & TrivialUniformSpace is axiom_U3 )
for X, Y being set st X in the entourages of TrivialUniformSpace & Y in the entourages of TrivialUniformSpace holds
X /\ Y in the entourages of TrivialUniformSpace ;
hence TrivialUniformSpace is cap-closed by FINSUB_1:def 2; :: thesis: ( TrivialUniformSpace is axiom_U1 & TrivialUniformSpace is axiom_U2 & TrivialUniformSpace is axiom_U3 )
for S being Element of the entourages of TrivialUniformSpace holds id the carrier of TrivialUniformSpace c= S ;
hence TrivialUniformSpace is axiom_U1 ; :: thesis: ( TrivialUniformSpace is axiom_U2 & TrivialUniformSpace is axiom_U3 )
now :: thesis: for S being Element of the entourages of TrivialUniformSpace holds S ~ in the entourages of TrivialUniformSpace
let S be Element of the entourages of TrivialUniformSpace; :: thesis: S ~ in the entourages of TrivialUniformSpace
S in {{}} by A1;
hence S ~ in the entourages of TrivialUniformSpace by A1; :: thesis: verum
end;
hence TrivialUniformSpace is axiom_U2 ; :: thesis: TrivialUniformSpace is axiom_U3
let S be Element of the entourages of TrivialUniformSpace; :: according to UNIFORM2:def 11 :: thesis: ex W being Element of the entourages of TrivialUniformSpace st W [*] W c= S
S [*] S c= S ;
hence ex W being Element of the entourages of TrivialUniformSpace st W [*] W c= S ; :: thesis: verum