set L = the non trivial INTegral positive-definite Z_Lattice;
take the non trivial INTegral positive-definite Z_Lattice ; :: thesis: ( not the non trivial INTegral positive-definite Z_Lattice is trivial & the non trivial INTegral positive-definite Z_Lattice is RATional & the non trivial INTegral positive-definite Z_Lattice is positive-definite )
thus ( not the non trivial INTegral positive-definite Z_Lattice is trivial & the non trivial INTegral positive-definite Z_Lattice is RATional & the non trivial INTegral positive-definite Z_Lattice is positive-definite ) by RAT_1:def 2; :: thesis: verum