( seq_logn in Big_Oh (seq_n^ (1 / 2)) & not seq_logn in Big_Omega (seq_n^ (1 / 2)) ) by Th4, Th5;
hence ( seq_n^ (1 / 2) in Big_Omega seq_logn & not seq_logn in Big_Omega (seq_n^ (1 / 2)) ) by ASYMPT_0:19; :: thesis: verum