( UniformSpaceStr(# X,(rho R) #) is upper & UniformSpaceStr(# X,(rho R) #) is cap-closed ) by Th20;
hence UniformSpaceStr(# X,(rho R) #) is strict upper cap-closed UniformSpaceStr ; :: thesis: verum