theorem Th12: :: LATTICE3:12
for A being non empty RelStr st A is complete holds
( A is with_suprema & A is with_infima )