let S be non empty 1-sorted ; :: thesis: for N being non empty NetStr over 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 over 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
set i = the Element of N;
take the Element of N ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of N holds
( not the Element of N <= b₁ or N . b₁ in X )
let j be Element of N; :: thesis: ( not the Element of N <= j or N . j in X )
N . j in rng the mapping of N by FUNCT_2:4;
hence ( not the Element of N <= j or N . j in X ) by A1; :: thesis: verum