let L be non empty 1-sorted ; :: thesis: for N being non empty NetStr over L
for X being set holds
( N is_eventually_in X iff not N is_often_in the carrier of L \ X )
let N be non empty NetStr over L; :: thesis: for X being set holds
( N is_eventually_in X iff not N is_often_in the carrier of L \ X )
let X be set ; :: thesis: ( N is_eventually_in X iff not N is_often_in the carrier of L \ X )
set Y = the carrier of L \ X;
thus ( N is_eventually_in X implies not N is_often_in the carrier of L \ X ) :: thesis: ( not N is_often_in the carrier of L \ X implies N is_eventually_in X )

proof

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: not N is_often_in the carrier of L \ X
take i ; :: according to WAYBEL_0:def 12 :: thesis: for j being Element of N holds
( not i <= j or not N . j in the carrier of L \ X )
let j be Element of N; :: thesis: ( not i <= j or not N . j in the carrier of L \ X )
assume i <= j ; :: thesis: not N . j in the carrier of L \ X
then N . j in X by A1;
hence not N . j in the carrier of L \ X by XBOOLE_0:def 5; :: thesis: verum

end;

given i being Element of N such that A2: for j being Element of N st i <= j holds
not N . j in the carrier of L \ X ; :: according to WAYBEL_0:def 12 :: thesis: N is_eventually_in X
take i ; :: according to WAYBEL_0:def 11 :: thesis: for j being Element of N st i <= j holds
N . j in X
let j be Element of N; :: thesis: ( i <= j implies N . j in X )
assume i <= j ; :: thesis: N . j in X
then not N . j in the carrier of L \ X by A2;
hence N . j in X by XBOOLE_0:def 5; :: thesis: verum