theorem :: YELLOW_4:45

for L being antisymmetric with_infima RelStr
for A being lower Subset of L
for B, C being Subset of L holds (A \/ B) "/\" (A \/ C) c= A \/ (B "/\" C)