theorem Th22: :: UNIFORM3:46

for X being set
for R being symmetric Relation of X holds rho R is axiom_UP2