set X = {{}};
reconsider SF = {[:{{}},{{}}:]} as Subset-Family of [:{{}},{{}}:] by ZFMISC_1:68;
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 )
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 #):]; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum
end;
then 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 )
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 #):]; :: thesis: ( 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 #) ; :: thesis: 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; :: thesis: verum
end;
hence UniformSpaceStr(# {{}},SF #) is cap-closed by ROUGHS_4:def 2; :: 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 {{}} c= S
proof
let S be Element of the entourages of UniformSpaceStr(# {{}},SF #); :: thesis: id {{}} c= S
S = [:{{}},{{}}:] by TARSKI:def 1;
hence id {{}} c= S ; :: thesis: verum
end;
hence UniformSpaceStr(# {{}},SF #) is axiom_U1 ; :: thesis: ( 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 #)
proof
let S be Element of the entourages of UniformSpaceStr(# {{}},SF #); :: thesis: S [~] in the entourages of UniformSpaceStr(# {{}},SF #)
S = [:{{}},{{}}:] by TARSKI:def 1;
then S [~] = [:{{}},{{}}:] by SYSREL:5;
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
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
proof
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
take S ; :: thesis: S [*] S c= S
S = [:{{}},{{}}:] by TARSKI:def 1;
hence S [*] S c= S ; :: thesis: verum
end;
hence UniformSpaceStr(# {{}},SF #) is axiom_U3 ; :: thesis: 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 ; :: thesis: verum