let L1 be Z_Sublattice of L; :: thesis: L1 is positive-definite
thus for w being Vector of L1 st w <> 0. L1 holds
||.w.|| > 0 :: according to ZMODLAT1:def 6 :: thesis: verum
proof
let w be Vector of L1; :: thesis: ( w <> 0. L1 implies ||.w.|| > 0 )
assume A1: w <> 0. L1 ; :: thesis: ||.w.|| > 0
reconsider v = w as Vector of L by ThSL4;
v <> 0. L by A1, defSublattice;
then ||.v.|| > 0 by defPositive;
hence ||.w.|| > 0 by ThSL18; :: thesis: verum
end;