now

thus StoneH L is one-to-one ; :: thesis: StoneH L is onto
thus StoneH L is onto :: thesis: verum

proof

thus rng (StoneH L) = the carrier of (StoneLatt L) ; :: according to FUNCT_2:def 3 :: thesis: verum

end;

end;

hence for b₁ being Function of L,(StoneLatt L) st b₁ = StoneH L holds
b₁ is bijective by FUNCT_2:def 4; :: thesis: verum