let T be non empty TopSpace; :: thesis: for N being constant net of T holds the_value_of N in Lim N
let N be constant net of T; :: thesis: the_value_of N in Lim N
set p = the_value_of N;
for S being a_neighborhood of the_value_of N holds N is_eventually_in S
proof
set i = the Element of N;
let S be a_neighborhood of the_value_of N; :: thesis: N is_eventually_in S
take the Element of N ; :: according to WAYBEL_0:def 11 :: thesis: for b1 being Element of the carrier of N holds
( not the Element of N <= b1 or N . b1 in S )
let j be Element of N; :: thesis: ( not the Element of N <= j or N . j in S )
assume the Element of N <= j ; :: thesis: N . j in S
N . j = the_value_of N by Th16;
hence N . j in S by CONNSP_2:4; :: thesis: verum
end;
hence the_value_of N in Lim N by Def15; :: thesis: verum