reconsider L1 = L as SubLattice of L by NAT_LAT:15;
take L1 ; :: thesis: L1 is complete
thus L1 is complete ; :: thesis: verum