let US be upper UniformSpaceStr ; :: thesis: ( ex R being Relation of the carrier of US st
( the entourages of US = rho R & meet the entourages of US in the entourages of US ) implies the entourages of US = rho (meet the entourages of US) )
given R being Relation of the carrier of US such that A2: the entourages of US = rho R and
A3: meet the entourages of US in the entourages of US ; :: thesis: the entourages of US = rho (meet the entourages of US)
the entourages of US is upper by UNIFORM2:def 7;
hence the entourages of US = rho (meet the entourages of US) by A2, A3, Th29, Th30; :: thesis: verum