theorem Th16: :: YELLOW_7:16

for L being RelStr holds
( L is with_infima iff L opp is with_suprema )