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
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 the carrier of S )
let j be Element of N; :: thesis: ( not the Element of N <= j or N . j in the carrier of S )
assume the Element of N <= j ; :: thesis: N . j in the carrier of S
thus N . j in the carrier of S ; :: thesis: verum