:: deftheorem Def8 defines latt KNASTER:def 8 :
for L being Lattice
for P being non empty with_suprema with_infima Subset of L
for b₃ being strict Lattice holds
( b₃ = latt P iff ( the carrier of b₃ = P & ( for x, y being Element of b₃ ex x9, y9 being Element of L st
( x = x9 & y = y9 & ( x [= y implies x9 [= y9 ) & ( x9 [= y9 implies x [= y ) ) ) ) );