:: deftheorem Def6 defines with_suprema KNASTER:def 6 :
for L being non empty LattStr
for P being Subset of L holds
( P is with_suprema 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 & x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
z [= z9 ) ) );