set T = the 1 -element LATTICE;
take the 1 -element LATTICE ; :: thesis: the 1 -element LATTICE is Mizar-widening-like
thus the 1 -element LATTICE is sup-Semilattice ; :: according to ABCMIZ_0:def 3 :: thesis: the 1 -element LATTICE is Noetherian
thus the 1 -element LATTICE is Noetherian ; :: thesis: verum