theorem Th3: :: YELLOW10:3

for S, T being non empty antisymmetric upper-bounded RelStr holds Top [:S,T:] = [(Top S),(Top T)]