theorem Th29: :: WAYBEL27:29

for S, T being non empty reflexive antisymmetric RelStr holds UPS ((id S),(id T)) = id (UPS (S,T))