theorem Th23: :: YELLOW_2:23

for L being non empty RelStr holds
( ( for X being set holds ex_sup_of X,L ) iff for Y being set holds ex_inf_of Y,L )