:: deftheorem Def22 defines initial LATTICES:def 22 :
for L being non empty LattStr
for S being Subset of L holds
( S is initial iff for p, q being Element of L st p [= q & q in S holds
p in S );