let S be non empty 1-sorted ; :: thesis: for N being net of S holds N is_eventually_in the carrier of S
let N be net of S; :: thesis: N is_eventually_in the carrier of S
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 the carrier of S )
let j be Element of N; :: thesis: ( not i <= j or N . j in the carrier of S )
assume i <= j ; :: thesis: N . j in the carrier of S
thus N . j in the carrier of S ; :: thesis: verum