theorem Th43: :: YELLOW_3:43

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_sup_of D1,S1 & ex_sup_of D2,S2 holds
sup [:D1,D2:] = [(sup D1),(sup D2)]