theorem Th20: :: UNIFORM2:24

for X being set
for A being Subset of X holds
( id X c= block_Pervin_quasi_uniformity A & (block_Pervin_quasi_uniformity A) * (block_Pervin_quasi_uniformity A) c= block_Pervin_quasi_uniformity A )