theorem Thm23: :: SRINGS_4:24

for x being non empty set holds product <*x*> = { <*y*> where y is Element of x : verum }