let L be non empty 1-sorted ; :: thesis: for N being non empty NetStr over L

for X, Y being set st X c= Y holds

( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) )

let N be non empty NetStr over L; :: thesis: for X, Y being set st X c= Y holds

( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) )

let X, Y be set ; :: thesis: ( X c= Y implies ( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) ) )

assume A1: X c= Y ; :: thesis: ( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) )

( i <= j & N . j in X ) ; :: according to WAYBEL_0:def 12 :: thesis: N is_often_in Y

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 Y )

consider j being Element of N such that

A4: i <= j and

A5: N . j in X by A3;

take j ; :: thesis: ( i <= j & N . j in Y )

thus ( i <= j & N . j in Y ) by A1, A4, A5; :: thesis: verum

for X, Y being set st X c= Y holds

( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) )

let N be non empty NetStr over L; :: thesis: for X, Y being set st X c= Y holds

( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) )

let X, Y be set ; :: thesis: ( X c= Y implies ( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) ) )

assume A1: X c= Y ; :: thesis: ( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) )

hereby :: thesis: ( N is_often_in X implies N is_often_in Y )

assume A3:
for i being Element of N ex j being Element of N st assume
N is_eventually_in X
; :: thesis: N is_eventually_in Y

then consider i being Element of N such that

A2: for j being Element of N st i <= j holds

N . j in X ;

thus N is_eventually_in Y :: thesis: verum

end;then consider i being Element of N such that

A2: for j being Element of N st i <= j holds

N . j in X ;

thus N is_eventually_in Y :: thesis: verum

( i <= j & N . j in X ) ; :: according to WAYBEL_0:def 12 :: thesis: N is_often_in Y

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 Y )

consider j being Element of N such that

A4: i <= j and

A5: N . j in X by A3;

take j ; :: thesis: ( i <= j & N . j in Y )

thus ( i <= j & N . j in Y ) by A1, A4, A5; :: thesis: verum