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

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

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

proof

take i ; :: according to WAYBEL_0:def 11 :: thesis: for j being Element of N st i <= j holds
N . j in Y
let j be Element of N; :: thesis: ( i <= j implies N . j in Y )
assume i <= j ; :: thesis: N . j in Y
then N . j in X by A2;
hence N . j in Y by A1; :: thesis: verum

end;

end;

assume A3: 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: 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