:: deftheorem Def7 defines with_infima KNASTER:def 7 :
for L being non empty LattStr
for P being Subset of L holds
( P is with_infima iff for x, y being Element of L st x in P & y in P holds
ex z being Element of L st
( z in P & z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= z ) ) );