theorem Th39: :: YELLOW_3:39

for S1, S2 being non empty antisymmetric RelStr
for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 holds
( ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) iff ex_sup_of [:D1,D2:],[:S1,S2:] )