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