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