let L be RelStr ; :: thesis: ( L is with_infima iff L opp is with_suprema )
( L is with_infima iff (L opp) ~ is with_infima ) by Th14;
hence ( L is with_infima iff L opp is with_suprema ) by LATTICE3:10; :: thesis: verum