let T be complete Lawson TopLattice; :: thesis: for N being eventually-filtered net of T holds rng the mapping of N is non empty filtered Subset of T
let N be eventually-filtered net of T; :: thesis: rng the mapping of N is non empty filtered Subset of T
reconsider F = rng the mapping of N as non empty Subset of T ;
F is filtered

proof

let x, y be Element of T; :: according to WAYBEL_0:def 2 :: thesis: ( not x in F or not y in F or ex b₁ being Element of the carrier of T st
( b₁ in F & b₁ <= x & b₁ <= y ) )
assume x in F ; :: thesis: ( not y in F or ex b₁ being Element of the carrier of T st
( b₁ in F & b₁ <= x & b₁ <= y ) )
then consider i1 being set such that
A1: ( i1 in dom the mapping of N & x = the mapping of N . i1 ) by FUNCT_1:def 5;
assume y in F ; :: thesis: ex b₁ being Element of the carrier of T st
( b₁ in F & b₁ <= x & b₁ <= y )
then consider i2 being set such that
A2: ( i2 in dom the mapping of N & y = the mapping of N . i2 ) by FUNCT_1:def 5;
A3: dom the mapping of N = the carrier of N by FUNCT_2:def 1;
reconsider i1 = i1, i2 = i2 as Element of N by A1, A2;
consider j1 being Element of N such that
A4: for k being Element of N st j1 <= k holds
N . i1 >= N . k by WAYBEL_0:12;
consider j2 being Element of N such that
A5: for k being Element of N st j2 <= k holds
N . i2 >= N . k by WAYBEL_0:12;
consider j being Element of N such that
A6: ( j2 <= j & j1 <= j ) by YELLOW_6:def 5;
take z = N . j; :: thesis: ( z in F & z <= x & z <= y )
thus z in F by A3, FUNCT_1:def 5; :: thesis: ( z <= x & z <= y )
thus ( z <= x & z <= y ) by A1, A2, A4, A5, A6; :: thesis: verum

end;

hence rng the mapping of N is non empty filtered Subset of T ; :: thesis: verum