let L be Lattice; :: thesis: for K being Sublattice of L
for a being Element of K holds a is Element of L
let K be Sublattice of L; :: thesis: for a being Element of K holds a is Element of L
H₁(K) c= H₁(L) by NAT_LAT:def 12;
hence for a being Element of K holds a is Element of L by TARSKI:def 3; :: thesis: verum