theorem Th7: :: WAYBEL20:7

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