set US = Uniform_Space X;
set E = the entourages of (Uniform_Space X);
thus the entourages of (Uniform_Space X) is upper ; :: according to UNIFORM2:def 7 :: thesis: ( Uniform_Space X is cap-closed & Uniform_Space X is axiom_U1 & not Uniform_Space X is axiom_U2 & Uniform_Space X is axiom_U3 )
thus the entourages of (Uniform_Space X) is cap-closed :: according to UNIFORM2:def 8 :: thesis: ( Uniform_Space X is axiom_U1 & not Uniform_Space X is axiom_U2 & Uniform_Space X is axiom_U3 )
proof
let Y1, Y2 be Subset of [: the carrier of (Uniform_Space X), the carrier of (Uniform_Space X):]; :: according to ROUGHS_4:def 2 :: thesis: ( not Y1 in the entourages of (Uniform_Space X) or not Y2 in the entourages of (Uniform_Space X) or Y1 /\ Y2 in the entourages of (Uniform_Space X) )
thus ( not Y1 in the entourages of (Uniform_Space X) or not Y2 in the entourages of (Uniform_Space X) or Y1 /\ Y2 in the entourages of (Uniform_Space X) ) ; :: thesis: verum
end;
thus for S being Element of the entourages of (Uniform_Space X) holds id the carrier of (Uniform_Space X) c= S ; :: according to UNIFORM2:def 9 :: thesis: ( not Uniform_Space X is axiom_U2 & Uniform_Space X is axiom_U3 )
thus not Uniform_Space X is axiom_U2 ; :: thesis: Uniform_Space X is axiom_U3
let S be Element of the entourages of (Uniform_Space X); :: according to UNIFORM2:def 11 :: thesis: ex W being Element of the entourages of (Uniform_Space X) st W [*] W c= S
S [*] S c= S ;
hence ex W being Element of the entourages of (Uniform_Space X) st W [*] W c= S ; :: thesis: verum