theorem Th61: :: YELLOW_4:61

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