theorem Th134: :: FINSEQ_3:136

for X, Y being set holds
( Union <*X,Y*> = X \/ Y & meet <*X,Y*> = X /\ Y )