:: deftheorem Def11 defines with_infima LATTICE3:def 11 :
for IT being RelStr holds
( IT is with_infima iff for x, y being Element of IT ex z being Element of IT st
( z <= x & z <= y & ( for z9 being Element of IT st z9 <= x & z9 <= y holds
z9 <= z ) ) );