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 b1 being Element of the carrier of T st
( b1 in F & b1 <= x & b1 <= y ) )
assume x in F ; :: thesis: ( not y in F or ex b1 being Element of the carrier of T st
( b1 in F & b1 <= x & b1 <= y ) )
then consider i1 being object such that
A1: i1 in dom the mapping of N and
A2: x = the mapping of N . i1 by FUNCT_1:def 3;
assume y in F ; :: thesis: ex b1 being Element of the carrier of T st
( b1 in F & b1 <= x & b1 <= y )
then consider i2 being object such that
A3: i2 in dom the mapping of N and
A4: y = the mapping of N . i2 by FUNCT_1:def 3;
A5: 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, A3;
consider j1 being Element of N such that
A6: 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
A7: 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
A8: j2 <= j and
A9: j1 <= j by YELLOW_6:def 3;
take z = N . j; :: thesis: ( z in F & z <= x & z <= y )
thus z in F by A5, FUNCT_1:def 3; :: thesis: ( z <= x & z <= y )
thus ( z <= x & z <= y ) by A2, A4, A6, A7, A8, A9; :: thesis: verum
end;
hence rng the mapping of N is non empty filtered Subset of T ; :: thesis: verum