theorem :: NAT_LAT:15

for L being Lattice holds L is SubLattice of L