theorem :: YELLOW_4:35

for L being with_suprema Poset
for D1, D2 being Subset of L holds uparrow ((uparrow D1) "\/" (uparrow D2)) = uparrow (D1 "\/" D2)