theorem :: YELLOW_3:19

for X, Y being non empty reflexive RelStr st [:X,Y:] is with_infima holds
( X is with_infima & Y is with_infima )