reconsider OL = Open_setLatt T as 0_Lattice by Th10;
OL is I_Lattice by Th9;
hence Open_setLatt T is Heyting ; :: thesis: verum