set US = Uniform_Space {{}};
set E = the entourages of (Uniform_Space {{}});
thus the entourages of (Uniform_Space {{}}) is upper ; :: according to UNIFORM2:def 7 :: thesis: ( Uniform_Space {{}} is cap-closed & not Uniform_Space {{}} is axiom_U2 )
thus the entourages of (Uniform_Space {{}}) is cap-closed :: according to UNIFORM2:def 8 :: thesis: not Uniform_Space {{}} is axiom_U2
proof
let Y1, Y2 be Subset of [: the carrier of (Uniform_Space {{}}), the carrier of (Uniform_Space {{}}):]; :: according to ROUGHS_4:def 2 :: thesis: ( not Y1 in the entourages of (Uniform_Space {{}}) or not Y2 in the entourages of (Uniform_Space {{}}) or Y1 /\ Y2 in the entourages of (Uniform_Space {{}}) )
thus ( not Y1 in the entourages of (Uniform_Space {{}}) or not Y2 in the entourages of (Uniform_Space {{}}) or Y1 /\ Y2 in the entourages of (Uniform_Space {{}}) ) ; :: thesis: verum
end;
thus not Uniform_Space {{}} is axiom_U2 ; :: thesis: verum