theorem Th133: :: FINSEQ_3:135

for X being set holds
( Union <*X*> = X & meet <*X*> = X )