let T be non empty Hausdorff TopSpace; :: thesis: for N being constant net of T holds lim N = the_value_of N
let N be constant net of T; :: thesis: lim N = the_value_of N
the_value_of N in Lim N by Th33;
hence lim N = the_value_of N by Def17; :: thesis: verum