let S be non empty 1-sorted ; :: thesis: for N being non empty NetStr of S
for X being set st rng the mapping of N c= X holds
N is_eventually_in X
let N be non empty NetStr of S; :: thesis: for X being set st rng the mapping of N c= X holds
N is_eventually_in X
let X be set ; :: thesis: ( rng the mapping of N c= X implies N is_eventually_in X )
assume A1: rng the mapping of N c= X ; :: thesis: N is_eventually_in X
consider i being Element of N;
take i ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of N holds
( not i <= b₁ or N . b₁ in X )
let j be Element of N; :: thesis: ( not i <= j or N . j in X )
N . j in rng the mapping of N by FUNCT_2:6;
hence ( not i <= j or N . j in X ) by A1; :: thesis: verum