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