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 )

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

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 A2:
for j being Element of N st i <= j holds
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;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

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