set L = the strict complete LATTICE;
take the strict complete LATTICE ; :: thesis: ( the strict complete LATTICE is complete & the strict complete LATTICE is strict )
thus ( the strict complete LATTICE is complete & the strict complete LATTICE is strict ) ; :: thesis: verum