theorem Th10: :: YELLOW_7:10

for L being RelStr
for X being set holds
( ex_sup_of X,L iff ex_inf_of X,L opp )