theorem :: FINSEQ_3:33

for x, y being object holds {} <> <*x,y*> ;