for L being Lattice
for K being Sublattice of L
for a being Element of K holds a is Element of L by NAT_LAT:def 12, TARSKI:def 3;