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