theorem Th32: :: YELLOW_4:32

for L being transitive antisymmetric with_suprema RelStr
for D1, D2 being Subset of L holds downarrow ((downarrow D1) "\/" (downarrow D2)) c= downarrow (D1 "\/" D2)