ex s being eventually-positive Real_Sequence st
( s = seq_a^ (2,1,1) & seq_a^ (2,1,0) in Big_Theta s )