theorem :: YELLOW_3:47

for L1, L2 being non empty antisymmetric RelStr
for D being non empty Subset of [:L1,L2:] st ( [:L1,L2:] is complete or ex_inf_of D,[:L1,L2:] ) holds
inf D = [(inf (proj1 D)),(inf (proj2 D))]