theorem :: LATTICE3:10

for A being RelStr holds
( A is with_suprema iff A ~ is with_infima )