theorem Th11: :: YELLOW_7:11

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