theorem Th20: :: PUA2MSS1:21

for A being partial non-empty UAStr
for R being Equivalence_Relation of the carrier of A st R c= DomRel A holds
for i being Element of NAT holds
( R |^ (A,i) is total & R |^ (A,i) is symmetric & R |^ (A,i) is transitive )