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
proof
let Y1, Y2 be Subset of [: the carrier of NonEmptyTrivialUniformSpace, the carrier of NonEmptyTrivialUniformSpace:]; :: thesis: ( Y1 in the entourages of NonEmptyTrivialUniformSpace & Y1 c= Y2 implies Y2 in the entourages of NonEmptyTrivialUniformSpace )
assume that
A2: Y1 in the entourages of NonEmptyTrivialUniformSpace and
A3: Y1 c= Y2 ; :: thesis: Y2 in the entourages of NonEmptyTrivialUniformSpace
A4: Y1 = [:{{}},{{}}:] by B1, B2, A2, TARSKI:def 1;
Y1 = Y2 by B2, A3, A4;
hence Y2 in the entourages of NonEmptyTrivialUniformSpace by A2; :: thesis: verum
end;
hence the entourages of NonEmptyTrivialUniformSpace is upper ; :: according to UNIFORM2:def 7 :: thesis: ( 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:]; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum
end;
hence NonEmptyTrivialUniformSpace is cap-closed by ROUGHS_4:def 2; :: thesis: ( 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
proof
let S be Element of the entourages of NonEmptyTrivialUniformSpace; :: thesis: id {{}} c= S
S = [:{{}},{{}}:] by B1, B2, TARSKI:def 1;
hence id {{}} c= S ; :: thesis: verum
end;
hence NonEmptyTrivialUniformSpace is axiom_U1 by B2; :: thesis: ( 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 :: according to UNIFORM2:def 10 :: thesis: NonEmptyTrivialUniformSpace is axiom_U3
proof
let S be Element of the entourages of NonEmptyTrivialUniformSpace; :: thesis: S ~ in the entourages of NonEmptyTrivialUniformSpace
S = [:{{}},{{}}:] by B1, B2, TARSKI:def 1;
then S ~ = [:{{}},{{}}:] by SYSREL:5;
hence S ~ in the entourages of NonEmptyTrivialUniformSpace by B1, B2, TARSKI:def 1; :: thesis: verum
end;
let S be Element of the entourages of NonEmptyTrivialUniformSpace; :: according to UNIFORM2:def 11 :: thesis: ex W being Element of the entourages of NonEmptyTrivialUniformSpace st W [*] W c= S
take S ; :: thesis: S [*] S c= S
S = [:{{}},{{}}:] by B1, B2, TARSKI:def 1;
hence S [*] S c= S by B2; :: thesis: verum