set X = {{}};
set US = NonEmptyTrivialUniformSpace ;
set E = the entourages of NonEmptyTrivialUniformSpace;
consider SF being Subset-Family of [:{{}},{{}}:] such that
B1:
SF = {[:{{}},{{}}:]}
and
B2:
NonEmptyTrivialUniformSpace = UniformSpaceStr(# {{}},SF #)
by D1;
for Y1, Y2 being Subset of [: the carrier of NonEmptyTrivialUniformSpace, the carrier of NonEmptyTrivialUniformSpace:] st Y1 in the entourages of NonEmptyTrivialUniformSpace & Y1 c= Y2 holds
Y2 in the entourages of NonEmptyTrivialUniformSpace
hence
the entourages of NonEmptyTrivialUniformSpace is upper
; UNIFORM2:def 7 ( NonEmptyTrivialUniformSpace is cap-closed & NonEmptyTrivialUniformSpace is axiom_U1 & NonEmptyTrivialUniformSpace is axiom_U2 & NonEmptyTrivialUniformSpace is axiom_U3 )
for a, b being Subset of [: the carrier of NonEmptyTrivialUniformSpace, the carrier of NonEmptyTrivialUniformSpace:] st a in the entourages of NonEmptyTrivialUniformSpace & b in the entourages of NonEmptyTrivialUniformSpace holds
a /\ b in the entourages of NonEmptyTrivialUniformSpace
proof
let a,
b be
Subset of
[: the carrier of NonEmptyTrivialUniformSpace, the carrier of NonEmptyTrivialUniformSpace:];
( a in the entourages of NonEmptyTrivialUniformSpace & b in the entourages of NonEmptyTrivialUniformSpace implies a /\ b in the entourages of NonEmptyTrivialUniformSpace )
assume that A5:
a in the
entourages of
NonEmptyTrivialUniformSpace
and A6:
b in the
entourages of
NonEmptyTrivialUniformSpace
;
a /\ b in the entourages of NonEmptyTrivialUniformSpace
(
a = [:{{}},{{}}:] &
b = [:{{}},{{}}:] )
by B1, B2, A5, A6, TARSKI:def 1;
hence
a /\ b in the
entourages of
NonEmptyTrivialUniformSpace
by B1, B2, TARSKI:def 1;
verum
end;
hence
NonEmptyTrivialUniformSpace is cap-closed
by ROUGHS_4:def 2; ( NonEmptyTrivialUniformSpace is axiom_U1 & NonEmptyTrivialUniformSpace is axiom_U2 & NonEmptyTrivialUniformSpace is axiom_U3 )
for S being Element of the entourages of NonEmptyTrivialUniformSpace holds id {{}} c= S
hence
NonEmptyTrivialUniformSpace is axiom_U1
by B2; ( NonEmptyTrivialUniformSpace is axiom_U2 & NonEmptyTrivialUniformSpace is axiom_U3 )
thus
for S being Element of the entourages of NonEmptyTrivialUniformSpace holds S ~ in the entourages of NonEmptyTrivialUniformSpace
UNIFORM2:def 10 NonEmptyTrivialUniformSpace is axiom_U3
let S be Element of the entourages of NonEmptyTrivialUniformSpace; UNIFORM2:def 11 ex W being Element of the entourages of NonEmptyTrivialUniformSpace st W [*] W c= S
take
S
; S [*] S c= S
S = [:{{}},{{}}:]
by B1, B2, TARSKI:def 1;
hence
S [*] S c= S
by B2; verum