set L = the complete LATTICE;
take the complete LATTICE |^ {} ; :: thesis: ( the complete LATTICE |^ {} is constituted-Functions & the complete LATTICE |^ {} is complete & the complete LATTICE |^ {} is strict )
thus ( the complete LATTICE |^ {} is constituted-Functions & the complete LATTICE |^ {} is complete & the complete LATTICE |^ {} is strict ) ; :: thesis: verum