theorem Th44: :: YELLOW_3:44

for S1, S2 being non empty antisymmetric RelStr
for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 st ex_inf_of D1,S1 & ex_inf_of D2,S2 holds
inf [:D1,D2:] = [(inf D1),(inf D2)]