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;