-(* notion 1998 *)
-definition l_e_st_eq_landau_n_rt_iii1_t20 ≝ λs:l_e_st_set l_e_st_eq_landau_n_rt_rat.λs1:Πx:l_e_st_eq_landau_n_rt_rat.Πt:l_e_st_eq_landau_n_rt_in x s.l_e_st_eq_landau_n_rt_some (λy:l_e_st_eq_landau_n_rt_rat.l_and (l_e_st_eq_landau_n_rt_in y s) (l_e_st_eq_landau_n_rt_more y x)).λx0:l_e_st_eq_landau_n_rt_rat.λi:l_e_st_eq_landau_n_rt_in x0 s.(s1 x0 i : l_e_st_eq_landau_n_rt_some (λy:l_e_st_eq_landau_n_rt_rat.l_and (l_e_st_eq_landau_n_rt_in y s) (l_e_st_eq_landau_n_rt_more y x0))).
+(* constant 1998 *)
+definition l_e_st_eq_landau_n_rt_iii1_t20 ≝ λs:l_e_st_set l_e_st_eq_landau_n_rt_rat.λs1:∀x:l_e_st_eq_landau_n_rt_rat.∀t:l_e_st_eq_landau_n_rt_in x s.l_e_st_eq_landau_n_rt_some (λy:l_e_st_eq_landau_n_rt_rat.l_and (l_e_st_eq_landau_n_rt_in y s) (l_e_st_eq_landau_n_rt_more y x)).λx0:l_e_st_eq_landau_n_rt_rat.λi:l_e_st_eq_landau_n_rt_in x0 s.(s1 x0 i : l_e_st_eq_landau_n_rt_some (λy:l_e_st_eq_landau_n_rt_rat.l_and (l_e_st_eq_landau_n_rt_in y s) (l_e_st_eq_landau_n_rt_more y x0))).
+
+(* constant 1999 *)
+definition l_e_st_eq_landau_n_rt_iii1_t21 ≝ λs:l_e_st_set l_e_st_eq_landau_n_rt_rat.λs1:∀x:l_e_st_eq_landau_n_rt_rat.∀t:l_e_st_eq_landau_n_rt_in x s.l_e_st_eq_landau_n_rt_some (λy:l_e_st_eq_landau_n_rt_rat.l_and (l_e_st_eq_landau_n_rt_in y s) (l_e_st_eq_landau_n_rt_more y x)).λx0:l_e_st_eq_landau_n_rt_rat.λi:l_e_st_eq_landau_n_rt_in x0 s.λy0:l_e_st_eq_landau_n_rt_rat.λa:l_and (l_e_st_eq_landau_n_rt_in y0 s) (l_e_st_eq_landau_n_rt_more y0 x0).(l_ande1 (l_e_st_eq_landau_n_rt_in y0 s) (l_e_st_eq_landau_n_rt_more y0 x0) a : l_e_st_eq_landau_n_rt_in y0 s).