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

proof

assume A1: for i being Element of N ex j being Element of N st
( i <= j & N . j in X ) ; :: according to WAYBEL_0:def 12 :: thesis: not N is_eventually_in the carrier of L \ X
let i be Element of N; :: according to WAYBEL_0:def 11 :: thesis: ex j being Element of N st
( i <= j & not N . j in the carrier of L \ X )
consider j being Element of N such that
A2: i <= j and
A3: N . j in X by A1;
take j ; :: thesis: ( i <= j & not N . j in the carrier of L \ X )
thus ( i <= j & not N . j in the carrier of L \ X ) by A2, A3, XBOOLE_0:def 5; :: thesis: verum

end;

assume A4: for i being Element of N ex j being Element of N st
( i <= j & not N . j in the carrier of L \ X ) ; :: according to WAYBEL_0:def 11 :: thesis: N is_often_in X
let i be Element of N; :: according to WAYBEL_0:def 12 :: thesis: ex j being Element of N st
( i <= j & N . j in X )
consider j being Element of N such that
A5: i <= j and
A6: not N . j in the carrier of L \ X by A4;
take j ; :: thesis: ( i <= j & N . j in X )
thus ( i <= j & N . j in X ) by A5, A6, XBOOLE_0:def 5; :: thesis: verum