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