set X = {{}};
reconsider SF = {[:{{}},{{}}:]} as Subset-Family of [:{{}},{{}}:] by ZFMISC_1:68;
set US = UniformSpaceStr(# {{}},SF #);
now ( UniformSpaceStr(# {{}},SF #) is upper & UniformSpaceStr(# {{}},SF #) is cap-closed & UniformSpaceStr(# {{}},SF #) is axiom_U1 & UniformSpaceStr(# {{}},SF #) is axiom_U2 & UniformSpaceStr(# {{}},SF #) is axiom_U3 )
for
Y1,
Y2 being
Subset of
[: the carrier of UniformSpaceStr(# {{}},SF #), the carrier of UniformSpaceStr(# {{}},SF #):] st
Y1 in the
entourages of
UniformSpaceStr(#
{{}},
SF #) &
Y1 c= Y2 holds
Y2 in the
entourages of
UniformSpaceStr(#
{{}},
SF #)
proof
let Y1,
Y2 be
Subset of
[: the carrier of UniformSpaceStr(# {{}},SF #), the carrier of UniformSpaceStr(# {{}},SF #):];
( Y1 in the entourages of UniformSpaceStr(# {{}},SF #) & Y1 c= Y2 implies Y2 in the entourages of UniformSpaceStr(# {{}},SF #) )
assume that A1:
Y1 in the
entourages of
UniformSpaceStr(#
{{}},
SF #)
and A2:
Y1 c= Y2
;
Y2 in the entourages of UniformSpaceStr(# {{}},SF #)
A3:
Y1 = [:{{}},{{}}:]
by A1, TARSKI:def 1;
Y1 = Y2
by A2, A3;
hence
Y2 in the
entourages of
UniformSpaceStr(#
{{}},
SF #)
by A1;
verum
end; then
the
entourages of
UniformSpaceStr(#
{{}},
SF #) is
upper
;
hence
UniformSpaceStr(#
{{}},
SF #) is
upper
;
( UniformSpaceStr(# {{}},SF #) is cap-closed & UniformSpaceStr(# {{}},SF #) is axiom_U1 & UniformSpaceStr(# {{}},SF #) is axiom_U2 & UniformSpaceStr(# {{}},SF #) is axiom_U3 )
for
a,
b being
Subset of
[: the carrier of UniformSpaceStr(# {{}},SF #), the carrier of UniformSpaceStr(# {{}},SF #):] st
a in the
entourages of
UniformSpaceStr(#
{{}},
SF #) &
b in the
entourages of
UniformSpaceStr(#
{{}},
SF #) holds
a /\ b in the
entourages of
UniformSpaceStr(#
{{}},
SF #)
proof
let a,
b be
Subset of
[: the carrier of UniformSpaceStr(# {{}},SF #), the carrier of UniformSpaceStr(# {{}},SF #):];
( a in the entourages of UniformSpaceStr(# {{}},SF #) & b in the entourages of UniformSpaceStr(# {{}},SF #) implies a /\ b in the entourages of UniformSpaceStr(# {{}},SF #) )
assume that A4:
a in the
entourages of
UniformSpaceStr(#
{{}},
SF #)
and A5:
b in the
entourages of
UniformSpaceStr(#
{{}},
SF #)
;
a /\ b in the entourages of UniformSpaceStr(# {{}},SF #)
(
a = [:{{}},{{}}:] &
b = [:{{}},{{}}:] )
by A4, A5, TARSKI:def 1;
hence
a /\ b in the
entourages of
UniformSpaceStr(#
{{}},
SF #)
by TARSKI:def 1;
verum
end; hence
UniformSpaceStr(#
{{}},
SF #) is
cap-closed
by ROUGHS_4:def 2;
( 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 {{}} c= S
hence
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
S [~] in the
entourages of
UniformSpaceStr(#
{{}},
SF #)
hence
UniformSpaceStr(#
{{}},
SF #) is
axiom_U2
;
UniformSpaceStr(# {{}},SF #) is axiom_U3
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
hence
UniformSpaceStr(#
{{}},
SF #) is
axiom_U3
;
verum end;
hence
for X being set
for SF being Subset-Family of [:X,X:] st X = {{}} & SF = {[:X,X:]} holds
UniformSpaceStr(# X,SF #) is UniformSpace
; verum