let L be Lattice; :: thesis: the carrier of L is Ideal of L
H₁(L) is Filter of L .: by FILTER_0:15;
hence the carrier of L is Ideal of L by Th21; :: thesis: verum