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 )

( 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

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 A4:
for i being Element of N ex j being Element of N st
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;( 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

( 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