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