for L being Lattice
for p being Element of L st ex r being Element of L st p "\/" r <> p holds
(.p.> <> the carrier of L