let S be non empty 1-sorted ; :: thesis: for N being net of S
for X being set st N is_eventually_in X holds
N is_often_in X
let N be net of S; :: thesis: for X being set st N is_eventually_in X holds
N is_often_in X
let X be set ; :: thesis: ( N is_eventually_in X implies N is_often_in X )
given i being Element of N such that A1: for j being Element of N st i <= j holds
N . j in X ; :: according to WAYBEL_0:def 11 :: thesis: N is_often_in X
let j be Element of N; :: according to WAYBEL_0:def 12 :: thesis: ex b₁ being Element of the carrier of N st
( j <= b₁ & N . b₁ in X )
consider z being Element of N such that
A2: ( i <= z & j <= z ) by Def3;
take z ; :: thesis: ( j <= z & N . z in X )
thus ( j <= z & N . z in X ) by A1, A2; :: thesis: verum