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