let L be positive-definite Z_Lattice; :: thesis: for v being Vector of L holds ||.v.|| >= 0
let v be Vector of L; :: thesis: ||.v.|| >= 0

per cases ( v = 0. L or v <> 0. L ) ;

suppose v = 0. L ; :: thesis: ||.v.|| >= 0

hence ||.v.|| >= 0 by ThSc6; :: thesis: verum

end;

suppose v <> 0. L ; :: thesis: ||.v.|| >= 0

hence ||.v.|| >= 0 by defPositive; :: thesis: verum

end;

end;