let T be non empty TopSpace; :: thesis: for N being net of T
for Y being subnet of N holds Lim N c= Lim Y
let N be net of T; :: thesis: for Y being subnet of N holds Lim N c= Lim Y
let Y be subnet of N; :: thesis: Lim N c= Lim Y
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Lim N or x in Lim Y )
consider f being Function of Y,N such that
A1: the mapping of Y = the mapping of N * f and
A2: for m being Element of N ex n being Element of Y st
for p being Element of Y st n <= p holds
m <= f . p by Def9;
assume A3: x in Lim N ; :: thesis: x in Lim Y
then reconsider p = x as Point of T ;
for V being a_neighborhood of p holds Y is_eventually_in V
proof
let V be a_neighborhood of p; :: thesis: Y is_eventually_in V
N is_eventually_in V by A3, Def15;
then consider ii being Element of N such that
A4: for j being Element of N st ii <= j holds
N . j in V ;
consider n being Element of Y such that
A5: for p being Element of Y st n <= p holds
ii <= f . p by A2;
take n ; :: according to WAYBEL_0:def 11 :: thesis: for b1 being Element of the carrier of Y holds
( not n <= b1 or Y . b1 in V )
let j be Element of Y; :: thesis: ( not n <= j or Y . j in V )
assume A6: n <= j ; :: thesis: Y . j in V
N . (f . j) = Y . j by A1, FUNCT_2:15;
hence Y . j in V by A4, A5, A6; :: thesis: verum
end;
hence x in Lim Y by Def15; :: thesis: verum