let T be non empty TopSpace; :: thesis: for N being net of
for Y being subnet of N holds Lim N c= Lim Y
let N be net of ; :: 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 set ; :: 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 ex n being Element of st
for p being Element of st n <= p holds
m <= f . p by Def12;
assume A3: x in Lim N ; :: thesis: x in Lim Y
then reconsider p = x as Point of ;
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, Def18;
then consider ii being Element of such that
A4: for j being Element of st ii <= j holds
N . j in V by WAYBEL_0:def 11;
consider n being Element of such that
A5: for p being Element of st n <= p holds
ii <= f . p by A2;
take n ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of Y holds
( not n <= b₁ or Y . b₁ in V )
let j be Element of ; :: 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:21;
hence Y . j in V by A4, A5, A6; :: thesis: verum

end;

hence x in Lim Y by Def18; :: thesis: verum